%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV238+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n010.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 01:20:32 PM UTC 2026
% Result : CounterSatisfiable 1.20s 0.59s
% Output : Saturation 1.20s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u76,axiom,
( p(enc(X0,X1))
| ~ p(X0)
| ~ p(X1) ) ).
cnf(u83,axiom,
( p(enc(enc(i(wk),X1),enc(i(lp),X0)))
| ~ p(X1)
| ~ p(X0) ) ).
cnf(u87,axiom,
( p(enc(i(enc(i(tc),X0)),X1))
| ~ p(X0)
| ~ p(X1) ) ).
cnf(u91,axiom,
( p(enc(enc(i(tc),X0),X1))
| ~ p(X0)
| ~ p(X1) ) ).
cnf(u95,axiom,
( p(enc(enc(i(tmk),X1),enc(i(tc),X0)))
| ~ p(X1)
| ~ p(X0) ) ).
cnf(u99,axiom,
( p(enc(enc(i(tmk),X1),enc(i(tmk),X0)))
| ~ p(X1)
| ~ p(X0) ) ).
cnf(u103,axiom,
( p(enc(wk,enc(i(tmk),X0)))
| ~ p(X0) ) ).
cnf(u107,axiom,
( p(enc(i(enc(i(zcmk),X1)),enc(i(tmk),X0)))
| ~ p(X1)
| ~ p(X0) ) ).
cnf(u111,axiom,
( p(enc(tmk,enc(i(enc(i(zcmk),X1)),X0)))
| ~ p(X1)
| ~ p(X0) ) ).
cnf(u225,axiom,
~ p(w) ).
cnf(u234,axiom,
~ p(lp) ).
cnf(u243,axiom,
~ p(tc) ).
cnf(u247,axiom,
p(k) ).
cnf(u252,axiom,
~ p(wk) ).
cnf(u265,axiom,
~ p(tmk) ).
cnf(u273,axiom,
( ~ p(enc(i(wk),X2))
| ~ p(X2) ) ).
cnf(u284,axiom,
( ~ p(enc(i(tmk),X1))
| ~ p(X1) ) ).
cnf(u288,axiom,
( p(enc(i(tc),X0))
| ~ p(X0) ) ).
cnf(u296,axiom,
( ~ p(i(enc(i(zcmk),X1)))
| ~ p(X1) ) ).
cnf(u309,axiom,
( ~ p(enc(i(zcmk),X0))
| ~ p(X0) ) ).
cnf(u377,axiom,
~ p(zcmk) ).
cnf(u412,axiom,
~ p(i(zcmk)) ).
cnf(u435,axiom,
~ p(i(wk)) ).
cnf(u453,axiom,
( p(enc(enc(i(wk),X1),enc(i(tmk),X2)))
| ~ p(X2)
| ~ p(X1) ) ).
cnf(u457,axiom,
( p(enc(enc(i(wk),X1),enc(i(tc),X2)))
| ~ p(X2)
| ~ p(X1) ) ).
cnf(u508,axiom,
~ p(i(tmk)) ).
cnf(u528,axiom,
( p(enc(enc(i(wk),X1),k))
| ~ p(X1) ) ).
cnf(u542,axiom,
( p(enc(enc(i(wk),X1),pp))
| ~ p(X1) ) ).
cnf(u679,axiom,
( ~ p(enc(i(enc(i(zcmk),X1)),X2))
| ~ p(X1)
| ~ p(X2) ) ).
cnf(u713,axiom,
( p(enc(enc(i(wk),X3),enc(i(enc(i(zcmk),X1)),X2)))
| ~ p(X3)
| ~ p(X1)
| ~ p(X2) ) ).
cnf(u882,axiom,
p(enc(w,k)) ).
cnf(u887,axiom,
p(enc(w,pp)) ).
cnf(u891,axiom,
( p(enc(w,enc(i(enc(i(zcmk),X0)),X1)))
| ~ p(X1)
| ~ p(X0) ) ).
cnf(u895,axiom,
( p(enc(w,enc(i(tmk),X0)))
| ~ p(X0) ) ).
cnf(u899,axiom,
( p(enc(w,enc(i(tc),X0)))
| ~ p(X0) ) ).
cnf(u1001,axiom,
( p(enc(w,enc(i(enc(i(enc(i(zcmk),X0)),X1)),X2)))
| ~ p(X1)
| ~ p(X0)
| ~ p(X2) ) ).
cnf(u1006,axiom,
( p(enc(w,enc(i(pp),X0)))
| ~ p(X0) ) ).
cnf(u1012,axiom,
( p(enc(w,X0))
| ~ p(enc(pp,X0)) ) ).
cnf(u1174,axiom,
( p(enc(enc(i(tmk),X0),enc(i(enc(i(enc(i(zcmk),X1)),X2)),X3)))
| ~ p(X2)
| ~ p(X1)
| ~ p(X3)
| ~ p(X0) ) ).
cnf(u1178,axiom,
( p(enc(enc(i(tmk),X0),enc(i(w),X1)))
| ~ p(X1)
| ~ p(X0) ) ).
cnf(u1182,axiom,
( p(enc(enc(i(tmk),X0),enc(i(pp),X1)))
| ~ p(X1)
| ~ p(X0) ) ).
cnf(u1186,axiom,
( p(enc(enc(i(tmk),X0),X1))
| ~ p(enc(pp,X1))
| ~ p(X0) ) ).
cnf(u1190,axiom,
( p(enc(enc(i(tmk),X0),X1))
| ~ p(enc(w,X1))
| ~ p(X0) ) ).
cnf(u1393,axiom,
( p(enc(pp,enc(i(enc(i(zcmk),X0)),X1)))
| ~ p(X1)
| ~ p(X0) ) ).
cnf(u1439,axiom,
( p(enc(pp,enc(i(enc(i(enc(i(zcmk),X0)),X1)),X2)))
| ~ p(X1)
| ~ p(X0)
| ~ p(X2) ) ).
cnf(u1695,axiom,
( p(enc(enc(i(enc(i(zcmk),X0)),X1),t2))
| ~ p(X1)
| ~ p(X0) ) ).
cnf(u1699,axiom,
( p(enc(enc(i(enc(i(zcmk),X0)),X1),enc(i(enc(i(zcmk),X2)),X3)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ) ).
cnf(u1703,axiom,
( p(enc(enc(i(enc(i(zcmk),X0)),X1),enc(i(w),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ) ).
cnf(u1707,axiom,
( p(enc(enc(i(enc(i(zcmk),X0)),X1),enc(i(pp),X2)))
| ~ p(X2)
| ~ p(X1)
| ~ p(X0) ) ).
cnf(u1711,axiom,
( p(enc(enc(i(enc(i(zcmk),X0)),X1),X2))
| ~ p(enc(pp,X2))
| ~ p(X1)
| ~ p(X0) ) ).
cnf(u1715,axiom,
( p(enc(enc(i(enc(i(zcmk),X0)),X1),X2))
| ~ p(enc(w,X2))
| ~ p(X1)
| ~ p(X0) ) ).
cnf(u1766,axiom,
( p(enc(enc(i(enc(i(zcmk),X0)),X1),enc(i(enc(i(enc(i(zcmk),X2)),X3)),X4)))
| ~ p(X3)
| ~ p(X2)
| ~ p(X4)
| ~ p(X1)
| ~ p(X0) ) ).
cnf(u550,axiom,
( ~ p(enc(zcmk,X0))
| p(enc(i(X0),pp)) ) ).
cnf(u405,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X0) ) ).
cnf(u2409,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X1)
| ~ p(enc(tc,enc(i(enc(i(X0),X1)),X2)))
| p(X2) ) ).
cnf(u2298,axiom,
( ~ p(enc(zcmk,X0))
| p(enc(enc(i(tmk),X2),X3))
| ~ p(X2)
| ~ p(enc(X0,X1))
| ~ p(enc(X1,X3)) ) ).
cnf(u2088,axiom,
( ~ p(enc(enc(i(zcmk),X3),X0))
| p(enc(enc(i(enc(i(zcmk),X1)),X2),X0))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1) ) ).
cnf(u177,axiom,
( ~ p(enc(enc(i(tmk),X2),X0))
| ~ p(X2)
| p(enc(enc(i(wk),X1),X0))
| ~ p(X1) ) ).
cnf(u701,axiom,
( ~ p(enc(tmk,X0))
| p(enc(X0,enc(i(enc(i(zcmk),X1)),X2)))
| ~ p(X1)
| ~ p(X2) ) ).
cnf(u1916,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| p(enc(w,X2))
| ~ p(X1)
| ~ p(enc(X0,X2)) ) ).
cnf(u593,axiom,
( ~ p(enc(wk,X0))
| ~ p(X1)
| p(enc(X0,enc(i(pp),X1))) ) ).
cnf(u2082,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| p(enc(enc(i(X0),X1),enc(i(enc(i(zcmk),X2)),X3))) ) ).
cnf(u50,axiom,
enc(i(X0),enc(X0,X1)) = X1 ).
cnf(u1471,axiom,
( ~ p(enc(zcmk,X0))
| p(enc(enc(i(X0),X1),k))
| ~ p(X1) ) ).
cnf(u1485,axiom,
( ~ p(enc(zcmk,X0))
| p(enc(enc(i(X0),X1),pp))
| ~ p(X1) ) ).
cnf(u627,axiom,
p(enc(w,t2)) ).
cnf(u1155,axiom,
( ~ p(enc(wk,X0))
| p(enc(enc(i(tmk),X2),X1))
| ~ p(enc(X0,X1))
| ~ p(X2) ) ).
cnf(u1994,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X2)
| ~ p(X1)
| p(enc(enc(i(X0),X1),enc(i(pp),X2))) ) ).
cnf(u776,axiom,
( p(enc(enc(i(enc(i(zcmk),X0)),X1),pp))
| ~ p(X0)
| ~ p(X1) ) ).
cnf(u579,axiom,
( ~ p(enc(lp,X0))
| p(enc(enc(i(tmk),X1),X0))
| ~ p(X1) ) ).
cnf(u363,axiom,
( p(enc(enc(i(tmk),X0),enc(i(enc(i(zcmk),X1)),X2)))
| ~ p(X0)
| ~ p(X1)
| ~ p(X2) ) ).
cnf(u928,axiom,
( ~ p(enc(lp,enc(i(pp),X0)))
| p(X0) ) ).
cnf(u1281,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| p(enc(X0,enc(i(enc(i(wk),X2)),X3))) ) ).
cnf(u2251,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X2)
| p(enc(X1,enc(i(pp),X2)))
| ~ p(enc(X0,X1)) ) ).
cnf(u1268,axiom,
( ~ p(enc(tmk,X0))
| ~ p(X3)
| p(enc(enc(i(enc(i(zcmk),X1)),X2),enc(i(X0),X3)))
| ~ p(X1)
| ~ p(X2) ) ).
cnf(u696,axiom,
( ~ p(enc(tc,X0))
| p(X0) ) ).
cnf(u703,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X1)
| p(enc(enc(i(tmk),X1),enc(i(X0),X2)))
| ~ p(X2) ) ).
cnf(u1112,axiom,
( ~ p(enc(tmk,X0))
| p(enc(enc(i(tmk),X2),X1))
| ~ p(enc(X0,X1))
| ~ p(X2) ) ).
cnf(u2240,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X2)
| p(enc(X1,enc(i(w),X2)))
| ~ p(enc(X0,X1)) ) ).
cnf(u336,axiom,
( p(enc(enc(i(tmk),X0),enc(i(lp),X1)))
| ~ p(X1)
| ~ p(X0) ) ).
cnf(u531,axiom,
( p(enc(pp,X0))
| ~ p(enc(tmk,X0)) ) ).
cnf(u70,axiom,
p(kk) ).
cnf(u2084,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| ~ p(X3)
| ~ p(X2)
| p(enc(X0,enc(i(enc(i(zcmk),X2)),X3)))
| ~ p(X1) ) ).
cnf(u683,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X2)
| p(enc(enc(i(X0),X1),enc(i(tmk),X2)))
| ~ p(X1) ) ).
cnf(u482,axiom,
( ~ p(enc(tmk,X0))
| ~ p(X0) ) ).
cnf(u1988,axiom,
( ~ p(enc(tmk,X0))
| p(X1)
| ~ p(enc(lp,enc(i(X0),X1))) ) ).
cnf(u326,axiom,
( ~ p(enc(tc,X0))
| ~ p(enc(i(X0),X1))
| p(X1) ) ).
cnf(u2318,axiom,
( ~ p(enc(zcmk,X0))
| p(X2)
| ~ p(enc(w,enc(i(X1),X2)))
| ~ p(enc(X0,X1)) ) ).
cnf(u415,axiom,
( p(enc(w,enc(i(enc(i(tmk),X0)),X1)))
| ~ p(X1)
| ~ p(X0) ) ).
cnf(u2346,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| p(enc(enc(i(enc(i(zcmk),X3)),X4),X2))
| ~ p(X3)
| ~ p(X4)
| ~ p(X1)
| ~ p(enc(X0,X2)) ) ).
cnf(u635,axiom,
( ~ p(enc(wk,X0))
| ~ p(X1)
| p(enc(X0,enc(i(w),X1))) ) ).
cnf(u668,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X2)
| p(enc(enc(i(X0),X1),enc(i(tc),X2)))
| ~ p(X1) ) ).
cnf(u464,axiom,
( p(enc(enc(i(wk),X0),enc(i(w),X1)))
| ~ p(X1)
| ~ p(X0) ) ).
cnf(u52,axiom,
i(i(X0)) = X0 ).
cnf(u983,axiom,
( ~ p(enc(wk,X0))
| p(enc(w,X1))
| ~ p(enc(X0,X1)) ) ).
cnf(u910,axiom,
( ~ p(enc(wk,X0))
| ~ p(enc(pp,X1))
| p(enc(X0,X1)) ) ).
cnf(u73,negated_conjecture,
~ p(enc(pp,a)) ).
cnf(u1317,axiom,
( ~ p(enc(tmk,X1))
| p(enc(X1,X0))
| ~ p(enc(w,X0)) ) ).
cnf(u705,axiom,
( ~ p(enc(enc(i(zcmk),X2),X0))
| ~ p(X1)
| ~ p(X2)
| p(enc(enc(i(tmk),X1),X0)) ) ).
cnf(u1856,axiom,
( ~ p(enc(wk,X0))
| ~ p(enc(tmk,enc(i(X0),X1)))
| p(X1) ) ).
cnf(u67,axiom,
p(enc(w,t1)) ).
cnf(u167,axiom,
( ~ p(enc(zcmk,X0))
| p(enc(i(X0),enc(i(tmk),X1)))
| ~ p(X1) ) ).
cnf(u1450,axiom,
( ~ p(enc(pp,enc(i(enc(i(tmk),X1)),X0)))
| p(X0)
| ~ p(X1) ) ).
cnf(u416,axiom,
( p(enc(enc(i(tmk),X2),enc(i(enc(i(tmk),X0)),X1)))
| ~ p(X1)
| ~ p(X0)
| ~ p(X2) ) ).
cnf(u2260,axiom,
( ~ p(enc(zcmk,X0))
| p(X2)
| ~ p(X1)
| ~ p(enc(pp,enc(i(enc(i(X0),X1)),X2))) ) ).
cnf(u69,axiom,
p(enc(tc,k)) ).
cnf(u2411,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| ~ p(enc(tc,enc(i(X0),X2)))
| ~ p(X1)
| p(X2) ) ).
cnf(u219,axiom,
( ~ p(i(X1))
| p(enc(X1,X0))
| ~ p(X0) ) ).
cnf(u319,axiom,
( ~ p(enc(tc,X0))
| ~ p(enc(X0,X1))
| p(X1) ) ).
cnf(u349,axiom,
( p(enc(enc(i(enc(i(zcmk),X0)),X1),enc(i(tc),X2)))
| ~ p(X2)
| ~ p(X0)
| ~ p(X1) ) ).
cnf(u1494,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X1)
| p(enc(w,enc(i(X0),X1))) ) ).
cnf(u536,axiom,
( ~ p(enc(tmk,X0))
| p(enc(X0,pp)) ) ).
cnf(u629,axiom,
( ~ p(enc(tmk,X0))
| p(enc(X0,t2)) ) ).
cnf(u1496,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| p(enc(w,X0))
| ~ p(X1) ) ).
cnf(u2086,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X3)
| p(enc(enc(i(enc(i(zcmk),X1)),X2),enc(i(X0),X3)))
| ~ p(X2)
| ~ p(X1) ) ).
cnf(u2015,axiom,
( ~ p(enc(enc(i(enc(i(zcmk),X3)),X4),X2))
| p(enc(enc(i(enc(i(zcmk),X0)),X1),X2))
| ~ p(X0)
| ~ p(X1)
| ~ p(X3)
| ~ p(X4) ) ).
cnf(u2040,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| p(enc(enc(i(tmk),X3),X2))
| ~ p(X3)
| ~ p(X1)
| ~ p(enc(X0,X2)) ) ).
cnf(u1264,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X3)
| ~ p(X2)
| p(enc(enc(i(X0),X1),enc(i(enc(i(tmk),X2)),X3)))
| ~ p(X1) ) ).
cnf(u2366,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X1)
| ~ p(enc(lp,enc(i(enc(i(X0),X1)),X2)))
| p(X2) ) ).
cnf(u1325,axiom,
( ~ p(enc(w,X0))
| p(enc(pp,X0)) ) ).
cnf(u762,axiom,
( ~ p(enc(enc(i(zcmk),X2),X0))
| ~ p(X3)
| ~ p(X1)
| ~ p(X2)
| p(enc(enc(i(wk),X1),enc(i(X0),X3))) ) ).
cnf(u1266,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| ~ p(X3)
| ~ p(X2)
| ~ p(X1)
| p(enc(X0,enc(i(enc(i(tmk),X2)),X3))) ) ).
cnf(u621,axiom,
( ~ p(enc(wk,X0))
| ~ p(X1)
| p(enc(w,enc(i(X0),X1))) ) ).
cnf(u1238,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| p(enc(enc(i(wk),X3),X2))
| ~ p(X3)
| ~ p(X1)
| ~ p(enc(X0,X2)) ) ).
cnf(u1820,axiom,
( ~ p(enc(tmk,enc(i(enc(i(tmk),X1)),X0)))
| ~ p(X1)
| p(X0) ) ).
cnf(u1487,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| ~ p(X1)
| p(enc(X0,pp)) ) ).
cnf(u1210,axiom,
( ~ p(enc(enc(i(zcmk),X2),X0))
| ~ p(X1)
| ~ p(X2)
| p(enc(enc(i(wk),X1),X0)) ) ).
cnf(u1588,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1))
| p(enc(X1,pp)) ) ).
cnf(u2309,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X2)
| ~ p(X3)
| p(enc(X1,enc(i(enc(i(zcmk),X3)),X2)))
| ~ p(enc(X0,X1)) ) ).
cnf(u659,axiom,
( p(enc(pp,enc(i(enc(i(tmk),X1)),X0)))
| ~ p(X0)
| ~ p(X1) ) ).
cnf(u585,axiom,
( ~ p(enc(tmk,X0))
| ~ p(X1)
| p(enc(w,enc(i(X0),X1))) ) ).
cnf(u1040,axiom,
( ~ p(enc(wk,X0))
| ~ p(X1)
| p(enc(pp,enc(i(X0),X1))) ) ).
cnf(u602,axiom,
( ~ p(enc(wk,X0))
| ~ p(X1)
| p(enc(X0,enc(i(tmk),X1))) ) ).
cnf(u1047,axiom,
( p(enc(w,X0))
| ~ p(enc(tmk,X0)) ) ).
cnf(u648,axiom,
( ~ p(enc(tc,enc(i(pp),X0)))
| p(X0) ) ).
cnf(u1306,axiom,
( ~ p(enc(tmk,X1))
| p(enc(X1,X0))
| ~ p(enc(pp,X0)) ) ).
cnf(u460,axiom,
( p(enc(enc(i(tmk),X2),enc(i(enc(i(wk),X0)),X1)))
| ~ p(X1)
| ~ p(X0)
| ~ p(X2) ) ).
cnf(u1034,axiom,
( ~ p(enc(enc(i(tmk),X1),X0))
| p(enc(pp,X0))
| ~ p(X1) ) ).
cnf(u655,axiom,
p(enc(pp,k)) ).
cnf(u611,axiom,
( ~ p(enc(wk,X0))
| ~ p(X1)
| p(enc(X0,enc(i(tc),X1))) ) ).
cnf(u1955,axiom,
( ~ p(enc(w,enc(i(enc(i(enc(i(zcmk),X1)),X2)),X0)))
| p(X0)
| ~ p(X2)
| ~ p(X1) ) ).
cnf(u517,axiom,
( p(enc(pp,X0))
| ~ p(enc(tc,X0)) ) ).
cnf(u1806,axiom,
( ~ p(enc(tmk,X1))
| ~ p(enc(w,enc(i(X1),X0)))
| p(X0) ) ).
cnf(u1293,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1))
| ~ p(X1) ) ).
cnf(u362,axiom,
( p(enc(enc(i(tmk),X0),pp))
| ~ p(X0) ) ).
cnf(u587,axiom,
( ~ p(enc(enc(i(tmk),X1),X0))
| p(enc(w,X0))
| ~ p(X1) ) ).
cnf(u173,axiom,
( ~ p(enc(wk,X0))
| ~ p(X1)
| ~ p(X2)
| p(enc(X0,enc(i(enc(i(tmk),X1)),X2))) ) ).
cnf(u2169,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(enc(pp,X2))
| p(enc(X1,X2))
| ~ p(enc(X0,X1)) ) ).
cnf(u2224,axiom,
( ~ p(enc(zcmk,X0))
| p(enc(pp,enc(i(X1),X2)))
| ~ p(enc(X0,X1))
| ~ p(X2) ) ).
cnf(u2199,axiom,
( ~ p(enc(zcmk,X0))
| p(enc(pp,X2))
| ~ p(enc(enc(i(X0),X1),X2))
| ~ p(X1) ) ).
cnf(u2262,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| p(X2)
| ~ p(enc(pp,enc(i(X0),X2)))
| ~ p(X1) ) ).
cnf(u358,axiom,
( p(enc(pp,enc(i(tmk),X0)))
| ~ p(X0) ) ).
cnf(u197,axiom,
( p(enc(i(kk),X0))
| ~ p(X0) ) ).
cnf(u154,axiom,
( ~ p(enc(tmk,enc(i(wk),X0)))
| p(X0) ) ).
cnf(u123,axiom,
( ~ p(i(X1))
| p(X0)
| ~ p(enc(X1,X0)) ) ).
cnf(u1340,axiom,
p(enc(pp,t1)) ).
cnf(u314,axiom,
( p(enc(i(k),X0))
| ~ p(X0) ) ).
cnf(u2158,axiom,
( ~ p(enc(zcmk,X0))
| p(enc(w,X2))
| ~ p(enc(X0,X1))
| ~ p(enc(X1,X2)) ) ).
cnf(u1849,axiom,
( ~ p(enc(wk,X0))
| ~ p(enc(lp,enc(i(X0),X1)))
| p(X1) ) ).
cnf(u125,negated_conjecture,
~ p(pp) ).
cnf(u758,axiom,
( ~ p(enc(wk,X0))
| ~ p(X3)
| p(enc(X0,enc(i(enc(i(enc(i(zcmk),X1)),X2)),X3)))
| ~ p(X1)
| ~ p(X2) ) ).
cnf(u150,axiom,
( ~ p(enc(tc,X0))
| ~ p(X1)
| p(enc(enc(i(tmk),X1),X0)) ) ).
cnf(u340,axiom,
( p(enc(enc(i(wk),X0),t2))
| ~ p(X0) ) ).
cnf(u136,axiom,
( ~ p(enc(tc,X0))
| p(enc(i(X0),X1))
| ~ p(X1) ) ).
cnf(u1996,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| ~ p(X2)
| p(enc(X0,enc(i(pp),X2)))
| ~ p(X1) ) ).
cnf(u1610,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X2)
| ~ p(enc(X0,X1))
| p(enc(enc(i(wk),X2),X1)) ) ).
cnf(u334,axiom,
( ~ p(enc(i(k),X0))
| p(X0) ) ).
cnf(u1943,axiom,
( ~ p(enc(pp,enc(i(enc(i(enc(i(zcmk),X1)),X2)),X0)))
| p(X0)
| ~ p(X2)
| ~ p(X1) ) ).
cnf(u129,axiom,
( p(enc(wk,X0))
| ~ p(enc(tmk,X0)) ) ).
cnf(u132,axiom,
( ~ p(enc(tc,X0))
| p(enc(X0,X1))
| ~ p(X1) ) ).
cnf(u733,axiom,
( ~ p(enc(wk,X0))
| ~ p(X2)
| p(enc(enc(i(tmk),X1),enc(i(X0),X2)))
| ~ p(X1) ) ).
cnf(u51,axiom,
enc(X0,enc(i(X0),X1)) = X1 ).
cnf(u1503,axiom,
( ~ p(enc(tmk,enc(i(enc(i(wk),X1)),X0)))
| ~ p(X1)
| p(X0) ) ).
cnf(u53,axiom,
( p(i(X0))
| ~ p(X0) ) ).
cnf(u2072,axiom,
( ~ p(enc(zcmk,X0))
| p(enc(X1,t2))
| ~ p(enc(X0,X1)) ) ).
cnf(u685,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| ~ p(X2)
| ~ p(X1)
| p(enc(X0,enc(i(tmk),X2))) ) ).
cnf(u2066,axiom,
( ~ p(enc(tmk,X0))
| p(X1)
| ~ p(enc(tc,enc(i(X0),X1))) ) ).
cnf(u837,axiom,
( ~ p(enc(i(kk),X0))
| p(X0) ) ).
cnf(u1502,axiom,
( ~ p(enc(lp,enc(i(enc(i(wk),X1)),X0)))
| ~ p(X1)
| p(X0) ) ).
cnf(u1821,axiom,
( ~ p(enc(tc,enc(i(enc(i(tmk),X1)),X0)))
| ~ p(X1)
| p(X0) ) ).
cnf(u637,axiom,
( p(enc(enc(i(wk),X1),X0))
| ~ p(enc(w,X0))
| ~ p(X1) ) ).
cnf(u1270,axiom,
( ~ p(enc(enc(i(tmk),X3),X0))
| p(enc(enc(i(enc(i(zcmk),X1)),X2),X0))
| ~ p(X3)
| ~ p(X1)
| ~ p(X2) ) ).
cnf(u1504,axiom,
( ~ p(enc(tc,enc(i(enc(i(wk),X1)),X0)))
| ~ p(X1)
| p(X0) ) ).
cnf(u359,axiom,
( p(enc(enc(i(enc(i(zcmk),X0)),X1),enc(i(tmk),X2)))
| ~ p(X2)
| ~ p(X0)
| ~ p(X1) ) ).
cnf(u1419,axiom,
( ~ p(enc(wk,X0))
| p(enc(pp,X1))
| ~ p(enc(X0,X1)) ) ).
cnf(u1067,axiom,
( ~ p(enc(tc,enc(i(w),X0)))
| p(X0) ) ).
cnf(u735,axiom,
( ~ p(enc(enc(i(wk),X2),X0))
| p(enc(enc(i(tmk),X1),X0))
| ~ p(X2)
| ~ p(X1) ) ).
cnf(u1279,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X3)
| ~ p(X2)
| p(enc(enc(i(X0),X1),enc(i(enc(i(wk),X2)),X3)))
| ~ p(X1) ) ).
cnf(u672,axiom,
( ~ p(enc(tc,X0))
| p(enc(enc(i(enc(i(zcmk),X1)),X2),X0))
| ~ p(X1)
| ~ p(X2) ) ).
cnf(u1745,axiom,
( ~ p(enc(wk,X0))
| p(enc(enc(i(enc(i(zcmk),X2)),X3),X1))
| ~ p(enc(X0,X1))
| ~ p(X2)
| ~ p(X3) ) ).
cnf(u912,axiom,
( ~ p(enc(pp,enc(i(enc(i(wk),X1)),X0)))
| p(X0)
| ~ p(X1) ) ).
cnf(u71,axiom,
p(i(kk)) ).
cnf(u1094,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X2)
| ~ p(enc(X0,X1))
| p(enc(enc(i(tmk),X2),X1)) ) ).
cnf(u1193,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X2)
| p(enc(enc(i(X0),X1),enc(i(lp),X2)))
| ~ p(X1) ) ).
cnf(u2201,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| p(enc(pp,X2))
| ~ p(X1)
| ~ p(enc(X0,X2)) ) ).
cnf(u867,axiom,
( ~ p(enc(tmk,X0))
| p(enc(w,X1))
| ~ p(enc(X0,X1)) ) ).
cnf(u687,axiom,
( ~ p(enc(tmk,X0))
| p(enc(enc(i(enc(i(zcmk),X1)),X2),X0))
| ~ p(X1)
| ~ p(X2) ) ).
cnf(u570,axiom,
( p(enc(enc(i(enc(i(zcmk),X1)),X2),enc(i(lp),X0)))
| ~ p(X0)
| ~ p(X1)
| ~ p(X2) ) ).
cnf(u1654,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X2)
| ~ p(X3)
| ~ p(enc(X0,X1))
| p(enc(X1,enc(i(enc(i(tmk),X3)),X2))) ) ).
cnf(u2038,axiom,
( ~ p(enc(zcmk,X0))
| p(enc(enc(i(tmk),X3),X2))
| ~ p(X3)
| ~ p(enc(enc(i(X0),X1),X2))
| ~ p(X1) ) ).
cnf(u2378,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X2)
| ~ p(X3)
| ~ p(X4)
| p(enc(X1,enc(i(enc(i(enc(i(zcmk),X3)),X2)),X4)))
| ~ p(enc(X0,X1)) ) ).
cnf(u2104,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| ~ p(X3)
| ~ p(X2)
| ~ p(X4)
| p(enc(X0,enc(i(enc(i(enc(i(zcmk),X2)),X3)),X4)))
| ~ p(X1) ) ).
cnf(u1016,axiom,
( ~ p(enc(tmk,X1))
| p(enc(X1,enc(i(w),X0)))
| ~ p(X0) ) ).
cnf(u813,axiom,
( p(enc(pp,X0))
| ~ p(enc(lp,X0)) ) ).
cnf(u1055,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X2)
| ~ p(enc(X0,X1))
| p(enc(X1,enc(i(tc),X2))) ) ).
cnf(u656,axiom,
( p(enc(enc(i(enc(i(zcmk),X0)),X1),k))
| ~ p(X0)
| ~ p(X1) ) ).
cnf(u1042,axiom,
( ~ p(enc(enc(i(wk),X1),X0))
| p(enc(pp,X0))
| ~ p(X1) ) ).
cnf(u663,axiom,
( p(enc(pp,enc(i(enc(i(wk),X1)),X0)))
| ~ p(X0)
| ~ p(X1) ) ).
cnf(u628,axiom,
( p(enc(enc(i(tmk),X0),t2))
| ~ p(X0) ) ).
cnf(u424,axiom,
( p(enc(enc(i(wk),X0),enc(i(enc(i(enc(i(zcmk),X1)),X2)),X3)))
| ~ p(X3)
| ~ p(X0)
| ~ p(X1)
| ~ p(X2) ) ).
cnf(u619,axiom,
( ~ p(enc(lp,enc(i(w),X0)))
| p(X0) ) ).
cnf(u1645,axiom,
( ~ p(enc(zcmk,X0))
| p(enc(w,X1))
| ~ p(enc(X0,X1)) ) ).
cnf(u771,negated_conjecture,
~ p(enc(tmk,a)) ).
cnf(u2231,axiom,
( ~ p(enc(zcmk,X0))
| p(enc(pp,X2))
| ~ p(enc(X0,X1))
| ~ p(enc(X1,X2)) ) ).
cnf(u1953,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| ~ p(enc(w,X2))
| p(enc(X0,X2))
| ~ p(X1) ) ).
cnf(u186,axiom,
( ~ p(enc(enc(i(wk),X2),X0))
| ~ p(X2)
| p(enc(enc(i(wk),X1),X0))
| ~ p(X1) ) ).
cnf(u1814,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| p(enc(pp,X0))
| ~ p(X1) ) ).
cnf(u1301,axiom,
( ~ p(enc(enc(i(enc(i(zcmk),X1)),X2),X0))
| p(enc(w,X0))
| ~ p(X1)
| ~ p(X2) ) ).
cnf(u2445,axiom,
( ~ p(enc(zcmk,X0))
| p(enc(enc(i(enc(i(zcmk),X2)),X3),X4))
| ~ p(X2)
| ~ p(X3)
| ~ p(enc(X0,X1))
| ~ p(enc(X1,X4)) ) ).
cnf(u337,axiom,
( ~ p(enc(tmk,X0))
| ~ p(X1)
| p(enc(X0,enc(i(lp),X1))) ) ).
cnf(u157,axiom,
( ~ p(enc(tmk,X0))
| ~ p(X1)
| p(enc(enc(i(tmk),X1),X0)) ) ).
cnf(u2401,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| ~ p(enc(tmk,enc(i(X0),X2)))
| ~ p(X1)
| p(X2) ) ).
cnf(u182,axiom,
( ~ p(enc(wk,X0))
| ~ p(X1)
| ~ p(X2)
| p(enc(X0,enc(i(enc(i(wk),X1)),X2))) ) ).
cnf(u194,axiom,
( ~ p(enc(X1,X0))
| p(X0)
| ~ p(X1) ) ).
cnf(u2325,axiom,
( ~ p(enc(zcmk,X0))
| p(enc(enc(i(enc(i(zcmk),X2)),X3),X1))
| ~ p(enc(X0,X1))
| ~ p(X3)
| ~ p(X2) ) ).
cnf(u175,axiom,
( ~ p(enc(tmk,X0))
| p(enc(enc(i(wk),X1),enc(i(X0),X2)))
| ~ p(X2)
| ~ p(X1) ) ).
cnf(u161,axiom,
( ~ p(enc(zcmk,X0))
| p(enc(tmk,enc(i(X0),X1)))
| ~ p(X1) ) ).
cnf(u1787,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X2)
| p(enc(enc(i(tmk),X1),enc(i(enc(i(X0),X2)),X3)))
| ~ p(X3)
| ~ p(X1) ) ).
cnf(u569,axiom,
( p(enc(pp,enc(i(lp),X0)))
| ~ p(X0) ) ).
cnf(u2399,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X1)
| ~ p(enc(tmk,enc(i(enc(i(X0),X1)),X2)))
| p(X2) ) ).
cnf(u441,axiom,
( ~ p(enc(tmk,X0))
| ~ p(enc(X0,X1))
| p(enc(enc(i(wk),X2),X1))
| ~ p(X2) ) ).
cnf(u1248,axiom,
( ~ p(enc(tmk,X1))
| p(enc(X1,enc(i(enc(i(enc(i(zcmk),X2)),X3)),X0)))
| ~ p(X2)
| ~ p(X3)
| ~ p(X0) ) ).
cnf(u566,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(i(X0)) ) ).
cnf(u1195,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| ~ p(X2)
| ~ p(X1)
| p(enc(X0,enc(i(lp),X2))) ) ).
cnf(u1620,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| p(enc(w,enc(i(X0),X2)))
| ~ p(X1)
| ~ p(X2) ) ).
cnf(u335,axiom,
( p(enc(w,enc(i(lp),X0)))
| ~ p(X0) ) ).
cnf(u1197,axiom,
( ~ p(enc(lp,X0))
| p(enc(enc(i(enc(i(zcmk),X1)),X2),X0))
| ~ p(X1)
| ~ p(X2) ) ).
cnf(u1951,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(enc(w,X2))
| ~ p(X1)
| p(enc(enc(i(X0),X1),X2)) ) ).
cnf(u1886,axiom,
( ~ p(enc(zcmk,X0))
| p(enc(pp,X1))
| ~ p(enc(X0,X1)) ) ).
cnf(u1224,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X2)
| ~ p(enc(X0,X1))
| p(enc(i(enc(i(zcmk),X2)),X1)) ) ).
cnf(u2421,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(enc(tmk,enc(i(X1),X2)))
| ~ p(enc(X0,X1))
| p(X2) ) ).
cnf(u643,axiom,
( ~ p(enc(enc(i(enc(i(zcmk),X0)),X1),X2))
| p(enc(enc(i(wk),X3),X2))
| ~ p(X3)
| ~ p(X0)
| ~ p(X1) ) ).
cnf(u1378,axiom,
( ~ p(enc(tmk,X0))
| p(enc(pp,X1))
| ~ p(enc(X0,X1)) ) ).
cnf(u1236,axiom,
( ~ p(enc(zcmk,X0))
| p(enc(enc(i(wk),X3),X2))
| ~ p(X3)
| ~ p(enc(enc(i(X0),X1),X2))
| ~ p(X1) ) ).
cnf(u760,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X3)
| ~ p(X1)
| p(enc(enc(i(wk),X1),enc(i(enc(i(X0),X2)),X3)))
| ~ p(X2) ) ).
cnf(u821,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(enc(i(X0),X1))
| ~ p(X1) ) ).
cnf(u1575,axiom,
( ~ p(enc(enc(i(enc(i(zcmk),X2)),X3),X1))
| p(enc(enc(i(tmk),X0),X1))
| ~ p(X0)
| ~ p(X2)
| ~ p(X3) ) ).
cnf(u604,axiom,
( ~ p(enc(tmk,X0))
| p(enc(enc(i(wk),X1),X0))
| ~ p(X1) ) ).
cnf(u522,axiom,
( ~ p(enc(tmk,X0))
| p(enc(X0,k)) ) ).
cnf(u595,axiom,
( p(enc(enc(i(wk),X1),X0))
| ~ p(enc(pp,X0))
| ~ p(X1) ) ).
cnf(u394,axiom,
( p(enc(i(enc(i(zcmk),X0)),enc(i(enc(i(zcmk),X1)),X2)))
| ~ p(X0)
| ~ p(X1)
| ~ p(X2) ) ).
cnf(u1463,axiom,
( ~ p(enc(w,enc(i(enc(i(tmk),X1)),X0)))
| p(X0)
| ~ p(X1) ) ).
cnf(u747,axiom,
( ~ p(enc(enc(i(zcmk),X2),X0))
| ~ p(X1)
| ~ p(X2)
| p(enc(i(enc(i(zcmk),X1)),X0)) ) ).
cnf(u1962,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X1)
| p(enc(pp,enc(i(enc(i(X0),X1)),X2)))
| ~ p(X2) ) ).
cnf(u1896,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| p(enc(X0,t2))
| ~ p(X1) ) ).
cnf(u1819,axiom,
( ~ p(enc(lp,enc(i(enc(i(tmk),X1)),X0)))
| ~ p(X1)
| p(X0) ) ).
cnf(u2256,axiom,
( ~ p(enc(lp,enc(i(enc(i(enc(i(zcmk),X2)),X1)),X0)))
| ~ p(X1)
| ~ p(X2)
| p(X0) ) ).
cnf(u352,axiom,
( p(enc(enc(i(tmk),X0),k))
| ~ p(X0) ) ).
cnf(u1939,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(enc(pp,X2))
| ~ p(X1)
| p(enc(enc(i(X0),X1),X2)) ) ).
cnf(u1075,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X2)
| ~ p(enc(X0,X1))
| p(enc(X1,enc(i(tmk),X2))) ) ).
cnf(u155,axiom,
( ~ p(enc(tmk,X0))
| p(enc(X0,enc(i(tmk),X1)))
| ~ p(X1) ) ).
cnf(u2178,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(enc(w,X2))
| p(enc(X1,X2))
| ~ p(enc(X0,X1)) ) ).
cnf(u1914,axiom,
( ~ p(enc(zcmk,X0))
| p(enc(w,X2))
| ~ p(enc(enc(i(X0),X1),X2))
| ~ p(X1) ) ).
cnf(u1023,axiom,
( ~ p(enc(wk,X0))
| ~ p(enc(w,X1))
| p(enc(X0,X1)) ) ).
cnf(u348,axiom,
( p(enc(pp,enc(i(tc),X0)))
| ~ p(X0) ) ).
cnf(u1618,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X1)
| p(enc(w,enc(i(enc(i(X0),X1)),X2)))
| ~ p(X2) ) ).
cnf(u1401,axiom,
( ~ p(enc(enc(i(enc(i(zcmk),X1)),X2),X0))
| p(enc(pp,X0))
| ~ p(X1)
| ~ p(X2) ) ).
cnf(u144,axiom,
( ~ p(enc(lp,X0))
| ~ p(X1)
| p(enc(enc(i(wk),X1),X0)) ) ).
cnf(u459,axiom,
( p(enc(w,enc(i(enc(i(wk),X0)),X1)))
| ~ p(X1)
| ~ p(X0) ) ).
cnf(u823,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| ~ p(X1)
| ~ p(X0) ) ).
cnf(u138,axiom,
( ~ p(enc(enc(i(tc),X1),X0))
| ~ p(X1)
| p(X0) ) ).
cnf(u461,axiom,
( ~ p(enc(tmk,X2))
| ~ p(X1)
| p(enc(X2,enc(i(enc(i(wk),X0)),X1)))
| ~ p(X0) ) ).
cnf(u417,axiom,
( ~ p(enc(tmk,X2))
| ~ p(X1)
| p(enc(X2,enc(i(enc(i(tmk),X0)),X1)))
| ~ p(X0) ) ).
cnf(u134,axiom,
( ~ p(enc(i(enc(i(tc),X1)),X0))
| ~ p(X1)
| p(X0) ) ).
cnf(u2293,axiom,
( ~ p(enc(zcmk,X0))
| p(X2)
| ~ p(enc(pp,enc(i(X1),X2)))
| ~ p(enc(X0,X1)) ) ).
cnf(u512,axiom,
( ~ p(enc(wk,X0))
| p(enc(X0,t2)) ) ).
cnf(u2280,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| p(X2)
| ~ p(enc(w,enc(i(X0),X2)))
| ~ p(X1) ) ).
cnf(u926,negated_conjecture,
~ p(enc(lp,a)) ).
cnf(u383,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1))
| p(enc(tmk,X1)) ) ).
cnf(u62,axiom,
( p(enc(enc(i(wk),X2),enc(i(enc(i(wk),X1)),X0)))
| ~ p(X1)
| ~ p(X0)
| ~ p(X2) ) ).
cnf(u721,axiom,
( ~ p(enc(enc(i(tmk),X2),X0))
| p(enc(enc(i(tmk),X1),X0))
| ~ p(X2)
| ~ p(X1) ) ).
cnf(u61,axiom,
( p(enc(enc(i(wk),X2),enc(i(enc(i(tmk),X1)),X0)))
| ~ p(X1)
| ~ p(X0)
| ~ p(X2) ) ).
cnf(u169,axiom,
( ~ p(enc(tmk,X0))
| ~ p(X1)
| p(enc(i(enc(i(zcmk),X1)),X0)) ) ).
cnf(u1720,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X2)
| ~ p(X3)
| ~ p(enc(X0,X1))
| p(enc(X1,enc(i(enc(i(wk),X3)),X2))) ) ).
cnf(u1516,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(enc(X0,X1))
| p(enc(X1,k)) ) ).
cnf(u393,axiom,
( p(enc(i(enc(i(zcmk),X0)),pp))
| ~ p(X0) ) ).
cnf(u2106,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X3)
| p(enc(enc(i(enc(i(zcmk),X1)),X2),enc(i(enc(i(X0),X3)),X4)))
| ~ p(X4)
| ~ p(X2)
| ~ p(X1) ) ).
cnf(u72,axiom,
p(a) ).
cnf(u779,axiom,
( p(enc(kk,X0))
| ~ p(X0) ) ).
cnf(u1932,axiom,
( ~ p(enc(zcmk,X0))
| p(enc(w,enc(i(X1),X2)))
| ~ p(enc(X0,X1))
| ~ p(X2) ) ).
cnf(u2108,axiom,
( ~ p(enc(enc(i(zcmk),X3),X0))
| p(enc(enc(i(enc(i(zcmk),X1)),X2),enc(i(X0),X4)))
| ~ p(X3)
| ~ p(X4)
| ~ p(X2)
| ~ p(X1) ) ).
cnf(u66,axiom,
p(enc(wk,w)) ).
cnf(u1976,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| ~ p(X2)
| p(enc(X0,enc(i(w),X2)))
| ~ p(X1) ) ).
cnf(u65,axiom,
p(enc(tmk,pp)) ).
cnf(u2102,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X3)
| ~ p(X2)
| ~ p(X4)
| ~ p(X1)
| p(enc(enc(i(X0),X1),enc(i(enc(i(enc(i(zcmk),X2)),X3)),X4))) ) ).
cnf(u68,axiom,
p(enc(lp,t2)) ).
cnf(u670,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| ~ p(X2)
| ~ p(X1)
| p(enc(X0,enc(i(tc),X2))) ) ).
cnf(u345,axiom,
( ~ p(enc(k,X0))
| p(X0) ) ).
cnf(u1473,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| ~ p(X1)
| p(enc(X0,k)) ) ).
cnf(u1506,axiom,
( ~ p(enc(wk,X0))
| p(X1)
| ~ p(enc(pp,enc(i(X0),X1))) ) ).
cnf(u1051,axiom,
( ~ p(enc(tmk,enc(i(w),X0)))
| p(X0) ) ).
cnf(u311,axiom,
( p(enc(k,X0))
| ~ p(X0) ) ).
cnf(u1676,axiom,
( ~ p(enc(tmk,X0))
| p(enc(enc(i(enc(i(zcmk),X2)),X3),X1))
| ~ p(enc(X0,X1))
| ~ p(X2)
| ~ p(X3) ) ).
cnf(u1867,axiom,
( ~ p(enc(wk,X0))
| ~ p(enc(tc,enc(i(X0),X1)))
| p(X1) ) ).
cnf(u148,axiom,
( ~ p(enc(tmk,X0))
| p(enc(X0,enc(i(tc),X1)))
| ~ p(X1) ) ).
cnf(u773,axiom,
( ~ p(enc(tmk,enc(i(pp),X0)))
| p(X0) ) ).
cnf(u719,axiom,
( ~ p(enc(tmk,X0))
| ~ p(X2)
| p(enc(enc(i(tmk),X1),enc(i(X0),X2)))
| ~ p(X1) ) ).
cnf(u806,axiom,
( ~ p(enc(wk,X0))
| p(enc(X0,pp)) ) ).
cnf(u1256,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X2)
| ~ p(X3)
| ~ p(enc(X0,X1))
| p(enc(enc(i(wk),X3),enc(i(X1),X2))) ) ).
cnf(u1595,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X2)
| ~ p(enc(X0,X1))
| p(enc(X1,enc(i(lp),X2))) ) ).
cnf(u1206,axiom,
( ~ p(enc(wk,X0))
| p(enc(X0,enc(i(enc(i(zcmk),X1)),X2)))
| ~ p(X1)
| ~ p(X2) ) ).
cnf(u1344,axiom,
( p(enc(pp,enc(i(w),X0)))
| ~ p(X0) ) ).
cnf(u2009,axiom,
( ~ p(enc(tmk,X0))
| p(X1)
| ~ p(enc(tmk,enc(i(X0),X1))) ) ).
cnf(u1063,axiom,
( p(enc(w,X0))
| ~ p(enc(tc,X0)) ) ).
cnf(u664,axiom,
( p(enc(enc(i(enc(i(zcmk),X1)),X2),enc(i(enc(i(wk),X3)),X0)))
| ~ p(X0)
| ~ p(X3)
| ~ p(X1)
| ~ p(X2) ) ).
cnf(u1862,axiom,
( ~ p(enc(w,enc(i(pp),X0)))
| p(X0) ) ).
cnf(u1894,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X1)
| p(enc(enc(i(X0),X1),t2)) ) ).
cnf(u1208,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X1)
| p(enc(enc(i(wk),X1),enc(i(X0),X2)))
| ~ p(X2) ) ).
cnf(u2368,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| ~ p(enc(lp,enc(i(X0),X2)))
| ~ p(X1)
| p(X2) ) ).
cnf(u660,axiom,
( p(enc(enc(i(enc(i(zcmk),X1)),X2),enc(i(enc(i(tmk),X3)),X0)))
| ~ p(X0)
| ~ p(X3)
| ~ p(X1)
| ~ p(X2) ) ).
cnf(u745,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X1)
| p(enc(i(enc(i(zcmk),X1)),enc(i(X0),X2)))
| ~ p(X2) ) ).
cnf(u1030,axiom,
( ~ p(enc(pp,enc(i(w),X0)))
| p(X0) ) ).
cnf(u428,axiom,
( ~ p(enc(wk,X0))
| ~ p(X0) ) ).
cnf(u623,axiom,
( ~ p(enc(enc(i(wk),X1),X0))
| p(enc(w,X0))
| ~ p(X1) ) ).
cnf(u1789,axiom,
( ~ p(enc(enc(i(zcmk),X2),X0))
| p(enc(enc(i(tmk),X1),enc(i(X0),X3)))
| ~ p(X2)
| ~ p(X3)
| ~ p(X1) ) ).
cnf(u1032,axiom,
( ~ p(enc(tmk,X0))
| ~ p(X1)
| p(enc(pp,enc(i(X0),X1))) ) ).
cnf(u844,axiom,
p(enc(pp,t2)) ).
cnf(u1528,axiom,
( ~ p(enc(wk,X0))
| p(X1)
| ~ p(enc(w,enc(i(X0),X1))) ) ).
cnf(u775,axiom,
p(enc(pp,pp)) ).
cnf(u1941,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| ~ p(enc(pp,X2))
| p(enc(X0,X2))
| ~ p(X1) ) ).
cnf(u800,axiom,
( ~ p(enc(wk,X0))
| p(enc(X0,k)) ) ).
cnf(u1974,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X2)
| ~ p(X1)
| p(enc(enc(i(X0),X1),enc(i(w),X2))) ) ).
cnf(u1025,axiom,
( ~ p(enc(w,enc(i(enc(i(wk),X1)),X0)))
| p(X0)
| ~ p(X1) ) ).
cnf(u220,axiom,
( p(enc(i(X1),X0))
| ~ p(X0)
| ~ p(X1) ) ).
cnf(u497,axiom,
( p(enc(w,X0))
| ~ p(enc(lp,X0)) ) ).
cnf(u2278,axiom,
( ~ p(enc(zcmk,X0))
| p(X2)
| ~ p(X1)
| ~ p(enc(w,enc(i(enc(i(X0),X1)),X2))) ) ).
cnf(u1283,axiom,
( ~ p(enc(wk,X0))
| ~ p(X3)
| p(enc(enc(i(enc(i(zcmk),X1)),X2),enc(i(X0),X3)))
| ~ p(X1)
| ~ p(X2) ) ).
cnf(u2436,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(enc(tc,enc(i(X1),X2)))
| ~ p(enc(X0,X1))
| p(X2) ) ).
cnf(u2392,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(enc(lp,enc(i(X1),X2)))
| ~ p(enc(X0,X1))
| p(X2) ) ).
cnf(u1285,axiom,
( ~ p(enc(enc(i(wk),X3),X0))
| p(enc(enc(i(enc(i(zcmk),X1)),X2),X0))
| ~ p(X3)
| ~ p(X1)
| ~ p(X2) ) ).
cnf(u2258,axiom,
( ~ p(enc(tc,enc(i(enc(i(enc(i(zcmk),X2)),X1)),X0)))
| ~ p(X1)
| ~ p(X2)
| p(X0) ) ).
cnf(u646,negated_conjecture,
~ p(enc(tc,a)) ).
cnf(u163,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| ~ p(X1)
| p(enc(tmk,X0)) ) ).
cnf(u2385,axiom,
( ~ p(enc(zcmk,X0))
| p(enc(enc(i(enc(i(zcmk),X2)),X3),enc(i(X1),X4)))
| ~ p(enc(X0,X1))
| ~ p(X4)
| ~ p(X3)
| ~ p(X2) ) ).
cnf(u193,axiom,
( ~ p(enc(kk,X0))
| p(X0) ) ).
cnf(u2257,axiom,
( ~ p(enc(tmk,enc(i(enc(i(enc(i(zcmk),X2)),X1)),X0)))
| ~ p(X1)
| ~ p(X2)
| p(X0) ) ).
cnf(u423,axiom,
( p(enc(enc(i(wk),X0),enc(i(pp),X1)))
| ~ p(X1)
| ~ p(X0) ) ).
cnf(u142,axiom,
( ~ p(enc(wk,X0))
| p(enc(X0,enc(i(lp),X1)))
| ~ p(X1) ) ).
cnf(u473,axiom,
( ~ p(enc(wk,X0))
| ~ p(enc(X0,X1))
| p(enc(enc(i(wk),X2),X1))
| ~ p(X2) ) ).
cnf(u2344,axiom,
( ~ p(enc(zcmk,X0))
| p(enc(enc(i(enc(i(zcmk),X3)),X4),X2))
| ~ p(X3)
| ~ p(X4)
| ~ p(enc(enc(i(X0),X1),X2))
| ~ p(X1) ) ).
cnf(u124,axiom,
( ~ p(enc(i(X1),X0))
| ~ p(X1)
| p(X0) ) ).
cnf(u743,axiom,
( ~ p(enc(zcmk,X0))
| p(enc(i(X0),enc(i(enc(i(zcmk),X1)),X2)))
| ~ p(X1)
| ~ p(X2) ) ).
cnf(u2060,axiom,
( ~ p(enc(zcmk,X0))
| p(enc(enc(i(tmk),X2),enc(i(X1),X3)))
| ~ p(enc(X0,X1))
| ~ p(X3)
| ~ p(X2) ) ).
cnf(u1812,axiom,
( ~ p(enc(zcmk,X0))
| ~ p(X1)
| p(enc(pp,enc(i(X0),X1))) ) ).
cnf(u905,axiom,
( ~ p(enc(tmk,X1))
| p(enc(X1,enc(i(pp),X0)))
| ~ p(X0) ) ).
cnf(u613,axiom,
( ~ p(enc(tc,X0))
| p(enc(enc(i(wk),X1),X0))
| ~ p(X1) ) ).
cnf(u117,axiom,
( ~ p(i(X0))
| p(X0) ) ).
cnf(u1631,axiom,
( ~ p(enc(zcmk,X0))
| p(enc(enc(i(wk),X2),X3))
| ~ p(X2)
| ~ p(enc(X0,X1))
| ~ p(enc(X1,X3)) ) ).
cnf(u1964,axiom,
( ~ p(enc(enc(i(zcmk),X1),X0))
| p(enc(pp,enc(i(X0),X2)))
| ~ p(X1)
| ~ p(X2) ) ).
cnf(u184,axiom,
( ~ p(enc(wk,X0))
| p(enc(enc(i(wk),X1),enc(i(X0),X2)))
| ~ p(X2)
| ~ p(X1) ) ).
cnf(u1776,axiom,
( ~ p(enc(tmk,X1))
| ~ p(enc(pp,enc(i(X1),X0)))
| p(X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV238+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.25/0.30 % Computer : n010.cluster.edu
% 0.25/0.30 % Model : x86_64 x86_64
% 0.25/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.25/0.30 % Memory : 8046.5625MB
% 0.25/0.30 % OS : Linux 6.8.0-71-generic
% 0.25/0.30 % CPULimit : 300
% 0.25/0.30 % WCLimit : 300
% 0.25/0.30 % DateTime : Mon Sep 28 10:14:47 UTC 2026
% 0.25/0.31 % CPUTime :
% 0.25/0.31 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.25/0.36 Running first-order model finding
% 0.25/0.36 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.20/0.59 % (1827744)Will run a generic schedule for satisfiability detection.
% 1.20/0.59 % (1827749)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2934807553_2999 on theBenchmark for (2999ds/0Mi)
% 1.20/0.59 % TRYING [1]
% 1.20/0.59 % TRYING [2]
% 1.20/0.59 % TRYING [3]
% 1.20/0.59 % TRYING [4]
% 1.20/0.59 % (1827750)% WARNING: option uhcvi not known.
% 1.20/0.59 % (1827750)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3477310778:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.20/0.59 % (1827753)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=502563207:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.20/0.59 % (1827754)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3940024082:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.20/0.59 % (1827752)dis+10_1_sil=32000:sp=arity:random_seed=672469549:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.20/0.59 % (1827751)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2414361476:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.20/0.59 % (1827755)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=441423600:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.20/0.59 % TRYING [5]
% 1.20/0.59 % (1827754)Instruction limit reached!
% 1.20/0.59 % (1827754)------------------------------
% 1.20/0.59 % (1827754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.20/0.59 % (1827754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.20/0.59 % (1827754)CaDiCaL version: 2.1.3
% 1.20/0.59 % (1827754)Termination reason: Instruction limit
% 1.20/0.59 % (1827754)Termination phase: Saturation
% 1.20/0.59 % (1827754)Time elapsed: 0.109 s
% 1.20/0.59 % (1827754)Peak memory usage: 13 MB
% 1.20/0.59 % (1827754)Instructions burned: 132 (million)
% 1.20/0.59 % (1827752)Instruction limit reached!
% 1.20/0.59 % (1827752)------------------------------
% 1.20/0.59 % (1827752)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.20/0.59 % (1827752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.20/0.59 % (1827752)CaDiCaL version: 2.1.3
% 1.20/0.59 % (1827752)Termination reason: Instruction limit
% 1.20/0.59 % (1827752)Termination phase: Saturation
% 1.20/0.59 % (1827752)Time elapsed: 0.113 s
% 1.20/0.59 % (1827752)Peak memory usage: 12 MB
% 1.20/0.59 % (1827752)Instructions burned: 104 (million)
% 1.20/0.59 % (1827753)Instruction limit reached!
% 1.20/0.59 % (1827753)------------------------------
% 1.20/0.59 % (1827753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.20/0.59 % (1827753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.20/0.59 % (1827753)CaDiCaL version: 2.1.3
% 1.20/0.59 % (1827753)Termination reason: Instruction limit
% 1.20/0.59 % (1827753)Termination phase: Saturation
% 1.20/0.59 % (1827753)Time elapsed: 0.113 s
% 1.20/0.59 % (1827753)Peak memory usage: 12 MB
% 1.20/0.59 % (1827753)Instructions burned: 117 (million)
% 1.20/0.59 % TRYING [6]
% 1.20/0.59 % (1827763)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3482277083:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 1.20/0.59 % (1827765)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2081538269:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.20/0.59 % (1827764)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=135794212:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.20/0.59 % (1827755)Instruction limit reached!
% 1.20/0.59 % (1827755)------------------------------
% 1.20/0.59 % (1827755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.20/0.59 % (1827755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.20/0.59 % (1827755)CaDiCaL version: 2.1.3
% 1.20/0.59 % (1827755)Termination reason: Instruction limit
% 1.20/0.59 % (1827755)Termination phase: Saturation
% 1.20/0.59 % (1827755)Time elapsed: 0.154 s
% 1.20/0.59 % (1827755)Peak memory usage: 13 MB
% 1.20/0.59 % (1827755)Instructions burned: 160 (million)
% 1.20/0.59 % TRYING [1]
% 1.20/0.59 % TRYING [2]
% 1.20/0.59 % TRYING [3]
% 1.20/0.59 % (1827750) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1827744-1827750"...
% 1.20/0.59 % TRYING [4]
% 1.20/0.59 % (1827750)...printing done.
% 1.20/0.59 % SZS status CounterSatisfiable for theBenchmark
% 1.20/0.59 % SZS output start Saturation.
% See solution above
% 1.20/0.60 % SZS output start Definitions and Model Updates.
% 1.20/0.60 % SZS output end Definitions and Model Updates.
% 1.20/0.60 % (1827750)------------------------------
% 1.20/0.60 % (1827750)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.20/0.60 % (1827750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.20/0.60 % (1827750)CaDiCaL version: 2.1.3
% 1.20/0.60 % (1827750)Termination reason: Satisfiable
% 1.20/0.60 % (1827750)Time elapsed: 0.166 s
% 1.20/0.60 % (1827750)Peak memory usage: 13 MB
% 1.20/0.60 % (1827750)Instructions burned: 155 (million)
% 1.20/0.60 % (1827744)Success in time 0.219 s
% 1.20/0.60 % Vampire exiting
%------------------------------------------------------------------------------