%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PLA025+1 : TPTP v9.3.1. Bugfixed v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n016.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:27:45 PM UTC 2026
% Result : CounterSatisfiable 14.18s 3.12s
% Output : Saturation 14.94s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u289,negated_conjecture,
~ on(block_6,table,sK0) ).
cnf(u509,hypothesis,
~ clear(table,time_0) ).
cnf(u512,hypothesis,
~ nonfixed(table) ).
cnf(u1783,hypothesis,
clear(block_9,s(s(s(s(s(s(time_0))))))) ).
cnf(u545,hypothesis,
clear(block_9,s(s(s(s(s(time_0)))))) ).
cnf(u552,hypothesis,
~ clear(block_8,s(s(s(s(s(s(time_0))))))) ).
cnf(u680,hypothesis,
~ clear(block_8,s(s(s(s(s(time_0)))))) ).
cnf(u562,hypothesis,
~ clear(block_7,s(s(s(s(s(s(time_0))))))) ).
cnf(u702,hypothesis,
~ clear(block_7,s(s(s(s(s(time_0)))))) ).
cnf(u572,hypothesis,
~ clear(block_6,s(s(s(s(s(s(time_0))))))) ).
cnf(u575,hypothesis,
clear(block_6,s(s(s(s(s(time_0)))))) ).
cnf(u1489,hypothesis,
clear(block_5,s(s(s(s(s(s(time_0))))))) ).
cnf(u647,hypothesis,
~ clear(block_5,s(s(s(s(s(time_0)))))) ).
cnf(u588,hypothesis,
source(block_5,s(s(s(s(s(time_0)))))) ).
cnf(u592,hypothesis,
~ clear(block_4,s(s(s(s(s(s(time_0))))))) ).
cnf(u669,hypothesis,
~ clear(block_4,s(s(s(s(s(time_0)))))) ).
cnf(u4794,hypothesis,
clear(block_3,s(s(s(s(s(s(time_0))))))) ).
cnf(u605,hypothesis,
clear(block_3,s(s(s(s(s(time_0)))))) ).
cnf(u612,hypothesis,
~ clear(block_2,s(s(s(s(s(s(time_0))))))) ).
cnf(u723,hypothesis,
~ clear(block_2,s(s(s(s(s(time_0)))))) ).
cnf(u622,hypothesis,
~ clear(block_1,s(s(s(s(s(s(time_0))))))) ).
cnf(u736,hypothesis,
~ clear(block_1,s(s(s(s(s(time_0)))))) ).
cnf(u639,hypothesis,
destination(block_6,s(s(s(s(s(time_0)))))) ).
cnf(u781,hypothesis,
~ clear(block_8,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u788,hypothesis,
~ clear(block_7,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u795,hypothesis,
~ clear(block_6,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u802,hypothesis,
~ clear(block_5,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u809,hypothesis,
~ clear(block_4,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u823,hypothesis,
~ clear(block_2,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u830,hypothesis,
~ clear(block_1,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u915,hypothesis,
destination(block_5,s(s(s(s(s(s(time_0))))))) ).
cnf(u1151,hypothesis,
on(block_9,table,s(s(s(s(s(time_0)))))) ).
cnf(u10398,hypothesis,
~ on(block_9,table,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u1224,hypothesis,
on(block_9,table,s(s(s(s(time_0))))) ).
cnf(u1249,hypothesis,
clear(block_6,s(s(s(s(time_0))))) ).
cnf(u7088,hypothesis,
~ clear(block_5,s(s(s(s(time_0))))) ).
cnf(u2319,hypothesis,
clear(block_9,s(s(s(s(time_0))))) ).
cnf(u1284,hypothesis,
~ clear(block_8,s(s(s(s(time_0))))) ).
cnf(u1294,hypothesis,
destination(block_7,s(s(s(s(time_0))))) ).
cnf(u1298,hypothesis,
~ clear(block_4,s(s(s(s(time_0))))) ).
cnf(u8742,hypothesis,
clear(block_3,s(s(s(s(time_0))))) ).
cnf(u1312,hypothesis,
~ clear(block_2,s(s(s(s(time_0))))) ).
cnf(u1319,hypothesis,
~ clear(block_1,s(s(s(s(time_0))))) ).
cnf(u1363,hypothesis,
on(block_5,block_4,s(s(s(s(time_0))))) ).
cnf(u1510,hypothesis,
on(block_9,table,s(s(s(time_0)))) ).
cnf(u4386,hypothesis,
~ clear(block_4,s(s(s(time_0)))) ).
cnf(u4372,hypothesis,
~ clear(block_6,s(s(s(time_0)))) ).
cnf(u1548,hypothesis,
source(block_6,s(s(s(time_0)))) ).
cnf(u7091,hypothesis,
~ clear(block_5,s(s(s(time_0)))) ).
cnf(u7511,hypothesis,
clear(block_8,s(s(s(time_0)))) ).
cnf(u1575,hypothesis,
destination(block_8,s(s(s(time_0)))) ).
cnf(u2632,hypothesis,
clear(block_7,s(s(s(time_0)))) ).
cnf(u8740,hypothesis,
clear(block_3,s(s(s(time_0)))) ).
cnf(u1593,hypothesis,
~ clear(block_2,s(s(s(time_0)))) ).
cnf(u1600,hypothesis,
~ clear(block_1,s(s(s(time_0)))) ).
cnf(u2313,hypothesis,
clear(block_9,s(s(s(time_0)))) ).
cnf(u1633,hypothesis,
on(block_9,table,s(s(time_0))) ).
cnf(u1689,hypothesis,
~ neq(block_9,block_9) ).
cnf(u1696,hypothesis,
object(block_8,s(s(time_0))) ).
cnf(u1751,hypothesis,
object(block_9,s(s(s(s(s(s(time_0))))))) ).
cnf(u1762,hypothesis,
on(block_9,table,s(s(s(s(s(s(time_0))))))) ).
cnf(u2041,hypothesis,
~ time(s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u2068,hypothesis,
( ~ on(block_9,X0,time_0)
| on(block_9,X0,s(time_0))
| ~ neq(block_9,X0)
| ~ a_block(X0) ) ).
cnf(u2078,hypothesis,
( ~ on(block_5,X0,time_0)
| on(block_5,X0,s(time_0))
| ~ neq(block_5,X0)
| ~ a_block(X0) ) ).
cnf(u2089,hypothesis,
object(block_3,time_0) ).
cnf(u2142,hypothesis,
~ clear(block_8,s(time_0)) ).
cnf(u2149,hypothesis,
~ clear(block_7,s(time_0)) ).
cnf(u2156,hypothesis,
~ clear(block_6,s(time_0)) ).
cnf(u2163,hypothesis,
~ clear(block_4,s(time_0)) ).
cnf(u4300,hypothesis,
clear(block_2,s(time_0)) ).
cnf(u2173,hypothesis,
source(block_2,time_0) ).
cnf(u2177,hypothesis,
~ clear(block_1,s(time_0)) ).
cnf(u5765,hypothesis,
clear(block_8,s(s(time_0))) ).
cnf(u2270,hypothesis,
~ clear(block_7,s(s(time_0))) ).
cnf(u7471,hypothesis,
clear(block_3,s(s(time_0))) ).
cnf(u4376,hypothesis,
clear(block_2,s(s(time_0))) ).
cnf(u2287,hypothesis,
destination(block_2,s(s(time_0))) ).
cnf(u2291,hypothesis,
~ clear(block_1,s(s(time_0))) ).
cnf(u2965,hypothesis,
clear(block_9,s(time_0)) ).
cnf(u4217,hypothesis,
clear(block_3,s(time_0)) ).
cnf(u2421,hypothesis,
( ~ object(X0,s(s(time_0)))
| ~ nonfixed(X0)
| ~ neq(X0,block_8)
| on(X0,block_8,s(s(s(time_0)))) ) ).
cnf(u2587,hypothesis,
on(block_7,block_6,s(s(time_0))) ).
cnf(u2663,hypothesis,
object(block_9,s(time_0)) ).
cnf(u2726,hypothesis,
object(block_7,s(s(s(time_0)))) ).
cnf(u2904,hypothesis,
on(block_5,block_4,s(s(time_0))) ).
cnf(u2926,hypothesis,
on(block_5,block_4,s(s(s(time_0)))) ).
cnf(u4368,hypothesis,
clear(block_9,s(s(time_0))) ).
cnf(u2973,hypothesis,
~ clear(block_5,s(s(time_0))) ).
cnf(u2996,hypothesis,
~ clear(block_5,s(time_0)) ).
cnf(u3063,hypothesis,
source(block_7,s(s(time_0))) ).
cnf(u3085,hypothesis,
source(table,s(s(s(s(time_0))))) ).
cnf(u3104,hypothesis,
source(table,s(s(s(s(s(s(time_0))))))) ).
cnf(u3164,hypothesis,
on(block_4,table,s(s(time_0))) ).
cnf(u3342,hypothesis,
on(block_7,block_6,s(s(s(time_0)))) ).
cnf(u3471,hypothesis,
on(block_1,table,s(s(s(s(time_0))))) ).
cnf(u3518,hypothesis,
on(block_1,table,s(s(time_0))) ).
cnf(u3559,hypothesis,
on(block_1,table,s(s(s(time_0)))) ).
cnf(u3846,hypothesis,
on(block_4,table,s(s(s(time_0)))) ).
cnf(u3862,hypothesis,
on(block_4,table,s(s(s(s(time_0))))) ).
cnf(u3888,hypothesis,
on(block_4,table,s(s(s(s(s(time_0)))))) ).
cnf(u4215,hypothesis,
on(block_2,block_1,s(s(s(time_0)))) ).
cnf(u4305,hypothesis,
on(block_2,block_1,s(s(time_0))) ).
cnf(u4405,hypothesis,
destination(block_5,time_0) ).
cnf(u4576,hypothesis,
destination(table,s(time_0)) ).
cnf(u4579,hypothesis,
( ~ object(X0,s(time_0))
| ~ nonfixed(X0)
| ~ neq(X0,block_9) ) ).
cnf(u4600,hypothesis,
( ~ object(X0,s(time_0))
| ~ nonfixed(X0)
| ~ neq(X0,block_9)
| on(X0,block_9,s(s(time_0))) ) ).
cnf(u4681,hypothesis,
on(block_3,block_5,s(s(time_0))) ).
cnf(u4820,hypothesis,
object(block_3,s(s(s(s(s(time_0)))))) ).
cnf(u5323,hypothesis,
on(block_3,block_6,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u5432,hypothesis,
source(block_8,s(time_0)) ).
cnf(u5888,hypothesis,
~ clear(block_4,s(s(time_0))) ).
cnf(u5962,hypothesis,
on(block_5,block_4,s(s(s(s(s(time_0)))))) ).
cnf(u6614,hypothesis,
on(block_5,block_4,s(s(s(s(s(s(time_0))))))) ).
cnf(u6637,hypothesis,
on(block_5,block_4,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u6751,hypothesis,
on(block_9,block_5,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u6933,hypothesis,
on(block_1,table,s(s(s(s(s(time_0)))))) ).
cnf(u7792,hypothesis,
on(block_3,block_5,s(s(s(s(time_0))))) ).
cnf(u7869,hypothesis,
on(block_4,table,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u8542,hypothesis,
on(block_7,block_8,s(s(s(s(s(time_0)))))) ).
cnf(u8646,hypothesis,
on(block_7,block_8,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u8692,hypothesis,
on(block_3,block_5,s(time_0)) ).
cnf(u8696,hypothesis,
on(block_3,block_5,s(s(s(time_0)))) ).
cnf(u9498,hypothesis,
on(block_8,block_2,s(s(s(s(time_0))))) ).
cnf(u9719,hypothesis,
object(block_6,s(s(s(s(time_0))))) ).
cnf(u9985,hypothesis,
on(block_6,table,s(s(time_0))) ).
cnf(u10455,hypothesis,
on(block_6,block_7,s(s(s(s(s(s(time_0))))))) ).
cnf(u10695,hypothesis,
on(block_6,block_7,s(s(s(s(s(time_0)))))) ).
cnf(u9384,hypothesis,
( ~ on(X0,block_6,s(s(s(s(time_0)))))
| ~ object(X0,s(s(s(time_0))))
| ~ neq(X0,block_6)
| ~ nonfixed(X0) ) ).
cnf(u248,hypothesis,
on(block_3,block_2,time_0) ).
cnf(u1384,hypothesis,
( ~ destination(X0,s(s(time_0)))
| ~ clear(X0,s(s(s(time_0))))
| ~ nonfixed(X0) ) ).
cnf(u7407,hypothesis,
( ~ on(X0,block_1,s(s(s(time_0))))
| ~ neq(block_2,X0)
| ~ neq(block_1,X0)
| ~ nonfixed(X0) ) ).
cnf(u2075,hypothesis,
( ~ on(block_6,X0,time_0)
| ~ a_block(X0)
| ~ neq(block_6,X0)
| on(block_6,X0,s(time_0)) ) ).
cnf(u2206,hypothesis,
( ~ on(block_7,X1,X2)
| ~ nonfixed(X0)
| ~ neq(block_7,X0)
| ~ neq(X1,X0)
| ~ nonfixed(X1)
| ~ neq(block_7,X1)
| ~ on(X0,X1,X2) ) ).
cnf(u10809,hypothesis,
( ~ source(X0,s(s(s(s(time_0)))))
| ~ a_block(X0)
| ~ neq(table,X0) ) ).
cnf(u521,hypothesis,
~ clear(block_4,time_0) ).
cnf(u276,axiom,
( ~ time(X0)
| ~ on(X1,X2,s(X0))
| destination(X2,X0)
| on(X1,X2,X0)
| ~ a_block(X2)
| ~ neq(X1,X2)
| ~ nonfixed(X1) ) ).
cnf(u10808,hypothesis,
~ destination(table,s(s(s(s(time_0))))) ).
cnf(u406,hypothesis,
neq(block_3,block_4) ).
cnf(u1944,hypothesis,
( ~ on(block_2,X2,X1)
| ~ a_block(X0)
| ~ neq(block_2,X0)
| ~ neq(X2,X0)
| ~ a_block(X2)
| ~ neq(block_2,X2)
| ~ on(block_2,X0,X1) ) ).
cnf(u1327,hypothesis,
~ object(block_4,s(s(s(s(time_0))))) ).
cnf(u6669,hypothesis,
~ neq(block_4,block_4) ).
cnf(u2184,hypothesis,
~ object(block_7,s(time_0)) ).
cnf(u2203,hypothesis,
( ~ on(block_4,X1,X2)
| ~ nonfixed(X0)
| ~ neq(block_4,X0)
| ~ neq(X1,X0)
| ~ nonfixed(X1)
| ~ neq(block_4,X1)
| ~ on(X0,X1,X2) ) ).
cnf(u5776,hypothesis,
~ destination(block_8,s(s(time_0))) ).
cnf(u10810,hypothesis,
( ~ object(X0,s(s(s(s(time_0)))))
| ~ on(X0,table,s(s(s(s(s(time_0))))))
| ~ neq(X0,table)
| ~ nonfixed(X0) ) ).
cnf(u417,hypothesis,
neq(block_4,block_9) ).
cnf(u404,hypothesis,
neq(block_2,block_9) ).
cnf(u3373,hypothesis,
~ on(block_6,block_7,s(s(s(time_0)))) ).
cnf(u1334,hypothesis,
~ destination(block_1,s(s(s(s(time_0))))) ).
cnf(u6010,hypothesis,
~ object(block_4,s(s(time_0))) ).
cnf(u1949,hypothesis,
( ~ on(block_7,X2,X1)
| ~ a_block(X0)
| ~ neq(block_7,X0)
| ~ neq(X2,X0)
| ~ a_block(X2)
| ~ neq(block_7,X2)
| ~ on(block_7,X0,X1) ) ).
cnf(u423,hypothesis,
neq(block_5,table) ).
cnf(u9265,hypothesis,
~ on(block_1,block_2,s(s(s(s(s(time_0)))))) ).
cnf(u1947,hypothesis,
( ~ on(block_5,X2,X1)
| ~ a_block(X0)
| ~ neq(block_5,X0)
| ~ neq(X2,X0)
| ~ a_block(X2)
| ~ neq(block_5,X2)
| ~ on(block_5,X0,X1) ) ).
cnf(u1338,hypothesis,
( ~ nonfixed(X0)
| source(X0,s(s(time_0)))
| clear(X0,s(s(time_0)))
| ~ clear(X0,s(s(s(time_0)))) ) ).
cnf(u2207,hypothesis,
( ~ on(block_8,X1,X2)
| ~ nonfixed(X0)
| ~ neq(block_8,X0)
| ~ neq(X1,X0)
| ~ nonfixed(X1)
| ~ neq(block_8,X1)
| ~ on(X0,X1,X2) ) ).
cnf(u666,hypothesis,
~ object(block_4,s(s(s(s(s(s(time_0))))))) ).
cnf(u9871,hypothesis,
( ~ on(block_3,X0,s(s(s(s(time_0)))))
| ~ neq(block_3,X0)
| ~ neq(block_5,X0)
| ~ a_block(X0) ) ).
cnf(u189,hypothesis,
different(block_2,table) ).
cnf(u421,hypothesis,
neq(block_5,block_8) ).
cnf(u2869,hypothesis,
( ~ on(X0,block_6,s(s(time_0)))
| ~ neq(block_7,X0)
| ~ neq(block_6,X0)
| ~ nonfixed(X0) ) ).
cnf(u444,hypothesis,
( clear(block_2,X0)
| ~ destination(block_2,X0) ) ).
cnf(u10331,hypothesis,
( ~ on(block_8,X0,s(s(s(s(s(s(s(time_0))))))))
| ~ neq(block_8,X0)
| ~ neq(block_2,X0)
| ~ a_block(X0) ) ).
cnf(u1336,hypothesis,
~ destination(block_2,s(s(s(s(time_0))))) ).
cnf(u5777,hypothesis,
( ~ object(X0,s(s(time_0)))
| ~ neq(X0,block_8)
| ~ nonfixed(X0) ) ).
cnf(u6024,hypothesis,
on(block_9,block_8,s(time_0)) ).
cnf(u179,hypothesis,
different(block_1,block_8) ).
cnf(u2368,hypothesis,
~ neq(block_3,block_3) ).
cnf(u335,hypothesis,
( ~ fixed(X0)
| ~ on(X0,block_2,X1) ) ).
cnf(u9914,hypothesis,
( ~ object(X0,s(s(s(s(s(s(time_0)))))))
| ~ on(X0,table,s(s(s(s(s(s(s(time_0))))))))
| ~ neq(X0,table)
| ~ nonfixed(X0) ) ).
cnf(u434,hypothesis,
( clear(block_1,X0)
| ~ destination(block_1,X0) ) ).
cnf(u10171,hypothesis,
( ~ on(block_3,X0,s(s(time_0)))
| ~ neq(block_3,X0)
| ~ neq(block_5,X0)
| ~ a_block(X0) ) ).
cnf(u8398,hypothesis,
( ~ on(X0,block_4,s(s(time_0)))
| ~ neq(block_5,X0)
| ~ neq(block_4,X0)
| ~ nonfixed(X0) ) ).
cnf(u177,hypothesis,
different(block_1,block_6) ).
cnf(u7045,hypothesis,
( ~ on(block_4,X0,s(s(s(s(s(s(time_0)))))))
| ~ neq(block_4,X0)
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u333,hypothesis,
( ~ fixed(X0)
| ~ on(X0,block_4,X1) ) ).
cnf(u432,hypothesis,
neq(block_8,table) ).
cnf(u1215,hypothesis,
( ~ destination(X1,s(s(s(s(time_0)))))
| ~ object(X0,s(s(s(s(time_0)))))
| on(X0,X1,s(s(s(s(s(time_0))))))
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u206,hypothesis,
different(block_5,block_9) ).
cnf(u2880,hypothesis,
~ destination(block_6,s(s(time_0))) ).
cnf(u2870,hypothesis,
~ on(block_6,block_7,s(s(time_0))) ).
cnf(u1372,hypothesis,
~ destination(block_2,time_0) ).
cnf(u461,hypothesis,
( ~ on(block_9,X0,X1)
| ~ nonfixed(X0)
| ~ clear(X0,X1) ) ).
cnf(u712,hypothesis,
~ object(block_4,s(s(s(s(s(time_0)))))) ).
cnf(u346,hypothesis,
neq(block_4,block_1) ).
cnf(u676,hypothesis,
~ destination(block_8,s(s(s(s(s(s(time_0))))))) ).
cnf(u204,hypothesis,
different(block_5,block_7) ).
cnf(u10172,hypothesis,
( ~ on(X0,block_5,s(s(time_0)))
| ~ neq(block_3,X0)
| ~ neq(block_5,X0)
| ~ nonfixed(X0) ) ).
cnf(u9027,hypothesis,
~ on(block_5,block_9,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u4685,hypothesis,
on(block_8,block_7,s(time_0)) ).
cnf(u1500,hypothesis,
( ~ destination(X0,s(s(s(time_0))))
| ~ clear(X0,s(s(s(s(time_0)))))
| ~ nonfixed(X0) ) ).
cnf(u451,hypothesis,
( clear(block_9,X0)
| ~ destination(block_9,X0) ) ).
cnf(u344,hypothesis,
neq(block_2,block_1) ).
cnf(u474,hypothesis,
( ~ on(X0,X1,s(time_0))
| object(X0,s(time_0))
| on(X0,X1,s(s(time_0)))
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u194,hypothesis,
different(block_3,block_8) ).
cnf(u2930,hypothesis,
on(block_4,table,s(time_0)) ).
cnf(u217,hypothesis,
different(block_9,table) ).
cnf(u363,hypothesis,
neq(block_6,block_3) ).
cnf(u716,hypothesis,
~ object(block_7,s(s(s(s(s(time_0)))))) ).
cnf(u350,hypothesis,
neq(block_8,block_1) ).
cnf(u6914,hypothesis,
( ~ destination(table,X1)
| ~ a_block(X0)
| ~ neq(table,X0)
| ~ destination(X0,X1) ) ).
cnf(u472,hypothesis,
( ~ destination(X1,s(time_0))
| ~ object(X0,s(time_0))
| on(X0,X1,s(s(time_0)))
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u7613,hypothesis,
~ destination(block_5,s(s(s(time_0)))) ).
cnf(u1379,hypothesis,
~ object(block_7,time_0) ).
cnf(u4725,hypothesis,
( ~ on(X0,block_7,s(s(time_0)))
| ~ neq(block_8,X0)
| ~ neq(block_7,X0)
| ~ nonfixed(X0) ) ).
cnf(u9667,hypothesis,
( ~ object(X0,s(s(s(s(s(time_0))))))
| on(X0,block_5,s(s(s(s(s(time_0))))))
| ~ neq(X0,block_5)
| ~ nonfixed(X0) ) ).
cnf(u849,hypothesis,
~ destination(block_2,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u2010,hypothesis,
( ~ on(block_4,X0,time_0)
| ~ neq(block_4,X0)
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u361,hypothesis,
neq(block_4,block_3) ).
cnf(u256,hypothesis,
clear(block_9,time_0) ).
cnf(u2016,hypothesis,
( ~ on(block_3,X0,time_0)
| ~ neq(block_3,X0)
| ~ neq(block_2,X0)
| ~ a_block(X0) ) ).
cnf(u234,hypothesis,
nonfixed(block_6) ).
cnf(u515,hypothesis,
~ clear(block_1,time_0) ).
cnf(u750,hypothesis,
( clear(X0,s(s(s(s(s(s(s(time_0))))))))
| destination(X0,s(s(s(s(s(s(time_0)))))))
| ~ clear(X0,s(s(s(s(s(s(time_0)))))))
| ~ nonfixed(X0) ) ).
cnf(u4050,hypothesis,
( ~ on(block_4,X0,s(s(s(s(time_0)))))
| ~ neq(block_4,X0)
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u6911,hypothesis,
( ~ destination(block_7,X1)
| ~ a_block(X0)
| ~ neq(block_7,X0)
| ~ destination(X0,X1) ) ).
cnf(u4153,hypothesis,
( ~ on(X0,block_1,s(time_0))
| ~ neq(block_2,X0)
| ~ neq(block_1,X0)
| ~ nonfixed(X0) ) ).
cnf(u7023,hypothesis,
( ~ time(X1)
| ~ neq(block_8,X0)
| ~ destination(X0,X1)
| object(block_3,X1)
| object(block_4,X1)
| object(block_5,X1)
| object(block_6,X1)
| object(block_7,X1)
| object(block_8,X1)
| object(block_1,X1)
| ~ a_block(X0)
| destination(block_2,X1)
| destination(block_3,X1)
| destination(block_4,X1)
| destination(block_5,X1)
| destination(block_6,X1)
| destination(block_7,X1)
| object(block_2,X1)
| destination(block_1,X1)
| destination(table,X1) ) ).
cnf(u9947,hypothesis,
( ~ object(X0,time_0)
| on(X0,block_5,s(time_0))
| ~ neq(X0,block_5)
| ~ nonfixed(X0) ) ).
cnf(u8641,hypothesis,
( ~ on(X0,block_8,s(s(s(s(s(s(time_0)))))))
| ~ neq(block_7,X0)
| ~ neq(block_8,X0)
| ~ nonfixed(X0) ) ).
cnf(u232,hypothesis,
nonfixed(block_4) ).
cnf(u6913,hypothesis,
( ~ destination(block_9,X1)
| ~ a_block(X0)
| ~ neq(block_9,X0)
| ~ destination(X0,X1) ) ).
cnf(u2073,hypothesis,
( ~ on(block_8,X0,time_0)
| ~ a_block(X0)
| ~ neq(block_8,X0)
| on(block_8,X0,s(time_0)) ) ).
cnf(u2190,hypothesis,
~ object(block_8,s(time_0)) ).
cnf(u4096,hypothesis,
on(block_4,table,s(s(s(s(s(s(time_0))))))) ).
cnf(u273,axiom,
( ~ source(X2,X0)
| ~ time(X0)
| ~ object(X1,X0)
| ~ on(X1,X2,s(X0))
| ~ a_block(X2)
| ~ neq(X1,X2)
| ~ nonfixed(X1) ) ).
cnf(u2994,hypothesis,
~ object(block_5,s(s(time_0))) ).
cnf(u633,hypothesis,
~ object(block_6,s(s(s(s(s(s(time_0))))))) ).
cnf(u390,hypothesis,
neq(block_1,block_3) ).
cnf(u8687,hypothesis,
~ on(block_5,block_3,s(s(time_0))) ).
cnf(u4341,hypothesis,
( ~ object(X0,time_0)
| ~ neq(X0,block_3)
| ~ nonfixed(X0) ) ).
cnf(u519,hypothesis,
~ clear(block_6,time_0) ).
cnf(u2050,hypothesis,
( ~ source(X0,time_0)
| clear(X0,s(time_0))
| ~ nonfixed(X0) ) ).
cnf(u10277,hypothesis,
( ~ on(block_9,X0,s(s(s(s(time_0)))))
| ~ neq(block_9,X0)
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u2187,hypothesis,
~ object(block_4,s(time_0)) ).
cnf(u4502,hypothesis,
~ object(block_4,s(s(s(time_0)))) ).
cnf(u10755,hypothesis,
( ~ on(X0,block_7,s(s(s(s(s(time_0))))))
| ~ neq(block_6,X0)
| ~ neq(block_7,X0)
| ~ nonfixed(X0) ) ).
cnf(u279,axiom,
( ~ time(X0)
| ~ clear(X1,s(X0))
| ~ destination(X1,X0)
| ~ nonfixed(X1) ) ).
cnf(u401,hypothesis,
neq(block_2,block_6) ).
cnf(u388,hypothesis,
neq(table,block_9) ).
cnf(u9859,hypothesis,
( ~ on(X0,block_5,s(s(s(s(s(time_0))))))
| ~ neq(block_3,X0)
| ~ neq(block_5,X0)
| ~ nonfixed(X0) ) ).
cnf(u2337,hypothesis,
~ object(block_7,s(s(time_0))) ).
cnf(u6907,hypothesis,
( ~ destination(block_3,X1)
| ~ a_block(X0)
| ~ neq(block_3,X0)
| ~ destination(X0,X1) ) ).
cnf(u277,axiom,
( ~ time(X0)
| clear(X1,s(X0))
| destination(X1,X0)
| ~ clear(X1,X0)
| ~ nonfixed(X1) ) ).
cnf(u528,hypothesis,
( ~ destination(X1,s(s(s(s(s(time_0))))))
| ~ object(X0,s(s(s(s(s(time_0))))))
| on(X0,X1,s(s(s(s(s(s(time_0)))))))
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u407,hypothesis,
neq(block_3,block_5) ).
cnf(u2074,hypothesis,
( ~ on(block_7,X0,time_0)
| ~ a_block(X0)
| ~ neq(block_7,X0)
| on(block_7,X0,s(time_0)) ) ).
cnf(u2201,hypothesis,
( ~ on(block_2,X1,X2)
| ~ nonfixed(X0)
| ~ neq(block_2,X0)
| ~ neq(X1,X0)
| ~ nonfixed(X1)
| ~ neq(block_2,X1)
| ~ on(X0,X1,X2) ) ).
cnf(u10033,hypothesis,
( ~ on(block_6,X0,s(s(time_0)))
| ~ neq(block_6,X0)
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u173,hypothesis,
different(block_1,block_2) ).
cnf(u405,hypothesis,
neq(block_2,table) ).
cnf(u1951,hypothesis,
( ~ on(block_9,X2,X1)
| ~ a_block(X0)
| ~ neq(block_9,X0)
| ~ neq(X2,X0)
| ~ a_block(X2)
| ~ neq(block_9,X2)
| ~ on(block_9,X0,X1) ) ).
cnf(u2202,hypothesis,
( ~ on(block_3,X1,X2)
| ~ nonfixed(X0)
| ~ neq(block_3,X0)
| ~ neq(X1,X0)
| ~ nonfixed(X1)
| ~ neq(block_3,X1)
| ~ on(X0,X1,X2) ) ).
cnf(u428,hypothesis,
neq(block_7,block_8) ).
cnf(u9877,hypothesis,
~ destination(block_6,s(s(s(s(time_0))))) ).
cnf(u7577,hypothesis,
~ object(block_5,s(s(s(s(time_0))))) ).
cnf(u447,hypothesis,
( clear(block_8,X0)
| ~ destination(block_8,X0) ) ).
cnf(u9401,hypothesis,
( ~ on(X0,block_1,s(s(s(s(s(s(time_0)))))))
| ~ neq(block_2,X0)
| ~ neq(block_1,X0)
| ~ nonfixed(X0) ) ).
cnf(u418,hypothesis,
neq(block_4,table) ).
cnf(u190,hypothesis,
different(block_3,block_4) ).
cnf(u2864,hypothesis,
~ clear(block_6,s(s(time_0))) ).
cnf(u8559,hypothesis,
~ on(block_8,block_7,s(s(s(s(s(time_0)))))) ).
cnf(u9012,hypothesis,
~ fixed(block_9) ).
cnf(u10409,hypothesis,
( ~ on(block_9,X0,s(s(s(s(s(s(s(time_0))))))))
| ~ neq(block_9,X0)
| ~ neq(block_5,X0)
| ~ a_block(X0) ) ).
cnf(u445,hypothesis,
( clear(block_2,X0)
| ~ object(block_2,X0) ) ).
cnf(u8558,hypothesis,
( ~ on(X0,block_8,s(s(s(s(s(time_0))))))
| ~ neq(block_7,X0)
| ~ neq(block_8,X0)
| ~ nonfixed(X0) ) ).
cnf(u416,hypothesis,
neq(block_4,block_8) ).
cnf(u1337,hypothesis,
~ object(block_2,s(s(s(s(time_0))))) ).
cnf(u188,hypothesis,
different(block_2,block_9) ).
cnf(u4726,hypothesis,
~ on(block_7,block_8,s(s(time_0))) ).
cnf(u9860,hypothesis,
~ on(block_5,block_3,s(s(s(s(s(time_0)))))) ).
cnf(u435,hypothesis,
( clear(block_1,X0)
| ~ object(block_1,X0) ) ).
cnf(u330,hypothesis,
~ on(block_3,block_3,X0) ).
cnf(u178,hypothesis,
different(block_1,block_7) ).
cnf(u846,hypothesis,
~ object(block_8,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u2899,hypothesis,
( ~ on(X0,block_4,s(time_0))
| ~ neq(block_5,X0)
| ~ neq(block_4,X0)
| ~ nonfixed(X0) ) ).
cnf(u9404,hypothesis,
on(block_2,block_1,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u10471,hypothesis,
( ~ on(X0,block_7,s(s(s(s(s(s(time_0)))))))
| ~ neq(block_6,X0)
| ~ neq(block_7,X0)
| ~ nonfixed(X0) ) ).
cnf(u10135,hypothesis,
( ~ on(X0,block_5,s(time_0))
| ~ neq(block_3,X0)
| ~ neq(block_5,X0)
| ~ nonfixed(X0) ) ).
cnf(u328,hypothesis,
~ on(block_5,block_5,X0) ).
cnf(u8536,hypothesis,
( ~ on(block_7,X0,s(s(s(s(time_0)))))
| ~ neq(block_7,X0)
| ~ neq(block_8,X0)
| ~ a_block(X0) ) ).
cnf(u458,hypothesis,
( ~ on(block_6,X0,X1)
| ~ nonfixed(X0)
| ~ clear(X0,X1) ) ).
cnf(u9727,hypothesis,
( ~ object(X0,s(s(s(s(s(s(time_0)))))))
| on(X0,block_5,s(s(s(s(s(s(s(time_0))))))))
| ~ neq(X0,block_5)
| ~ nonfixed(X0) ) ).
cnf(u1373,hypothesis,
~ object(block_2,time_0) ).
cnf(u2186,hypothesis,
~ destination(block_4,s(time_0)) ).
cnf(u201,hypothesis,
different(block_4,block_9) ).
cnf(u9911,hypothesis,
( ~ object(X0,s(s(s(s(s(s(time_0)))))))
| on(X0,table,s(s(s(s(s(s(time_0)))))))
| ~ neq(X0,table)
| ~ nonfixed(X0) ) ).
cnf(u347,hypothesis,
neq(block_5,block_1) ).
cnf(u334,hypothesis,
~ on(block_2,block_2,X0) ).
cnf(u456,hypothesis,
( ~ on(block_4,X0,X1)
| ~ nonfixed(X0)
| ~ clear(X0,X1) ) ).
cnf(u8872,hypothesis,
( ~ on(block_1,X0,s(s(s(s(s(s(time_0)))))))
| ~ neq(block_1,X0)
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u10427,hypothesis,
( ~ on(X0,block_6,s(s(s(s(s(s(s(time_0))))))))
| ~ neq(block_3,X0)
| ~ neq(block_6,X0)
| ~ nonfixed(X0) ) ).
cnf(u1501,hypothesis,
( ~ object(X0,s(s(s(time_0))))
| on(X0,X1,s(s(s(s(time_0)))))
| ~ destination(X1,s(s(s(time_0))))
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u207,hypothesis,
different(block_5,table) ).
cnf(u10534,hypothesis,
( ~ object(X0,s(s(time_0)))
| on(X0,block_7,s(s(time_0)))
| ~ neq(X0,block_7)
| ~ nonfixed(X0) ) ).
cnf(u345,hypothesis,
neq(block_3,block_1) ).
cnf(u10470,hypothesis,
( ~ on(block_6,X0,s(s(s(s(s(s(time_0)))))))
| ~ neq(block_6,X0)
| ~ neq(block_7,X0)
| ~ a_block(X0) ) ).
cnf(u8874,hypothesis,
on(block_1,table,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u368,hypothesis,
neq(block_5,block_4) ).
cnf(u462,hypothesis,
~ on(table,block_2,X0) ).
cnf(u1383,hypothesis,
( ~ destination(X0,s(s(s(s(time_0)))))
| ~ clear(X0,s(s(s(s(s(time_0))))))
| ~ nonfixed(X0) ) ).
cnf(u218,hypothesis,
a_block(block_1) ).
cnf(u5185,hypothesis,
( ~ on(block_7,X0,s(s(s(time_0))))
| ~ neq(block_7,X0)
| ~ neq(block_6,X0)
| ~ a_block(X0) ) ).
cnf(u4724,hypothesis,
( ~ on(block_8,X0,s(s(time_0)))
| ~ neq(block_8,X0)
| ~ neq(block_7,X0)
| ~ a_block(X0) ) ).
cnf(u473,hypothesis,
( ~ on(X0,X1,s(s(time_0)))
| object(X0,s(time_0))
| on(X0,X1,s(time_0))
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u374,hypothesis,
neq(block_6,block_5) ).
cnf(u10160,hypothesis,
( ~ on(block_6,X0,s(s(s(s(time_0)))))
| ~ neq(block_6,X0)
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u216,hypothesis,
different(block_8,table) ).
cnf(u2530,hypothesis,
~ on(block_6,block_7,s(time_0)) ).
cnf(u1649,hypothesis,
~ object(block_1,s(s(s(time_0)))) ).
cnf(u247,hypothesis,
( object(block_9,X0)
| object(block_2,X0)
| object(block_3,X0)
| object(block_4,X0)
| object(block_5,X0)
| object(block_6,X0)
| object(block_7,X0)
| object(block_8,X0)
| object(block_1,X0)
| ~ time(X0) ) ).
cnf(u257,hypothesis,
on(block_8,block_7,time_0) ).
cnf(u524,hypothesis,
( ~ nonfixed(X0)
| source(X0,s(s(s(s(s(time_0))))))
| clear(X0,s(s(s(s(s(time_0))))))
| ~ clear(X0,s(s(s(s(s(s(time_0))))))) ) ).
cnf(u372,hypothesis,
neq(block_9,block_4) ).
cnf(u1809,hypothesis,
~ on(table,block_9,s(s(s(s(s(s(time_0))))))) ).
cnf(u10537,hypothesis,
( ~ on(X0,block_7,s(s(s(time_0))))
| ~ object(X0,s(s(time_0)))
| ~ neq(X0,block_7)
| ~ nonfixed(X0) ) ).
cnf(u4860,hypothesis,
~ destination(block_3,s(s(s(s(s(time_0)))))) ).
cnf(u245,hypothesis,
( ~ time(X0)
| source(block_2,X0)
| source(block_3,X0)
| source(block_4,X0)
| source(block_5,X0)
| source(block_6,X0)
| source(block_7,X0)
| source(block_8,X0)
| source(block_9,X0)
| source(table,X0)
| source(block_1,X0) ) ).
cnf(u263,axiom,
( ~ nonfixed(X1)
| ~ on(X1,X3,X0)
| ~ a_block(X3)
| ~ neq(X1,X3)
| ~ neq(X2,X3)
| ~ a_block(X2)
| ~ neq(X1,X2)
| ~ on(X1,X2,X0) ) ).
cnf(u385,hypothesis,
neq(table,block_7) ).
cnf(u745,hypothesis,
~ destination(block_1,s(s(s(s(s(time_0)))))) ).
cnf(u500,hypothesis,
~ on(block_2,block_3,time_0) ).
cnf(u3977,hypothesis,
( ~ on(block_4,X0,s(s(time_0)))
| ~ neq(block_4,X0)
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u9555,hypothesis,
on(block_8,block_2,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u391,hypothesis,
neq(block_1,block_4) ).
cnf(u529,hypothesis,
( ~ on(X0,X1,s(s(s(s(s(s(time_0)))))))
| object(X0,s(s(s(s(s(time_0))))))
| on(X0,X1,s(s(s(s(s(time_0))))))
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u284,axiom,
( ~ nonfixed(X1)
| ~ object(X1,X0)
| clear(X1,X0) ) ).
cnf(u2343,hypothesis,
~ object(block_1,s(s(time_0))) ).
cnf(u10536,hypothesis,
( ~ source(X0,s(s(time_0)))
| ~ a_block(X0)
| ~ neq(block_7,X0) ) ).
cnf(u9531,hypothesis,
( ~ on(block_8,X0,s(s(s(s(s(time_0))))))
| ~ neq(block_8,X0)
| ~ neq(block_2,X0)
| ~ a_block(X0) ) ).
cnf(u2336,hypothesis,
~ destination(block_7,s(s(time_0))) ).
cnf(u389,hypothesis,
neq(block_1,block_2) ).
cnf(u274,axiom,
( ~ object(X1,X0)
| ~ destination(X1,X0)
| ~ nonfixed(X1) ) ).
cnf(u412,hypothesis,
neq(block_3,table) ).
cnf(u6910,hypothesis,
( ~ destination(block_6,X1)
| ~ a_block(X0)
| ~ neq(block_6,X0)
| ~ destination(X0,X1) ) ).
cnf(u8442,hypothesis,
( ~ on(block_5,X0,s(s(s(s(s(time_0))))))
| ~ neq(block_5,X0)
| ~ neq(block_4,X0)
| ~ a_block(X0) ) ).
cnf(u3022,hypothesis,
~ destination(block_5,s(time_0)) ).
cnf(u2342,hypothesis,
~ destination(block_1,s(s(time_0))) ).
cnf(u431,hypothesis,
neq(block_8,block_9) ).
cnf(u5512,hypothesis,
~ fixed(block_3) ).
cnf(u9872,hypothesis,
( ~ on(X0,block_5,s(s(s(s(time_0)))))
| ~ neq(block_3,X0)
| ~ neq(block_5,X0)
| ~ nonfixed(X0) ) ).
cnf(u402,hypothesis,
neq(block_2,block_7) ).
cnf(u711,hypothesis,
~ destination(block_4,s(s(s(s(s(time_0)))))) ).
cnf(u174,hypothesis,
different(block_1,block_3) ).
cnf(u743,hypothesis,
~ destination(block_2,s(s(s(s(s(time_0)))))) ).
cnf(u2200,hypothesis,
( ~ on(block_1,X1,X2)
| ~ nonfixed(X0)
| ~ neq(block_1,X0)
| ~ neq(X1,X0)
| ~ nonfixed(X1)
| ~ neq(block_1,X1)
| ~ on(X0,X1,X2) ) ).
cnf(u6908,hypothesis,
( ~ destination(block_4,X1)
| ~ a_block(X0)
| ~ neq(block_4,X0)
| ~ destination(X0,X1) ) ).
cnf(u1340,hypothesis,
( ~ on(X0,X1,s(s(s(time_0))))
| destination(X1,s(s(time_0)))
| on(X0,X1,s(s(time_0)))
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u10053,hypothesis,
on(block_6,table,s(s(s(s(time_0))))) ).
cnf(u429,hypothesis,
neq(block_7,block_9) ).
cnf(u2231,hypothesis,
( ~ on(X0,block_7,time_0)
| ~ neq(block_8,X0)
| ~ neq(block_7,X0)
| ~ nonfixed(X0) ) ).
cnf(u400,hypothesis,
neq(block_2,block_5) ).
cnf(u172,hypothesis,
( ~ different(X1,X0)
| neq(X1,X0) ) ).
cnf(u1213,hypothesis,
( ~ on(X0,X1,s(s(s(s(s(time_0))))))
| destination(X1,s(s(s(s(time_0)))))
| on(X0,X1,s(s(s(s(time_0)))))
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u9517,hypothesis,
on(block_8,block_2,s(s(s(s(s(time_0)))))) ).
cnf(u187,hypothesis,
different(block_2,block_8) ).
cnf(u419,hypothesis,
neq(block_5,block_6) ).
cnf(u10134,hypothesis,
( ~ on(block_3,X0,s(time_0))
| ~ neq(block_3,X0)
| ~ neq(block_5,X0)
| ~ a_block(X0) ) ).
cnf(u442,hypothesis,
( clear(block_4,X0)
| ~ destination(block_4,X0) ) ).
cnf(u7614,hypothesis,
~ object(block_5,s(s(s(time_0)))) ).
cnf(u1344,hypothesis,
( ~ on(X0,X1,s(s(time_0)))
| object(X0,s(s(time_0)))
| on(X0,X1,s(s(s(time_0))))
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u185,hypothesis,
different(block_2,block_6) ).
cnf(u836,hypothesis,
~ object(block_6,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u701,hypothesis,
~ source(block_7,s(s(s(s(s(time_0)))))) ).
cnf(u440,hypothesis,
( clear(block_3,X0)
| ~ destination(block_3,X0) ) ).
cnf(u3757,hypothesis,
( ~ on(block_1,X0,s(s(time_0)))
| ~ neq(block_1,X0)
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u841,hypothesis,
~ destination(block_5,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u699,hypothesis,
~ object(block_7,s(s(s(s(s(s(time_0))))))) ).
cnf(u9669,hypothesis,
( ~ source(X0,s(s(s(s(s(time_0))))))
| ~ a_block(X0)
| ~ neq(block_5,X0) ) ).
cnf(u10333,hypothesis,
~ on(block_2,block_8,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u191,hypothesis,
different(block_3,block_5) ).
cnf(u8557,hypothesis,
( ~ on(block_7,X0,s(s(s(s(s(time_0))))))
| ~ neq(block_7,X0)
| ~ neq(block_8,X0)
| ~ a_block(X0) ) ).
cnf(u331,hypothesis,
( ~ on(X0,block_3,X1)
| ~ fixed(X0) ) ).
cnf(u5815,hypothesis,
( ~ on(block_6,X0,s(time_0))
| ~ neq(block_6,X0)
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u9494,hypothesis,
~ on(block_2,block_8,s(s(s(time_0)))) ).
cnf(u329,hypothesis,
( ~ on(X0,block_5,X1)
| ~ fixed(X0) ) ).
cnf(u459,hypothesis,
( ~ on(block_7,X0,X1)
| ~ nonfixed(X0)
| ~ clear(X0,X1) ) ).
cnf(u352,hypothesis,
neq(table,block_1) ).
cnf(u850,hypothesis,
~ object(block_2,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u845,hypothesis,
~ destination(block_8,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u202,hypothesis,
different(block_4,table) ).
cnf(u7656,hypothesis,
on(block_8,block_2,s(s(s(time_0)))) ).
cnf(u1629,hypothesis,
~ on(table,block_9,s(s(s(time_0)))) ).
cnf(u457,hypothesis,
( ~ on(block_5,X0,X1)
| ~ nonfixed(X0)
| ~ clear(X0,X1) ) ).
cnf(u9532,hypothesis,
( ~ on(X0,block_2,s(s(s(s(s(time_0))))))
| ~ neq(block_8,X0)
| ~ neq(block_2,X0)
| ~ nonfixed(X0) ) ).
cnf(u358,hypothesis,
neq(block_8,block_2) ).
cnf(u200,hypothesis,
different(block_4,block_8) ).
cnf(u2514,hypothesis,
on(block_7,block_6,s(time_0)) ).
cnf(u2241,hypothesis,
( ~ on(X0,block_1,time_0)
| ~ neq(block_2,X0)
| ~ neq(block_1,X0)
| ~ nonfixed(X0) ) ).
cnf(u2452,hypothesis,
( ~ on(block_1,X0,s(time_0))
| ~ neq(block_1,X0)
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u231,hypothesis,
nonfixed(block_3) ).
cnf(u369,hypothesis,
neq(block_6,block_4) ).
cnf(u463,hypothesis,
~ on(table,block_6,X0) ).
cnf(u356,hypothesis,
neq(block_6,block_2) ).
cnf(u1646,hypothesis,
~ destination(block_2,s(s(s(time_0)))) ).
cnf(u1378,hypothesis,
~ destination(block_7,time_0) ).
cnf(u1502,hypothesis,
( ~ on(X0,X1,s(s(s(s(time_0)))))
| object(X0,s(s(s(time_0))))
| on(X0,X1,s(s(s(time_0))))
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u229,hypothesis,
nonfixed(block_1) ).
cnf(u375,hypothesis,
neq(block_7,block_5) ).
cnf(u497,hypothesis,
~ on(block_7,block_8,time_0) ).
cnf(u729,hypothesis,
~ object(block_8,s(s(s(s(s(time_0)))))) ).
cnf(u5860,hypothesis,
~ on(block_4,block_5,s(s(s(time_0)))) ).
cnf(u240,hypothesis,
time(s(s(time_0))) ).
cnf(u9553,hypothesis,
~ on(block_2,block_8,s(s(s(s(s(s(time_0))))))) ).
cnf(u219,hypothesis,
a_block(block_2) ).
cnf(u373,hypothesis,
neq(table,block_4) ).
cnf(u503,hypothesis,
~ clear(block_8,time_0) ).
cnf(u2738,hypothesis,
~ destination(block_7,s(s(s(time_0)))) ).
cnf(u268,axiom,
( ~ source(X1,X0)
| ~ object(X1,X0)
| ~ nonfixed(X1) ) ).
cnf(u1667,hypothesis,
( ~ object(X0,X1)
| ~ neq(X0,block_9)
| ~ nonfixed(X0)
| object(block_2,X1)
| object(block_3,X1)
| object(block_4,X1)
| object(block_5,X1)
| object(block_6,X1)
| object(block_7,X1)
| object(block_8,X1)
| object(block_1,X1)
| ~ time(X1) ) ).
cnf(u10472,hypothesis,
~ on(block_7,block_6,s(s(s(s(s(s(time_0))))))) ).
cnf(u246,hypothesis,
( destination(block_9,X0)
| destination(block_2,X0)
| destination(block_3,X0)
| destination(block_4,X0)
| destination(block_5,X0)
| destination(block_6,X0)
| destination(block_7,X0)
| destination(block_8,X0)
| destination(block_1,X0)
| destination(table,X0)
| ~ time(X0) ) ).
cnf(u6909,hypothesis,
( ~ destination(block_5,X1)
| ~ a_block(X0)
| ~ neq(block_5,X0)
| ~ destination(X0,X1) ) ).
cnf(u2199,hypothesis,
~ object(block_6,s(time_0)) ).
cnf(u527,hypothesis,
( clear(X0,s(s(s(s(s(s(time_0)))))))
| destination(X0,s(s(s(s(s(time_0))))))
| ~ clear(X0,s(s(s(s(s(time_0))))))
| ~ nonfixed(X0) ) ).
cnf(u746,hypothesis,
~ object(block_1,s(s(s(s(s(time_0)))))) ).
cnf(u10487,hypothesis,
~ on(block_7,block_6,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u8443,hypothesis,
( ~ on(X0,block_4,s(s(s(s(s(time_0))))))
| ~ neq(block_5,X0)
| ~ neq(block_4,X0)
| ~ nonfixed(X0) ) ).
cnf(u8599,hypothesis,
~ on(block_4,block_5,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u501,hypothesis,
~ on(block_1,block_2,time_0) ).
cnf(u752,hypothesis,
( ~ on(X0,X1,s(s(s(s(s(s(s(time_0))))))))
| object(X0,s(s(s(s(s(s(time_0)))))))
| on(X0,X1,s(s(s(s(s(s(time_0)))))))
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u258,hypothesis,
on(block_7,block_6,time_0) ).
cnf(u396,hypothesis,
neq(block_1,block_9) ).
cnf(u244,hypothesis,
time(s(s(s(s(s(s(time_0))))))) ).
cnf(u2056,hypothesis,
( ~ nonfixed(X0)
| object(X0,time_0)
| ~ on(X0,X1,time_0)
| ~ a_block(X1)
| ~ neq(X0,X1)
| on(X0,X1,s(time_0)) ) ).
cnf(u530,hypothesis,
( ~ on(X0,X1,s(s(s(s(s(time_0))))))
| object(X0,s(s(s(s(s(time_0))))))
| on(X0,X1,s(s(s(s(s(s(time_0)))))))
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u5369,hypothesis,
~ on(block_6,block_3,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u285,axiom,
( ~ a_block(X1)
| ~ on(X1,X1,X0) ) ).
cnf(u415,hypothesis,
neq(block_4,block_7) ).
cnf(u2192,hypothesis,
~ destination(block_1,s(time_0)) ).
cnf(u6912,hypothesis,
( ~ destination(block_8,X1)
| ~ a_block(X0)
| ~ neq(block_8,X0)
| ~ destination(X0,X1) ) ).
cnf(u386,hypothesis,
neq(block_9,block_8) ).
cnf(u2441,hypothesis,
on(block_1,table,s(time_0)) ).
cnf(u1069,hypothesis,
~ object(block_8,time_0) ).
cnf(u6039,hypothesis,
( ~ on(X0,block_8,s(time_0))
| ~ neq(block_9,X0)
| ~ neq(block_8,X0)
| ~ nonfixed(X0) ) ).
cnf(u1945,hypothesis,
( ~ on(block_3,X2,X1)
| ~ a_block(X0)
| ~ neq(block_3,X0)
| ~ neq(X2,X0)
| ~ a_block(X2)
| ~ neq(block_3,X2)
| ~ on(block_3,X0,X1) ) ).
cnf(u275,axiom,
( ~ a_block(X1)
| ~ destination(X2,X0)
| ~ a_block(X2)
| ~ neq(X1,X2)
| ~ destination(X1,X0) ) ).
cnf(u413,hypothesis,
neq(block_4,block_5) ).
cnf(u9263,hypothesis,
( ~ on(block_2,X0,s(s(s(s(s(time_0))))))
| ~ neq(block_2,X0)
| ~ neq(block_1,X0)
| ~ a_block(X0) ) ).
cnf(u7565,hypothesis,
( ~ destination(X0,s(s(s(time_0))))
| ~ neq(block_8,X0)
| ~ a_block(X0) ) ).
cnf(u384,hypothesis,
neq(block_9,block_7) ).
cnf(u8561,hypothesis,
on(block_7,block_8,s(s(s(s(s(s(time_0))))))) ).
cnf(u7556,hypothesis,
( ~ object(X0,s(s(s(s(time_0)))))
| on(X0,block_7,s(s(s(s(s(time_0))))))
| ~ neq(X0,block_7)
| ~ nonfixed(X0) ) ).
cnf(u171,hypothesis,
( ~ different(X0,X1)
| neq(X1,X0) ) ).
cnf(u403,hypothesis,
neq(block_2,block_8) ).
cnf(u2208,hypothesis,
( ~ on(block_9,X1,X2)
| ~ nonfixed(X0)
| ~ neq(block_9,X0)
| ~ neq(X1,X0)
| ~ nonfixed(X1)
| ~ neq(block_9,X1)
| ~ on(X0,X1,X2) ) ).
cnf(u426,hypothesis,
neq(block_6,block_9) ).
cnf(u1341,hypothesis,
( clear(X0,s(s(s(time_0))))
| destination(X0,s(s(time_0)))
| ~ clear(X0,s(s(time_0)))
| ~ nonfixed(X0) ) ).
cnf(u6040,hypothesis,
~ on(block_8,block_9,s(time_0)) ).
cnf(u4138,hypothesis,
on(block_2,block_1,s(time_0)) ).
cnf(u1214,hypothesis,
( clear(X0,s(s(s(s(s(time_0))))))
| destination(X0,s(s(s(s(time_0)))))
| ~ clear(X0,s(s(s(s(time_0)))))
| ~ nonfixed(X0) ) ).
cnf(u668,hypothesis,
~ source(block_4,s(s(s(s(s(time_0)))))) ).
cnf(u10215,hypothesis,
( ~ on(block_9,X0,s(s(time_0)))
| ~ neq(block_9,X0)
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u424,hypothesis,
neq(block_6,block_7) ).
cnf(u9535,hypothesis,
on(block_8,block_2,s(s(s(s(s(s(time_0))))))) ).
cnf(u1331,hypothesis,
~ object(block_8,s(s(s(s(time_0))))) ).
cnf(u2237,hypothesis,
( ~ on(X0,block_6,time_0)
| ~ neq(block_7,X0)
| ~ neq(block_6,X0)
| ~ nonfixed(X0) ) ).
cnf(u9400,hypothesis,
( ~ on(block_2,X0,s(s(s(s(s(s(time_0)))))))
| ~ neq(block_2,X0)
| ~ neq(block_1,X0)
| ~ a_block(X0) ) ).
cnf(u839,hypothesis,
~ destination(block_4,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u175,hypothesis,
different(block_1,block_4) ).
cnf(u1212,hypothesis,
( ~ source(X0,s(s(s(s(time_0)))))
| clear(X0,s(s(s(s(s(time_0))))))
| ~ nonfixed(X0) ) ).
cnf(u443,hypothesis,
( clear(block_4,X0)
| ~ object(block_4,X0) ) ).
cnf(u430,hypothesis,
neq(block_7,table) ).
cnf(u186,hypothesis,
different(block_2,block_7) ).
cnf(u1345,hypothesis,
~ destination(block_6,time_0) ).
cnf(u5196,hypothesis,
( ~ object(X0,s(s(s(time_0))))
| ~ neq(X0,block_7)
| ~ nonfixed(X0) ) ).
cnf(u2228,hypothesis,
( ~ on(X0,block_4,time_0)
| ~ neq(block_5,X0)
| ~ neq(block_4,X0)
| ~ nonfixed(X0) ) ).
cnf(u5319,hypothesis,
~ on(block_6,block_3,s(s(s(s(s(s(time_0))))))) ).
cnf(u10058,hypothesis,
( ~ object(X0,s(time_0))
| on(X0,table,s(s(time_0)))
| ~ neq(X0,table)
| ~ nonfixed(X0) ) ).
cnf(u441,hypothesis,
( clear(block_3,X0)
| ~ object(block_3,X0) ) ).
cnf(u336,hypothesis,
~ on(table,table,X0) ).
cnf(u184,hypothesis,
different(block_2,block_5) ).
cnf(u6849,hypothesis,
( ~ source(X0,time_0)
| ~ a_block(X0)
| ~ neq(block_2,X0) ) ).
cnf(u4422,hypothesis,
~ destination(block_6,s(s(s(time_0)))) ).
cnf(u1216,hypothesis,
( ~ on(X0,X1,s(s(s(s(s(time_0))))))
| object(X0,s(s(s(s(time_0)))))
| on(X0,X1,s(s(s(s(time_0)))))
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u10186,hypothesis,
( ~ on(X0,block_5,s(s(s(time_0))))
| ~ neq(block_3,X0)
| ~ neq(block_5,X0)
| ~ nonfixed(X0) ) ).
cnf(u8537,hypothesis,
( ~ on(X0,block_8,s(s(s(s(time_0)))))
| ~ neq(block_7,X0)
| ~ neq(block_8,X0)
| ~ nonfixed(X0) ) ).
cnf(u2881,hypothesis,
~ object(block_6,s(s(time_0))) ).
cnf(u6084,hypothesis,
~ neq(block_1,block_1) ).
cnf(u4803,hypothesis,
~ neq(block_5,block_5) ).
cnf(u342,hypothesis,
~ on(block_9,block_9,X0) ).
cnf(u9551,hypothesis,
( ~ on(block_8,X0,s(s(s(s(s(s(time_0)))))))
| ~ neq(block_8,X0)
| ~ neq(block_2,X0)
| ~ a_block(X0) ) ).
cnf(u842,hypothesis,
~ object(block_5,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u1371,hypothesis,
~ object(block_1,time_0) ).
cnf(u1648,hypothesis,
~ destination(block_1,s(s(s(time_0)))) ).
cnf(u8397,hypothesis,
( ~ on(block_5,X0,s(s(time_0)))
| ~ neq(block_5,X0)
| ~ neq(block_4,X0)
| ~ a_block(X0) ) ).
cnf(u215,hypothesis,
different(block_8,block_9) ).
cnf(u353,hypothesis,
neq(block_3,block_2) ).
cnf(u10035,hypothesis,
on(block_6,table,s(s(s(time_0)))) ).
cnf(u340,hypothesis,
~ on(block_6,block_6,X0) ).
cnf(u470,hypothesis,
( ~ on(X0,X1,s(s(time_0)))
| destination(X1,s(time_0))
| on(X0,X1,s(time_0))
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u2198,hypothesis,
~ destination(block_6,s(time_0)) ).
cnf(u8458,hypothesis,
( ~ on(X0,block_4,s(s(s(s(s(s(time_0)))))))
| ~ neq(block_5,X0)
| ~ neq(block_4,X0)
| ~ nonfixed(X0) ) ).
cnf(u3023,hypothesis,
~ object(block_5,s(time_0)) ).
cnf(u1499,hypothesis,
( clear(X0,s(s(s(s(time_0)))))
| destination(X0,s(s(s(time_0))))
| ~ clear(X0,s(s(s(time_0))))
| ~ nonfixed(X0) ) ).
cnf(u9533,hypothesis,
~ on(block_2,block_8,s(s(s(s(s(time_0)))))) ).
cnf(u213,hypothesis,
different(block_7,block_9) ).
cnf(u1998,hypothesis,
( ~ on(block_6,X0,time_0)
| ~ neq(block_6,X0)
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u359,hypothesis,
neq(block_9,block_2) ).
cnf(u9946,hypothesis,
( ~ destination(X0,time_0)
| ~ neq(block_5,X0)
| ~ a_block(X0) ) ).
cnf(u2004,hypothesis,
( ~ on(block_1,X0,time_0)
| ~ neq(block_1,X0)
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u468,hypothesis,
( ~ nonfixed(X0)
| source(X0,s(time_0))
| clear(X0,s(time_0))
| ~ clear(X0,s(s(time_0))) ) ).
cnf(u4325,hypothesis,
~ on(block_1,block_2,s(s(time_0))) ).
cnf(u224,hypothesis,
a_block(block_7) ).
cnf(u2052,hypothesis,
( clear(X0,s(time_0))
| destination(X0,time_0)
| ~ clear(X0,time_0)
| ~ nonfixed(X0) ) ).
cnf(u203,hypothesis,
different(block_5,block_6) ).
cnf(u357,hypothesis,
neq(block_7,block_2) ).
cnf(u2941,hypothesis,
( ~ on(block_4,X0,s(time_0))
| ~ neq(block_4,X0)
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u380,hypothesis,
neq(block_8,block_6) ).
cnf(u1233,hypothesis,
~ on(table,block_9,s(s(s(s(time_0))))) ).
cnf(u230,hypothesis,
nonfixed(block_2) ).
cnf(u9493,hypothesis,
( ~ on(X0,block_2,s(s(s(time_0))))
| ~ neq(block_8,X0)
| ~ neq(block_2,X0)
| ~ nonfixed(X0) ) ).
cnf(u2049,hypothesis,
( ~ nonfixed(X0)
| source(X0,time_0)
| clear(X0,time_0)
| ~ clear(X0,s(time_0)) ) ).
cnf(u4349,hypothesis,
( ~ on(X0,block_2,s(time_0))
| ~ object(X0,time_0)
| ~ neq(X0,block_2)
| ~ nonfixed(X0) ) ).
cnf(u253,hypothesis,
clear(block_5,time_0) ).
cnf(u7003,hypothesis,
( ~ time(X1)
| ~ neq(block_9,X0)
| ~ destination(X0,X1)
| destination(block_2,X1)
| destination(block_3,X1)
| destination(block_4,X1)
| destination(block_5,X1)
| destination(block_6,X1)
| destination(block_7,X1)
| destination(block_8,X1)
| destination(block_1,X1)
| destination(table,X1)
| ~ a_block(X0) ) ).
cnf(u271,axiom,
( ~ source(X2,X0)
| ~ object(X1,X0)
| on(X1,X2,X0)
| ~ a_block(X2)
| ~ neq(X1,X2)
| ~ nonfixed(X1) ) ).
cnf(u9858,hypothesis,
( ~ on(block_3,X0,s(s(s(s(s(time_0))))))
| ~ neq(block_3,X0)
| ~ neq(block_5,X0)
| ~ a_block(X0) ) ).
cnf(u2031,hypothesis,
( ~ on(block_2,X0,time_0)
| ~ neq(block_2,X0)
| ~ neq(block_1,X0)
| ~ a_block(X0) ) ).
cnf(u370,hypothesis,
neq(block_7,block_4) ).
cnf(u753,hypothesis,
( ~ on(X0,X1,s(s(s(s(s(s(time_0)))))))
| object(X0,s(s(s(s(s(s(time_0)))))))
| on(X0,X1,s(s(s(s(s(s(s(time_0))))))))
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u8658,hypothesis,
( ~ on(block_7,X0,s(s(s(s(s(s(s(time_0))))))))
| ~ neq(block_7,X0)
| ~ neq(block_8,X0)
| ~ a_block(X0) ) ).
cnf(u7266,hypothesis,
( ~ on(X0,block_1,s(s(time_0)))
| ~ neq(block_2,X0)
| ~ neq(block_1,X0)
| ~ nonfixed(X0) ) ).
cnf(u228,hypothesis,
fixed(table) ).
cnf(u8660,hypothesis,
~ on(block_8,block_7,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u9492,hypothesis,
( ~ on(block_8,X0,s(s(s(time_0))))
| ~ neq(block_8,X0)
| ~ neq(block_2,X0)
| ~ a_block(X0) ) ).
cnf(u4340,hypothesis,
~ destination(block_3,time_0) ).
cnf(u243,hypothesis,
time(s(s(s(s(s(time_0)))))) ).
cnf(u269,axiom,
( ~ source(X1,X0)
| ~ source(X2,X0)
| ~ a_block(X2)
| ~ neq(X1,X2)
| ~ a_block(X1) ) ).
cnf(u399,hypothesis,
neq(block_2,block_4) ).
cnf(u9241,hypothesis,
~ destination(table,s(s(s(s(s(s(time_0))))))) ).
cnf(u2013,hypothesis,
( ~ on(block_7,X0,time_0)
| ~ neq(block_7,X0)
| ~ neq(block_6,X0)
| ~ a_block(X0) ) ).
cnf(u498,hypothesis,
~ on(block_6,block_7,time_0) ).
cnf(u6633,hypothesis,
~ on(block_4,block_5,s(s(s(s(s(s(time_0))))))) ).
cnf(u665,hypothesis,
~ destination(block_4,s(s(s(s(s(s(time_0))))))) ).
cnf(u10410,hypothesis,
( ~ on(X0,block_5,s(s(s(s(s(s(s(time_0))))))))
| ~ neq(block_9,X0)
| ~ neq(block_5,X0)
| ~ nonfixed(X0) ) ).
cnf(u241,hypothesis,
time(s(s(s(time_0)))) ).
cnf(u1020,hypothesis,
( ~ object(X0,s(s(s(s(s(time_0))))))
| on(X0,block_6,s(s(s(s(s(s(time_0)))))))
| ~ neq(X0,block_6)
| ~ nonfixed(X0) ) ).
cnf(u259,hypothesis,
on(block_6,table,time_0) ).
cnf(u397,hypothesis,
neq(block_1,table) ).
cnf(u1943,hypothesis,
( ~ on(block_1,X2,X1)
| ~ a_block(X0)
| ~ neq(block_1,X0)
| ~ neq(X2,X0)
| ~ a_block(X2)
| ~ neq(block_1,X2)
| ~ on(block_1,X0,X1) ) ).
cnf(u282,axiom,
( ~ time(X0)
| ~ on(X1,X2,s(X0))
| object(X1,X0)
| on(X1,X2,X0)
| ~ a_block(X2)
| ~ neq(X1,X2)
| ~ nonfixed(X1) ) ).
cnf(u496,hypothesis,
~ on(block_8,block_9,time_0) ).
cnf(u10806,hypothesis,
( ~ object(X0,s(s(s(s(time_0)))))
| on(X0,table,s(s(s(s(time_0)))))
| ~ neq(X0,table)
| ~ nonfixed(X0) ) ).
cnf(u8855,hypothesis,
( ~ on(X0,block_1,s(s(s(s(time_0)))))
| ~ neq(block_2,X0)
| ~ neq(block_1,X0)
| ~ nonfixed(X0) ) ).
cnf(u1647,hypothesis,
~ object(block_2,s(s(s(time_0)))) ).
cnf(u7576,hypothesis,
~ destination(block_5,s(s(s(s(time_0))))) ).
cnf(u264,axiom,
( ~ nonfixed(X1)
| ~ on(X3,X2,X0)
| ~ nonfixed(X3)
| ~ neq(X1,X3)
| ~ neq(X2,X3)
| ~ nonfixed(X2)
| ~ neq(X1,X2)
| ~ on(X1,X2,X0) ) ).
cnf(u6905,hypothesis,
( ~ destination(block_1,X1)
| ~ a_block(X0)
| ~ neq(block_1,X0)
| ~ destination(X0,X1) ) ).
cnf(u387,hypothesis,
neq(table,block_8) ).
cnf(u280,axiom,
( ~ time(X0)
| on(X1,X2,s(X0))
| ~ object(X1,X0)
| ~ destination(X2,X0)
| ~ a_block(X2)
| ~ neq(X1,X2)
| ~ nonfixed(X1) ) ).
cnf(u410,hypothesis,
neq(block_3,block_8) ).
cnf(u9267,hypothesis,
on(block_2,block_1,s(s(s(s(s(s(time_0))))))) ).
cnf(u1068,hypothesis,
~ destination(block_8,time_0) ).
cnf(u8457,hypothesis,
( ~ on(block_5,X0,s(s(s(s(s(s(time_0)))))))
| ~ neq(block_5,X0)
| ~ neq(block_4,X0)
| ~ a_block(X0) ) ).
cnf(u286,axiom,
( ~ nonfixed(X1)
| ~ clear(X2,X0)
| ~ nonfixed(X2)
| ~ on(X1,X2,X0) ) ).
cnf(u408,hypothesis,
neq(block_3,block_6) ).
cnf(u1948,hypothesis,
( ~ on(block_6,X2,X1)
| ~ a_block(X0)
| ~ neq(block_6,X0)
| ~ neq(X2,X0)
| ~ a_block(X2)
| ~ neq(block_6,X2)
| ~ on(block_6,X0,X1) ) ).
cnf(u8583,hypothesis,
on(block_1,table,s(s(s(s(s(s(time_0))))))) ).
cnf(u8255,hypothesis,
( ~ on(block_5,X0,s(s(s(s(time_0)))))
| ~ neq(block_5,X0)
| ~ neq(block_4,X0)
| ~ a_block(X0) ) ).
cnf(u4154,hypothesis,
~ on(block_1,block_2,s(time_0)) ).
cnf(u6009,hypothesis,
~ destination(block_4,s(s(time_0))) ).
cnf(u1946,hypothesis,
( ~ on(block_4,X2,X1)
| ~ a_block(X0)
| ~ neq(block_4,X0)
| ~ neq(X2,X0)
| ~ a_block(X2)
| ~ neq(block_4,X2)
| ~ on(block_4,X0,X1) ) ).
cnf(u427,hypothesis,
neq(block_6,table) ).
cnf(u414,hypothesis,
neq(block_4,block_6) ).
cnf(u749,hypothesis,
( ~ on(X0,X1,s(s(s(s(s(s(s(time_0))))))))
| destination(X1,s(s(s(s(s(s(time_0)))))))
| on(X0,X1,s(s(s(s(s(s(time_0)))))))
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u1335,hypothesis,
~ object(block_1,s(s(s(s(time_0))))) ).
cnf(u1211,hypothesis,
( ~ nonfixed(X0)
| source(X0,s(s(s(s(time_0)))))
| clear(X0,s(s(s(s(time_0)))))
| ~ clear(X0,s(s(s(s(s(time_0)))))) ) ).
cnf(u9515,hypothesis,
~ on(block_2,block_8,s(s(s(s(time_0))))) ).
cnf(u2365,hypothesis,
~ neq(block_8,block_8) ).
cnf(u4152,hypothesis,
( ~ on(block_2,X0,s(time_0))
| ~ neq(block_2,X0)
| ~ neq(block_1,X0)
| ~ a_block(X0) ) ).
cnf(u425,hypothesis,
neq(block_6,block_8) ).
cnf(u1463,hypothesis,
( ~ destination(block_9,X0)
| object(block_2,X0)
| object(block_3,X0)
| object(block_4,X0)
| object(block_5,X0)
| object(block_6,X0)
| object(block_7,X0)
| object(block_8,X0)
| object(block_1,X0)
| ~ time(X0) ) ).
cnf(u9415,hypothesis,
( ~ on(block_2,X0,s(s(s(s(s(s(s(time_0))))))))
| ~ neq(block_2,X0)
| ~ neq(block_1,X0)
| ~ a_block(X0) ) ).
cnf(u10308,hypothesis,
( ~ on(block_9,X0,s(s(s(s(s(s(time_0)))))))
| ~ neq(block_9,X0)
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u1342,hypothesis,
( ~ destination(X1,s(s(time_0)))
| ~ object(X0,s(s(time_0)))
| on(X0,X1,s(s(s(time_0))))
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u2993,hypothesis,
~ destination(block_5,s(s(time_0))) ).
cnf(u326,hypothesis,
~ on(block_7,block_7,X0) ).
cnf(u7409,hypothesis,
on(block_2,block_1,s(s(s(s(time_0))))) ).
cnf(u5317,hypothesis,
( ~ on(block_3,X0,s(s(s(s(s(s(time_0)))))))
| ~ neq(block_3,X0)
| ~ neq(block_6,X0)
| ~ a_block(X0) ) ).
cnf(u199,hypothesis,
different(block_4,block_7) ).
cnf(u337,hypothesis,
( ~ fixed(X0)
| ~ on(X0,table,X1) ) ).
cnf(u10332,hypothesis,
( ~ on(X0,block_2,s(s(s(s(s(s(s(time_0))))))))
| ~ neq(block_8,X0)
| ~ neq(block_2,X0)
| ~ nonfixed(X0) ) ).
cnf(u7301,hypothesis,
( ~ destination(X0,s(s(time_0)))
| ~ neq(block_2,X0)
| ~ a_block(X0) ) ).
cnf(u324,hypothesis,
~ on(block_1,block_1,X0) ).
cnf(u2371,hypothesis,
~ neq(block_2,block_2) ).
cnf(u454,hypothesis,
( ~ on(block_2,X0,X1)
| ~ nonfixed(X0)
| ~ clear(X0,X1) ) ).
cnf(u1346,hypothesis,
~ object(block_6,time_0) ).
cnf(u851,hypothesis,
~ destination(block_1,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u197,hypothesis,
different(block_4,block_5) ).
cnf(u343,hypothesis,
( ~ on(X0,block_9,X1)
| ~ fixed(X0) ) ).
cnf(u465,hypothesis,
~ on(table,block_4,X0) ).
cnf(u10426,hypothesis,
( ~ on(block_3,X0,s(s(s(s(s(s(s(time_0))))))))
| ~ neq(block_3,X0)
| ~ neq(block_6,X0)
| ~ a_block(X0) ) ).
cnf(u452,hypothesis,
( clear(block_9,X0)
| ~ object(block_9,X0) ) ).
cnf(u7025,hypothesis,
( ~ destination(X0,s(s(s(s(s(time_0))))))
| ~ neq(block_6,X0)
| ~ a_block(X0) ) ).
cnf(u208,hypothesis,
different(block_6,block_7) ).
cnf(u1503,hypothesis,
( ~ on(X0,X1,s(s(s(time_0))))
| object(X0,s(s(s(time_0))))
| on(X0,X1,s(s(s(s(time_0)))))
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u4699,hypothesis,
( ~ on(block_8,X0,s(time_0))
| ~ neq(block_8,X0)
| ~ neq(block_7,X0)
| ~ a_block(X0) ) ).
cnf(u6087,hypothesis,
~ neq(block_6,block_6) ).
cnf(u1382,hypothesis,
( ~ destination(X0,s(s(s(s(s(s(time_0)))))))
| ~ clear(X0,s(s(s(s(s(s(s(time_0))))))))
| ~ nonfixed(X0) ) ).
cnf(u9670,hypothesis,
( ~ on(X0,block_5,s(s(s(s(s(s(time_0)))))))
| ~ object(X0,s(s(s(s(s(time_0))))))
| ~ neq(X0,block_5)
| ~ nonfixed(X0) ) ).
cnf(u341,hypothesis,
( ~ fixed(X0)
| ~ on(X0,block_6,X1) ) ).
cnf(u471,hypothesis,
( clear(X0,s(s(time_0)))
| destination(X0,s(time_0))
| ~ clear(X0,s(time_0))
| ~ nonfixed(X0) ) ).
cnf(u364,hypothesis,
neq(block_7,block_3) ).
cnf(u1217,hypothesis,
( ~ on(X0,X1,s(s(s(s(time_0)))))
| object(X0,s(s(s(s(time_0)))))
| on(X0,X1,s(s(s(s(s(time_0))))))
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u1995,hypothesis,
( ~ on(block_9,X0,time_0)
| ~ neq(block_9,X0)
| ~ neq(block_8,X0)
| ~ a_block(X0) ) ).
cnf(u214,hypothesis,
different(block_7,table) ).
cnf(u1386,hypothesis,
~ object(block_4,time_0) ).
cnf(u2055,hypothesis,
( ~ on(X0,X1,s(time_0))
| object(X0,time_0)
| on(X0,X1,time_0)
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u2001,hypothesis,
( ~ on(block_8,X0,time_0)
| ~ neq(block_8,X0)
| ~ neq(block_7,X0)
| ~ a_block(X0) ) ).
cnf(u1380,hypothesis,
( ~ destination(X0,s(time_0))
| ~ clear(X0,s(s(time_0)))
| ~ nonfixed(X0) ) ).
cnf(u237,hypothesis,
nonfixed(block_9) ).
cnf(u383,hypothesis,
neq(block_8,block_7) ).
cnf(u469,hypothesis,
( ~ source(X0,s(time_0))
| clear(X0,s(s(time_0)))
| ~ nonfixed(X0) ) ).
cnf(u354,hypothesis,
neq(block_4,block_2) ).
cnf(u9417,hypothesis,
~ on(block_1,block_2,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u212,hypothesis,
different(block_7,block_8) ).
cnf(u751,hypothesis,
( ~ destination(X1,s(s(s(s(s(s(time_0)))))))
| ~ object(X0,s(s(s(s(s(s(time_0)))))))
| on(X0,X1,s(s(s(s(s(s(s(time_0))))))))
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u4094,hypothesis,
( ~ on(block_4,X0,s(s(s(s(s(time_0))))))
| ~ neq(block_4,X0)
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u227,hypothesis,
a_block(table) ).
cnf(u381,hypothesis,
neq(block_9,block_6) ).
cnf(u632,hypothesis,
~ destination(block_6,s(s(s(s(s(s(time_0))))))) ).
cnf(u4863,hypothesis,
on(block_3,block_6,s(s(s(s(s(s(time_0))))))) ).
cnf(u2922,hypothesis,
~ on(block_4,block_5,s(s(time_0))) ).
cnf(u254,hypothesis,
on(block_4,table,time_0) ).
cnf(u2053,hypothesis,
( ~ destination(X0,time_0)
| ~ clear(X0,s(time_0))
| ~ nonfixed(X0) ) ).
cnf(u1820,hypothesis,
~ destination(block_9,s(s(s(s(s(s(time_0))))))) ).
cnf(u225,hypothesis,
a_block(block_8) ).
cnf(u8477,hypothesis,
( ~ on(block_5,X0,s(s(s(time_0))))
| ~ neq(block_5,X0)
| ~ neq(block_4,X0)
| ~ a_block(X0) ) ).
cnf(u371,hypothesis,
neq(block_8,block_4) ).
cnf(u8659,hypothesis,
( ~ on(X0,block_8,s(s(s(s(s(s(s(time_0))))))))
| ~ neq(block_7,X0)
| ~ neq(block_8,X0)
| ~ nonfixed(X0) ) ).
cnf(u2183,hypothesis,
~ destination(block_7,s(time_0)) ).
cnf(u266,axiom,
( ~ a_block(X1)
| ~ fixed(X2)
| ~ on(X2,X1,X0) ) ).
cnf(u252,hypothesis,
on(block_5,block_4,time_0) ).
cnf(u4347,hypothesis,
( ~ object(X0,time_0)
| on(X0,block_2,time_0)
| ~ neq(X0,block_2)
| ~ nonfixed(X0) ) ).
cnf(u499,hypothesis,
~ on(block_4,block_5,time_0) ).
cnf(u2054,hypothesis,
( ~ destination(X1,time_0)
| ~ object(X0,time_0)
| on(X0,X1,s(time_0))
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u525,hypothesis,
( clear(X0,s(s(s(s(s(s(time_0)))))))
| ~ source(X0,s(s(s(s(s(time_0))))))
| ~ nonfixed(X0) ) ).
cnf(u2083,hypothesis,
( ~ on(block_4,X0,time_0)
| ~ a_block(X0)
| ~ neq(block_4,X0)
| on(block_4,X0,s(time_0)) ) ).
cnf(u394,hypothesis,
neq(block_1,block_7) ).
cnf(u242,hypothesis,
time(s(s(s(s(time_0))))) ).
cnf(u9402,hypothesis,
~ on(block_1,block_2,s(s(s(s(s(s(time_0))))))) ).
cnf(u523,hypothesis,
~ clear(block_2,time_0) ).
cnf(u283,axiom,
( ~ time(X0)
| on(X1,X2,s(X0))
| object(X1,X0)
| ~ on(X1,X2,X0)
| ~ a_block(X2)
| ~ neq(X1,X2)
| ~ nonfixed(X1) ) ).
cnf(u9468,hypothesis,
( ~ on(block_1,X0,s(s(s(s(s(s(s(time_0))))))))
| ~ neq(block_1,X0)
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u10243,hypothesis,
( ~ on(block_9,X0,s(s(s(time_0))))
| ~ neq(block_9,X0)
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u270,axiom,
( ~ time(X0)
| ~ clear(X1,s(X0))
| source(X1,X0)
| clear(X1,X0)
| ~ nonfixed(X1) ) ).
cnf(u392,hypothesis,
neq(block_1,block_5) ).
cnf(u2205,hypothesis,
( ~ on(block_6,X1,X2)
| ~ nonfixed(X0)
| ~ neq(block_6,X0)
| ~ neq(X1,X0)
| ~ nonfixed(X1)
| ~ neq(block_6,X1)
| ~ on(X0,X1,X2) ) ).
cnf(u281,axiom,
( ~ object(X2,X0)
| ~ object(X1,X0)
| ~ a_block(X2)
| ~ neq(X1,X2)
| ~ nonfixed(X1) ) ).
cnf(u411,hypothesis,
neq(block_3,block_9) ).
cnf(u398,hypothesis,
neq(block_2,block_3) ).
cnf(u6007,hypothesis,
~ on(block_4,block_5,s(s(s(s(s(time_0)))))) ).
cnf(u4660,hypothesis,
~ neq(table,table) ).
cnf(u4423,hypothesis,
~ object(block_6,s(s(s(time_0)))) ).
cnf(u8640,hypothesis,
( ~ on(block_7,X0,s(s(s(s(s(s(time_0)))))))
| ~ neq(block_7,X0)
| ~ neq(block_8,X0)
| ~ a_block(X0) ) ).
cnf(u733,hypothesis,
~ object(block_1,s(s(s(s(s(s(time_0))))))) ).
cnf(u409,hypothesis,
neq(block_3,block_7) ).
cnf(u2092,hypothesis,
( ~ on(block_1,X0,time_0)
| ~ a_block(X0)
| ~ neq(block_1,X0)
| on(block_1,X0,s(time_0)) ) ).
cnf(u2211,hypothesis,
( ~ on(X0,block_2,time_0)
| ~ neq(block_3,X0)
| ~ neq(block_2,X0)
| ~ nonfixed(X0) ) ).
cnf(u7222,hypothesis,
~ destination(block_9,s(time_0)) ).
cnf(u8598,hypothesis,
( ~ on(X0,block_4,s(s(s(s(s(s(s(time_0))))))))
| ~ neq(block_5,X0)
| ~ neq(block_4,X0)
| ~ nonfixed(X0) ) ).
cnf(u10136,hypothesis,
~ on(block_5,block_3,s(time_0)) ).
cnf(u1339,hypothesis,
( ~ source(X0,s(s(time_0)))
| clear(X0,s(s(s(time_0))))
| ~ nonfixed(X0) ) ).
cnf(u2193,hypothesis,
~ object(block_1,s(time_0)) ).
cnf(u1326,hypothesis,
~ destination(block_4,s(s(s(s(time_0))))) ).
cnf(u183,hypothesis,
different(block_2,block_4) ).
cnf(u2362,hypothesis,
~ neq(block_7,block_7) ).
cnf(u351,hypothesis,
neq(block_9,block_1) ).
cnf(u438,hypothesis,
( clear(block_5,X0)
| ~ destination(block_5,X0) ) ).
cnf(u1330,hypothesis,
~ destination(block_8,s(s(s(s(time_0))))) ).
cnf(u10417,hypothesis,
( ~ object(X0,s(s(s(s(s(s(time_0)))))))
| ~ neq(X0,block_9)
| ~ nonfixed(X0) ) ).
cnf(u181,hypothesis,
different(block_1,table) ).
cnf(u6038,hypothesis,
( ~ on(block_9,X0,s(time_0))
| ~ neq(block_9,X0)
| ~ neq(block_8,X0)
| ~ a_block(X0) ) ).
cnf(u436,hypothesis,
( clear(block_7,X0)
| ~ destination(block_7,X0) ) ).
cnf(u9792,hypothesis,
on(block_3,block_5,s(s(s(s(s(time_0)))))) ).
cnf(u6850,hypothesis,
( ~ source(X0,s(time_0))
| ~ a_block(X0)
| ~ neq(block_8,X0) ) ).
cnf(u9913,hypothesis,
( ~ source(X0,s(s(s(s(s(s(time_0)))))))
| ~ a_block(X0)
| ~ neq(table,X0) ) ).
cnf(u835,hypothesis,
~ destination(block_6,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u327,hypothesis,
( ~ fixed(X0)
| ~ on(X0,block_7,X1) ) ).
cnf(u449,hypothesis,
( clear(block_6,X0)
| ~ destination(block_6,X0) ) ).
cnf(u2900,hypothesis,
~ on(block_4,block_5,s(time_0)) ).
cnf(u192,hypothesis,
different(block_3,block_6) ).
cnf(u339,hypothesis,
( ~ fixed(X0)
| ~ on(X0,block_8,X1) ) ).
cnf(u698,hypothesis,
~ destination(block_7,s(s(s(s(s(s(time_0))))))) ).
cnf(u325,hypothesis,
( ~ fixed(X0)
| ~ on(X0,block_1,X1) ) ).
cnf(u455,hypothesis,
( ~ on(block_3,X0,X1)
| ~ nonfixed(X0)
| ~ clear(X0,X1) ) ).
cnf(u5450,hypothesis,
( ~ on(X0,block_8,s(s(time_0)))
| ~ object(X0,s(time_0))
| ~ neq(X0,block_8)
| ~ nonfixed(X0) ) ).
cnf(u348,hypothesis,
neq(block_6,block_1) ).
cnf(u4501,hypothesis,
~ destination(block_4,s(s(s(time_0)))) ).
cnf(u10051,hypothesis,
( ~ on(block_6,X0,s(s(s(time_0))))
| ~ neq(block_6,X0)
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u198,hypothesis,
different(block_4,block_6) ).
cnf(u9264,hypothesis,
( ~ on(X0,block_1,s(s(s(s(s(time_0))))))
| ~ neq(block_2,X0)
| ~ neq(block_1,X0)
| ~ nonfixed(X0) ) ).
cnf(u9552,hypothesis,
( ~ on(X0,block_2,s(s(s(s(s(s(time_0)))))))
| ~ neq(block_8,X0)
| ~ neq(block_2,X0)
| ~ nonfixed(X0) ) ).
cnf(u852,hypothesis,
~ object(block_1,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u1370,hypothesis,
~ destination(block_1,time_0) ).
cnf(u10057,hypothesis,
( ~ destination(X0,s(time_0))
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u3986,hypothesis,
( ~ on(block_4,X0,s(s(s(time_0))))
| ~ neq(block_4,X0)
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u221,hypothesis,
a_block(block_4) ).
cnf(u2868,hypothesis,
( ~ on(block_7,X0,s(s(time_0)))
| ~ neq(block_7,X0)
| ~ neq(block_6,X0)
| ~ a_block(X0) ) ).
cnf(u367,hypothesis,
neq(table,block_3) ).
cnf(u453,hypothesis,
( ~ on(block_1,X0,X1)
| ~ nonfixed(X0)
| ~ clear(X0,X1) ) ).
cnf(u5448,hypothesis,
( ~ object(X0,s(time_0))
| on(X0,block_8,s(time_0))
| ~ neq(X0,block_8)
| ~ nonfixed(X0) ) ).
cnf(u338,hypothesis,
~ on(block_8,block_8,X0) ).
cnf(u196,hypothesis,
different(block_3,table) ).
cnf(u735,hypothesis,
~ source(block_1,s(s(s(s(s(time_0)))))) ).
cnf(u1498,hypothesis,
( ~ on(X0,X1,s(s(s(s(time_0)))))
| destination(X1,s(s(s(time_0))))
| on(X0,X1,s(s(s(time_0))))
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u708,hypothesis,
~ object(block_5,s(s(s(s(s(time_0)))))) ).
cnf(u10185,hypothesis,
( ~ on(block_3,X0,s(s(s(time_0))))
| ~ neq(block_3,X0)
| ~ neq(block_5,X0)
| ~ a_block(X0) ) ).
cnf(u1492,hypothesis,
( destination(block_8,X0)
| object(block_3,X0)
| object(block_4,X0)
| object(block_5,X0)
| object(block_6,X0)
| object(block_7,X0)
| object(block_8,X0)
| object(block_1,X0)
| ~ time(X0)
| destination(block_2,X0)
| destination(block_3,X0)
| destination(block_4,X0)
| destination(block_5,X0)
| destination(block_6,X0)
| destination(block_7,X0)
| object(block_2,X0)
| destination(block_1,X0)
| destination(table,X0) ) ).
cnf(u211,hypothesis,
different(block_6,table) ).
cnf(u365,hypothesis,
neq(block_8,block_3) ).
cnf(u10756,hypothesis,
~ on(block_7,block_6,s(s(s(s(s(time_0)))))) ).
cnf(u466,hypothesis,
~ on(table,block_1,X0) ).
cnf(u10485,hypothesis,
( ~ on(block_6,X0,s(s(s(s(s(s(s(time_0))))))))
| ~ neq(block_6,X0)
| ~ neq(block_7,X0)
| ~ a_block(X0) ) ).
cnf(u238,hypothesis,
time(time_0) ).
cnf(u1381,hypothesis,
( ~ destination(X0,s(s(s(s(s(time_0))))))
| ~ clear(X0,s(s(s(s(s(s(time_0)))))))
| ~ nonfixed(X0) ) ).
cnf(u1496,hypothesis,
( ~ nonfixed(X0)
| source(X0,s(s(s(time_0))))
| clear(X0,s(s(s(time_0))))
| ~ clear(X0,s(s(s(s(time_0))))) ) ).
cnf(u209,hypothesis,
different(block_6,block_8) ).
cnf(u355,hypothesis,
neq(block_5,block_2) ).
cnf(u744,hypothesis,
~ object(block_2,s(s(s(s(s(time_0)))))) ).
cnf(u378,hypothesis,
neq(table,block_5) ).
cnf(u464,hypothesis,
~ on(table,block_7,X0) ).
cnf(u1385,hypothesis,
~ destination(block_4,time_0) ).
cnf(u236,hypothesis,
nonfixed(block_8) ).
cnf(u3823,hypothesis,
( ~ on(block_1,X0,s(s(s(time_0))))
| ~ neq(block_1,X0)
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u9416,hypothesis,
( ~ on(X0,block_1,s(s(s(s(s(s(s(time_0))))))))
| ~ neq(block_2,X0)
| ~ neq(block_1,X0)
| ~ nonfixed(X0) ) ).
cnf(u251,hypothesis,
on(block_1,table,time_0) ).
cnf(u10754,hypothesis,
( ~ on(block_6,X0,s(s(s(s(s(time_0))))))
| ~ neq(block_6,X0)
| ~ neq(block_7,X0)
| ~ a_block(X0) ) ).
cnf(u376,hypothesis,
neq(block_8,block_5) ).
cnf(u8856,hypothesis,
~ on(block_1,block_2,s(s(s(s(time_0))))) ).
cnf(u226,hypothesis,
a_block(block_9) ).
cnf(u7265,hypothesis,
( ~ on(block_2,X0,s(s(time_0)))
| ~ neq(block_2,X0)
| ~ neq(block_1,X0)
| ~ a_block(X0) ) ).
cnf(u635,hypothesis,
~ source(block_6,s(s(s(s(s(time_0)))))) ).
cnf(u249,hypothesis,
clear(block_3,time_0) ).
cnf(u267,axiom,
( ~ source(X1,X0)
| ~ destination(X1,X0)
| ~ a_block(X1) ) ).
cnf(u748,hypothesis,
( ~ source(X0,s(s(s(s(s(s(time_0)))))))
| clear(X0,s(s(s(s(s(s(s(time_0))))))))
| ~ nonfixed(X0) ) ).
cnf(u382,hypothesis,
neq(table,block_6) ).
cnf(u1159,hypothesis,
~ on(table,block_9,s(s(s(s(s(time_0)))))) ).
cnf(u10725,hypothesis,
( ~ object(X0,s(s(s(s(time_0)))))
| ~ neq(X0,block_6)
| ~ nonfixed(X0) ) ).
cnf(u526,hypothesis,
( ~ on(X0,X1,s(s(s(s(s(s(time_0)))))))
| destination(X1,s(s(s(s(s(time_0))))))
| on(X0,X1,s(s(s(s(s(time_0))))))
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u2189,hypothesis,
~ destination(block_8,s(time_0)) ).
cnf(u255,hypothesis,
on(block_9,block_8,time_0) ).
cnf(u6906,hypothesis,
( ~ destination(block_2,X1)
| ~ a_block(X0)
| ~ neq(block_2,X0)
| ~ destination(X0,X1) ) ).
cnf(u265,axiom,
( ~ on(X1,X2,X0)
| ~ on(X2,X1,X0)
| ~ a_block(X2)
| ~ neq(X1,X2)
| ~ a_block(X1) ) ).
cnf(u395,hypothesis,
neq(block_1,block_8) ).
cnf(u8478,hypothesis,
( ~ on(X0,block_4,s(s(s(time_0))))
| ~ neq(block_5,X0)
| ~ neq(block_4,X0)
| ~ nonfixed(X0) ) ).
cnf(u9383,hypothesis,
( ~ source(X0,s(s(s(time_0))))
| ~ a_block(X0)
| ~ neq(block_6,X0) ) ).
cnf(u7567,hypothesis,
on(block_7,block_8,s(s(s(s(time_0))))) ).
cnf(u393,hypothesis,
neq(block_1,block_6) ).
cnf(u1950,hypothesis,
( ~ on(block_8,X2,X1)
| ~ a_block(X0)
| ~ neq(block_8,X0)
| ~ neq(X2,X0)
| ~ a_block(X2)
| ~ neq(block_8,X2)
| ~ on(block_8,X0,X1) ) ).
cnf(u677,hypothesis,
~ object(block_8,s(s(s(s(s(s(time_0))))))) ).
cnf(u7302,hypothesis,
( ~ object(X0,s(s(time_0)))
| on(X0,block_2,s(s(s(time_0))))
| ~ neq(X0,block_2)
| ~ nonfixed(X0) ) ).
cnf(u10474,hypothesis,
on(block_6,block_7,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u2091,hypothesis,
( ~ on(block_2,X0,time_0)
| ~ a_block(X0)
| ~ neq(block_2,X0)
| on(block_2,X0,s(time_0)) ) ).
cnf(u8854,hypothesis,
( ~ on(block_2,X0,s(s(s(s(time_0)))))
| ~ neq(block_2,X0)
| ~ neq(block_1,X0)
| ~ a_block(X0) ) ).
cnf(u9726,hypothesis,
( ~ destination(X0,s(s(s(s(s(s(time_0)))))))
| ~ neq(block_5,X0)
| ~ a_block(X0) ) ).
cnf(u715,hypothesis,
~ destination(block_7,s(s(s(s(s(time_0)))))) ).
cnf(u2204,hypothesis,
( ~ on(block_5,X1,X2)
| ~ nonfixed(X0)
| ~ neq(block_5,X0)
| ~ neq(X1,X0)
| ~ nonfixed(X1)
| ~ neq(block_5,X1)
| ~ on(X0,X1,X2) ) ).
cnf(u422,hypothesis,
neq(block_5,block_9) ).
cnf(u1343,hypothesis,
( ~ on(X0,X1,s(s(s(time_0))))
| object(X0,s(s(time_0)))
| on(X0,X1,s(s(time_0)))
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u223,hypothesis,
a_block(block_6) ).
cnf(u4256,hypothesis,
~ on(block_1,block_2,s(s(s(time_0)))) ).
cnf(u433,hypothesis,
neq(block_9,table) ).
cnf(u2528,hypothesis,
( ~ on(block_7,X0,s(time_0))
| ~ neq(block_7,X0)
| ~ neq(block_6,X0)
| ~ a_block(X0) ) ).
cnf(u420,hypothesis,
neq(block_5,block_7) ).
cnf(u176,hypothesis,
different(block_1,block_5) ).
cnf(u4700,hypothesis,
( ~ on(X0,block_7,s(time_0))
| ~ neq(block_8,X0)
| ~ neq(block_7,X0)
| ~ nonfixed(X0) ) ).
cnf(u679,hypothesis,
~ source(block_8,s(s(s(s(s(time_0)))))) ).
cnf(u9514,hypothesis,
( ~ on(X0,block_2,s(s(s(s(time_0)))))
| ~ neq(block_8,X0)
| ~ neq(block_2,X0)
| ~ nonfixed(X0) ) ).
cnf(u7406,hypothesis,
( ~ on(block_2,X0,s(s(s(time_0))))
| ~ neq(block_2,X0)
| ~ neq(block_1,X0)
| ~ a_block(X0) ) ).
cnf(u439,hypothesis,
( clear(block_5,X0)
| ~ object(block_5,X0) ) ).
cnf(u2884,hypothesis,
on(block_5,block_4,s(time_0)) ).
cnf(u182,hypothesis,
different(block_2,block_3) ).
cnf(u6649,hypothesis,
( ~ on(block_1,X0,s(s(s(s(time_0)))))
| ~ neq(block_1,X0)
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u5804,hypothesis,
on(block_6,table,s(time_0)) ).
cnf(u9381,hypothesis,
( ~ object(X0,s(s(s(time_0))))
| on(X0,block_6,s(s(s(time_0))))
| ~ neq(X0,block_6)
| ~ nonfixed(X0) ) ).
cnf(u840,hypothesis,
~ object(block_4,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u437,hypothesis,
( clear(block_7,X0)
| ~ object(block_7,X0) ) ).
cnf(u4701,hypothesis,
~ on(block_7,block_8,s(time_0)) ).
cnf(u2234,hypothesis,
( ~ on(X0,block_8,time_0)
| ~ neq(block_9,X0)
| ~ neq(block_8,X0)
| ~ nonfixed(X0) ) ).
cnf(u332,hypothesis,
~ on(block_4,block_4,X0) ).
cnf(u180,hypothesis,
different(block_1,block_9) ).
cnf(u9513,hypothesis,
( ~ on(block_8,X0,s(s(s(s(time_0)))))
| ~ neq(block_8,X0)
| ~ neq(block_2,X0)
| ~ a_block(X0) ) ).
cnf(u10840,hypothesis,
~ on(block_6,table,s(s(s(s(s(time_0)))))) ).
cnf(u205,hypothesis,
different(block_5,block_8) ).
cnf(u8625,hypothesis,
( ~ on(block_4,X0,s(s(s(s(s(s(s(time_0))))))))
| ~ neq(block_4,X0)
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u4703,hypothesis,
on(block_8,block_7,s(s(time_0))) ).
cnf(u7633,hypothesis,
~ on(block_5,block_3,s(s(s(s(time_0))))) ).
cnf(u2898,hypothesis,
( ~ on(block_5,X0,s(time_0))
| ~ neq(block_5,X0)
| ~ neq(block_4,X0)
| ~ a_block(X0) ) ).
cnf(u5186,hypothesis,
( ~ on(X0,block_6,s(s(s(time_0))))
| ~ neq(block_7,X0)
| ~ neq(block_6,X0)
| ~ nonfixed(X0) ) ).
cnf(u460,hypothesis,
( ~ on(block_8,X0,X1)
| ~ nonfixed(X0)
| ~ clear(X0,X1) ) ).
cnf(u10187,hypothesis,
~ on(block_5,block_3,s(s(s(time_0)))) ).
cnf(u8581,hypothesis,
( ~ on(block_1,X0,s(s(s(s(s(time_0))))))
| ~ neq(block_1,X0)
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u719,hypothesis,
~ destination(block_2,s(s(s(s(s(s(time_0))))))) ).
cnf(u8597,hypothesis,
( ~ on(block_5,X0,s(s(s(s(s(s(s(time_0))))))))
| ~ neq(block_5,X0)
| ~ neq(block_4,X0)
| ~ a_block(X0) ) ).
cnf(u8256,hypothesis,
( ~ on(X0,block_4,s(s(s(s(time_0)))))
| ~ neq(block_5,X0)
| ~ neq(block_4,X0)
| ~ nonfixed(X0) ) ).
cnf(u844,hypothesis,
~ object(block_7,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u195,hypothesis,
different(block_3,block_9) ).
cnf(u349,hypothesis,
neq(block_7,block_1) ).
cnf(u450,hypothesis,
( clear(block_6,X0)
| ~ object(block_6,X0) ) ).
cnf(u222,hypothesis,
a_block(block_5) ).
cnf(u5318,hypothesis,
( ~ on(X0,block_6,s(s(s(s(s(s(time_0)))))))
| ~ neq(block_3,X0)
| ~ neq(block_6,X0)
| ~ nonfixed(X0) ) ).
cnf(u722,hypothesis,
~ source(block_2,s(s(s(s(s(time_0)))))) ).
cnf(u193,hypothesis,
different(block_3,block_7) ).
cnf(u728,hypothesis,
~ destination(block_8,s(s(s(s(s(time_0)))))) ).
cnf(u362,hypothesis,
neq(block_5,block_3) ).
cnf(u448,hypothesis,
( clear(block_8,X0)
| ~ object(block_8,X0) ) ).
cnf(u220,hypothesis,
a_block(block_3) ).
cnf(u707,hypothesis,
~ destination(block_5,s(s(s(s(s(time_0)))))) ).
cnf(u7551,hypothesis,
( ~ destination(X0,s(s(s(s(time_0)))))
| ~ neq(block_7,X0)
| ~ a_block(X0) ) ).
cnf(u8858,hypothesis,
on(block_2,block_1,s(s(s(s(s(time_0)))))) ).
cnf(u843,hypothesis,
~ destination(block_7,s(s(s(s(s(s(s(time_0)))))))) ).
cnf(u2529,hypothesis,
( ~ on(X0,block_6,s(time_0))
| ~ neq(block_7,X0)
| ~ neq(block_6,X0)
| ~ nonfixed(X0) ) ).
cnf(u235,hypothesis,
nonfixed(block_7) ).
cnf(u467,hypothesis,
~ on(table,block_8,X0) ).
cnf(u10299,hypothesis,
( ~ on(block_9,X0,s(s(s(s(s(time_0))))))
| ~ neq(block_9,X0)
| ~ neq(table,X0)
| ~ a_block(X0) ) ).
cnf(u360,hypothesis,
neq(table,block_2) ).
cnf(u210,hypothesis,
different(block_6,block_9) ).
cnf(u1497,hypothesis,
( ~ source(X0,s(s(s(time_0))))
| clear(X0,s(s(s(s(time_0)))))
| ~ nonfixed(X0) ) ).
cnf(u8642,hypothesis,
~ on(block_8,block_7,s(s(s(s(s(s(time_0))))))) ).
cnf(u5197,hypothesis,
( ~ destination(X0,s(s(s(time_0))))
| on(block_7,X0,s(s(s(s(time_0)))))
| ~ a_block(X0)
| ~ neq(block_7,X0) ) ).
cnf(u8538,hypothesis,
~ on(block_8,block_7,s(s(s(s(time_0))))) ).
cnf(u720,hypothesis,
~ object(block_2,s(s(s(s(s(s(time_0))))))) ).
cnf(u10486,hypothesis,
( ~ on(X0,block_7,s(s(s(s(s(s(s(time_0))))))))
| ~ neq(block_6,X0)
| ~ neq(block_7,X0)
| ~ nonfixed(X0) ) ).
cnf(u233,hypothesis,
nonfixed(block_5) ).
cnf(u379,hypothesis,
neq(block_7,block_6) ).
cnf(u732,hypothesis,
~ destination(block_1,s(s(s(s(s(s(time_0))))))) ).
cnf(u366,hypothesis,
neq(block_9,block_3) ).
cnf(u10216,hypothesis,
~ on(table,block_9,s(s(time_0))) ).
cnf(u2028,hypothesis,
( ~ on(block_5,X0,time_0)
| ~ neq(block_5,X0)
| ~ neq(block_4,X0)
| ~ a_block(X0) ) ).
cnf(u747,hypothesis,
( ~ nonfixed(X0)
| source(X0,s(s(s(s(s(s(time_0)))))))
| clear(X0,s(s(s(s(s(s(time_0)))))))
| ~ clear(X0,s(s(s(s(s(s(s(time_0)))))))) ) ).
cnf(u4861,hypothesis,
( ~ object(X0,s(s(s(s(s(time_0))))))
| ~ neq(X0,block_3)
| ~ nonfixed(X0) ) ).
cnf(u4079,hypothesis,
~ on(block_4,block_5,s(s(s(s(time_0))))) ).
cnf(u239,hypothesis,
time(s(time_0)) ).
cnf(u377,hypothesis,
neq(block_9,block_5) ).
cnf(u2051,hypothesis,
( ~ on(X0,X1,s(time_0))
| destination(X1,time_0)
| on(X0,X1,time_0)
| ~ a_block(X1)
| ~ neq(X0,X1)
| ~ nonfixed(X0) ) ).
cnf(u272,axiom,
( ~ time(X0)
| clear(X1,s(X0))
| ~ source(X1,X0)
| ~ nonfixed(X1) ) ).
cnf(u250,hypothesis,
on(block_2,block_1,time_0) ).
cnf(u505,hypothesis,
~ clear(block_7,time_0) ).
cnf(u278,axiom,
( ~ nonfixed(X1)
| ~ destination(X1,X0)
| clear(X1,X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PLA025+1 : TPTP v9.3.1. Bugfixed v2.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.42 % Computer : n016.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.43 % DateTime : Sun Sep 27 22:15:02 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.43 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.22/0.47 Running first-order theorem proving
% 0.22/0.47 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
% 14.18/3.11 % (3044841)Detected formulas, will run a generic FOF schedule.
% 14.18/3.11 % (3044851)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1624166689:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 14.18/3.11 % (3044854)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1190103840:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 14.18/3.11 % (3044852)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=26046369:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 14.18/3.11 % (3044853)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2696741267:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 14.18/3.11 % (3044850)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=62448904:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 14.18/3.11 % (3044855)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1907822944:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 14.18/3.11 % (3044856)dis-21_1_sil=8000:lcm=predicate:random_seed=1032139177:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 14.18/3.11 % (3044854)Instruction limit reached!
% 14.18/3.11 % (3044854)------------------------------
% 14.18/3.11 % (3044854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/3.11 % (3044854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/3.11 % (3044854)CaDiCaL version: 2.1.3
% 14.18/3.11 % (3044854)Termination reason: Instruction limit
% 14.18/3.11 % (3044854)Termination phase: Saturation
% 14.18/3.11 % (3044854)Time elapsed: 0.089 s
% 14.18/3.11 % (3044854)Peak memory usage: 87 MB
% 14.18/3.11 % (3044854)Instructions burned: 119 (million)
% 14.18/3.11 % (3044853)Instruction limit reached!
% 14.18/3.11 % (3044853)------------------------------
% 14.18/3.11 % (3044853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/3.11 % (3044853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/3.11 % (3044853)CaDiCaL version: 2.1.3
% 14.18/3.11 % (3044853)Termination reason: Instruction limit
% 14.18/3.11 % (3044853)Termination phase: Saturation
% 14.18/3.11 % (3044853)Time elapsed: 0.089 s
% 14.18/3.11 % (3044853)Peak memory usage: 88 MB
% 14.18/3.11 % (3044853)Instructions burned: 109 (million)
% 14.18/3.11 % (3044856)Instruction limit reached!
% 14.18/3.11 % (3044856)------------------------------
% 14.18/3.11 % (3044856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/3.11 % (3044856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/3.11 % (3044856)CaDiCaL version: 2.1.3
% 14.18/3.11 % (3044856)Termination reason: Instruction limit
% 14.18/3.11 % (3044856)Termination phase: Saturation
% 14.18/3.11 % (3044856)Time elapsed: 0.118 s
% 14.18/3.11 % (3044856)Peak memory usage: 90 MB
% 14.18/3.11 % (3044856)Instructions burned: 129 (million)
% 14.18/3.11 % (3044855)Instruction limit reached!
% 14.18/3.11 % (3044855)------------------------------
% 14.18/3.11 % (3044855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/3.11 % (3044855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/3.11 % (3044855)CaDiCaL version: 2.1.3
% 14.18/3.11 % (3044855)Termination reason: Instruction limit
% 14.18/3.11 % (3044855)Termination phase: Saturation
% 14.18/3.11 % (3044855)Time elapsed: 0.127 s
% 14.18/3.11 % (3044855)Peak memory usage: 89 MB
% 14.18/3.11 % (3044855)Instructions burned: 140 (million)
% 14.18/3.11 % (3044864)lrs+10_1_sil=8000:sp=occurrence:random_seed=2298685063:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 14.18/3.11 % (3044865)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2276412352:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 14.18/3.11 % (3044865)Refutation not found, incomplete strategy
% 14.18/3.11 % (3044865)------------------------------
% 14.18/3.11 % (3044865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/3.11 % (3044865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/3.11 % (3044865)CaDiCaL version: 2.1.3
% 14.18/3.11 % (3044865)Termination reason: Refutation not found, incomplete strategy
% 14.18/3.11 % (3044865)Time elapsed: 0.005 s
% 14.18/3.11 % (3044865)Peak memory usage: 88 MB
% 14.18/3.11 % (3044865)Instructions burned: 3 (million)
% 14.18/3.11 % (3044866)lrs+1011_1_sil=32000:sp=occurrence:random_seed=218694545:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 14.18/3.11 % (3044867)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=948590510:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 14.18/3.11 % (3044864)Instruction limit reached!
% 14.18/3.11 % (3044864)------------------------------
% 14.18/3.11 % (3044864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/3.11 % (3044864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/3.11 % (3044864)CaDiCaL version: 2.1.3
% 14.18/3.11 % (3044864)Termination reason: Instruction limit
% 14.18/3.11 % (3044864)Termination phase: Saturation
% 14.18/3.11 % (3044864)Time elapsed: 0.196 s
% 14.18/3.11 % (3044864)Peak memory usage: 89 MB
% 14.18/3.11 % (3044864)Instructions burned: 286 (million)
% 14.18/3.11 % (3044867)Refutation not found, incomplete strategy
% 14.18/3.12 % (3044867)------------------------------
% 14.18/3.12 % (3044867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/3.12 % (3044867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/3.12 % (3044867)CaDiCaL version: 2.1.3
% 14.18/3.12 % (3044867)Termination reason: Refutation not found, incomplete strategy
% 14.18/3.12 % (3044867)Time elapsed: 0.096 s
% 14.18/3.12 % (3044867)Peak memory usage: 89 MB
% 14.18/3.12 % (3044867)Instructions burned: 112 (million)
% 14.18/3.12 % (3044866)Instruction limit reached!
% 14.18/3.12 % (3044866)------------------------------
% 14.18/3.12 % (3044866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/3.12 % (3044866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/3.12 % (3044866)CaDiCaL version: 2.1.3
% 14.18/3.12 % (3044866)Termination reason: Instruction limit
% 14.18/3.12 % (3044866)Termination phase: Saturation
% 14.18/3.12 % (3044866)Time elapsed: 0.294 s
% 14.18/3.12 % (3044866)Peak memory usage: 91 MB
% 14.18/3.12 % (3044866)Instructions burned: 325 (million)
% 14.18/3.12 % (3044872)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2993246903:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2992 on theBenchmark for (2992ds/294Mi)
% 14.18/3.12 % (3044865)------------------------------
% 14.18/3.12 % (3044865)------------------------------
% 14.18/3.12 % (3044872)Instruction limit reached!
% 14.18/3.12 % (3044872)------------------------------
% 14.18/3.12 % (3044872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/3.12 % (3044872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/3.12 % (3044872)CaDiCaL version: 2.1.3
% 14.18/3.12 % (3044872)Termination reason: Instruction limit
% 14.18/3.12 % (3044872)Termination phase: Saturation
% 14.18/3.12 % (3044872)Time elapsed: 0.147 s
% 14.18/3.12 % (3044872)Peak memory usage: 88 MB
% 14.18/3.12 % (3044872)Instructions burned: 295 (million)
% 14.18/3.12 % (3044867)------------------------------
% 14.18/3.12 % (3044867)------------------------------
% 14.18/3.12 % (3044873)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1935205227:i=2350_2990 on theBenchmark for (2990ds/2350Mi)
% 14.18/3.12 % (3044875)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1334818426:cts=off:i=113:fsr=off:ss=included:sgt=4_2989 on theBenchmark for (2989ds/113Mi)
% 14.18/3.12 % (3044877)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4007901256:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2987 on theBenchmark for (2987ds/114Mi)
% 14.18/3.12 % (3044876)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=842540184:i=127:av=off:fsr=off:sup=off_2988 on theBenchmark for (2988ds/127Mi)
% 14.18/3.12 % (3044875)Instruction limit reached!
% 14.18/3.12 % (3044875)------------------------------
% 14.18/3.12 % (3044875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/3.12 % (3044875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/3.12 % (3044875)CaDiCaL version: 2.1.3
% 14.18/3.12 % (3044875)Termination reason: Instruction limit
% 14.18/3.12 % (3044875)Termination phase: Saturation
% 14.18/3.12 % (3044875)Time elapsed: 0.109 s
% 14.18/3.12 % (3044875)Peak memory usage: 90 MB
% 14.18/3.12 % (3044875)Instructions burned: 113 (million)
% 14.18/3.12 % (3044877)Refutation not found, incomplete strategy
% 14.18/3.12 % (3044877)------------------------------
% 14.18/3.12 % (3044877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/3.12 % (3044877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/3.12 % (3044877)CaDiCaL version: 2.1.3
% 14.18/3.12 % (3044877)Termination reason: Refutation not found, incomplete strategy
% 14.18/3.12 % (3044877)Time elapsed: 0.009 s
% 14.18/3.12 % (3044877)Peak memory usage: 88 MB
% 14.18/3.12 % (3044877)Instructions burned: 7 (million)
% 14.18/3.12 % (3044876)Instruction limit reached!
% 14.18/3.12 % (3044876)------------------------------
% 14.18/3.12 % (3044876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.18/3.12 % (3044876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.18/3.12 % (3044876)CaDiCaL version: 2.1.3
% 14.18/3.12 % (3044876)Termination reason: Instruction limit
% 14.18/3.12 % (3044876)Termination phase: Saturation
% 14.18/3.12 % (3044876)Time elapsed: 0.115 s
% 14.18/3.12 % (3044876)Peak memory usage: 89 MB
% 14.18/3.12 % (3044876)Instructions burned: 127 (million)
% 14.18/3.12 % (3044882)lrs+10_1_sil=8000:sp=occurrence:random_seed=2561398407:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 14.18/3.12 % (3044851)First to succeed.
% 14.18/3.12 % (3044851)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3044841"
% 14.18/3.12 % (3044877)------------------------------
% 14.18/3.12 % (3044877)------------------------------
% 14.18/3.12 % (3044883)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2161101799:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 14.18/3.12 % SZS status CounterSatisfiable for theBenchmark
% 14.18/3.12 % SZS output start Saturation.
% See solution above
% 14.94/3.35 % SZS output start Definitions and Model Updates.
% 14.94/3.35 for all groundings,
% 14.94/3.35 whenever goal_time(sK0) is false, set goal_time(sK0) to true
% 14.94/3.35 for all groundings,
% 14.94/3.35 whenever goal_time(s(s(s(s(s(s(time_0))))))) is false, set goal_time(s(s(s(s(s(s(time_0))))))) to true
% 14.94/3.35 % SZS output end Definitions and Model Updates.
% 14.94/3.35 % (3044851)------------------------------
% 14.94/3.35 % (3044851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.94/3.35 % (3044851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.94/3.35 % (3044851)CaDiCaL version: 2.1.3
% 14.94/3.35 % (3044851)Termination reason: Satisfiable
% 14.94/3.35 % (3044851)Time elapsed: 1.551 s
% 14.94/3.35 % (3044851)Peak memory usage: 138 MB
% 14.94/3.35 % (3044851)Instructions burned: 2420 (million)
% 14.94/3.35 % (3044851)------------------------------
% 14.94/3.35 % (3044851)------------------------------
% 14.94/3.35 % (3044841)Success in time 1.995 s
% 14.94/3.35 % Vampire exiting
%------------------------------------------------------------------------------