%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWV238+1 : TPTP v8.1.0. Released v3.2.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Wed Jul 20 21:41:44 EDT 2022
% Result : CounterSatisfiable 0.71s 0.91s
% Output : Saturation 0.71s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 351)
% Comments :
%------------------------------------------------------------------------------
cnf(1645,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(x)
| ~ p(i(i(zcmk)))
| ~ p(y)
| p(enc(enc(i(enc(i(zcmk),u)),v),enc(i(enc(i(y),w)),x))) ),
inference(sor,[status(thm)],[1578,15]),
[iquote('0:SoR:1578.2,15.2')] ).
cnf(1643,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(x)
| ~ p(i(i(enc(i(enc(i(zcmk),w)),x))))
| ~ p(y)
| p(enc(enc(i(enc(i(zcmk),u)),v),y)) ),
inference(sor,[status(thm)],[1582,15]),
[iquote('0:SoR:1582.4,15.2')] ).
cnf(1642,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(x)
| ~ p(i(i(zcmk)))
| ~ p(y)
| p(enc(enc(i(y),u),enc(i(enc(i(enc(i(zcmk),v)),w)),x))) ),
inference(sor,[status(thm)],[1584,15]),
[iquote('0:SoR:1584.0,15.2')] ).
cnf(1578,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(i(i(zcmk)),w))
| ~ p(x)
| ~ p(y)
| p(enc(enc(i(enc(i(zcmk),u)),v),enc(i(enc(i(w),x)),y))) ),
inference(spr,[status(thm),theory(equality)],[13,1196]),
[iquote('0:SpR:13.0,1196.5')] ).
cnf(1580,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(enc(i(i(enc(i(zcmk),w))),x))
| ~ p(y)
| p(enc(enc(i(enc(i(zcmk),u)),v),enc(i(x),y))) ),
inference(spr,[status(thm),theory(equality)],[13,1196]),
[iquote('0:SpR:13.0,1196.5')] ).
cnf(1582,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(x)
| ~ p(enc(i(i(enc(i(enc(i(zcmk),w)),x))),y))
| p(enc(enc(i(enc(i(zcmk),u)),v),y)) ),
inference(spr,[status(thm),theory(equality)],[13,1196]),
[iquote('0:SpR:13.0,1196.5')] ).
cnf(1584,plain,
( ~ p(enc(i(i(zcmk)),u))
| ~ p(v)
| ~ p(w)
| ~ p(x)
| ~ p(y)
| p(enc(enc(i(u),v),enc(i(enc(i(enc(i(zcmk),w)),x)),y))) ),
inference(spr,[status(thm),theory(equality)],[13,1196]),
[iquote('0:SpR:13.0,1196.5')] ).
cnf(1586,plain,
( ~ p(u)
| ~ p(enc(i(i(enc(i(zcmk),u))),v))
| ~ p(w)
| ~ p(x)
| ~ p(y)
| p(enc(v,enc(i(enc(i(enc(i(zcmk),w)),x)),y))) ),
inference(spr,[status(thm),theory(equality)],[13,1196]),
[iquote('0:SpR:13.0,1196.5')] ).
cnf(1579,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(zcmk,w))
| ~ p(x)
| ~ p(y)
| p(enc(enc(i(enc(i(zcmk),u)),v),enc(i(enc(i(w),x)),y))) ),
inference(spr,[status(thm),theory(equality)],[12,1196]),
[iquote('0:SpR:12.0,1196.5')] ).
cnf(1581,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(enc(enc(i(zcmk),w),x))
| ~ p(y)
| p(enc(enc(i(enc(i(zcmk),u)),v),enc(i(x),y))) ),
inference(spr,[status(thm),theory(equality)],[12,1196]),
[iquote('0:SpR:12.0,1196.5')] ).
cnf(1583,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(x)
| ~ p(enc(enc(i(enc(i(zcmk),w)),x),y))
| p(enc(enc(i(enc(i(zcmk),u)),v),y)) ),
inference(spr,[status(thm),theory(equality)],[12,1196]),
[iquote('0:SpR:12.0,1196.5')] ).
cnf(1585,plain,
( ~ p(enc(zcmk,u))
| ~ p(v)
| ~ p(w)
| ~ p(x)
| ~ p(y)
| p(enc(enc(i(u),v),enc(i(enc(i(enc(i(zcmk),w)),x)),y))) ),
inference(spr,[status(thm),theory(equality)],[12,1196]),
[iquote('0:SpR:12.0,1196.5')] ).
cnf(1587,plain,
( ~ p(u)
| ~ p(enc(enc(i(zcmk),u),v))
| ~ p(w)
| ~ p(x)
| ~ p(y)
| p(enc(v,enc(i(enc(i(enc(i(zcmk),w)),x)),y))) ),
inference(spr,[status(thm),theory(equality)],[12,1196]),
[iquote('0:SpR:12.0,1196.5')] ).
cnf(1196,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(x)
| ~ p(y)
| p(enc(enc(i(enc(i(zcmk),u)),v),enc(i(enc(i(enc(i(zcmk),w)),x)),y))) ),
inference(sor,[status(thm)],[1181,431]),
[iquote('0:SoR:1181.0,431.3')] ).
cnf(1562,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(i(i(zcmk)))
| ~ p(x)
| p(enc(enc(i(tmk),v),enc(i(enc(i(x),w)),u))) ),
inference(sor,[status(thm)],[1485,15]),
[iquote('0:SoR:1485.3,15.2')] ).
cnf(1559,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(i(i(enc(i(enc(i(zcmk),w)),v))))
| ~ p(x)
| p(enc(enc(i(tmk),u),x)) ),
inference(sor,[status(thm)],[1489,15]),
[iquote('0:SoR:1489.0,15.2')] ).
cnf(1557,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(i(i(zcmk)))
| ~ p(x)
| p(enc(enc(i(enc(i(zcmk),w)),v),enc(i(x),u))) ),
inference(sor,[status(thm)],[1460,15]),
[iquote('0:SoR:1460.1,15.2')] ).
cnf(1554,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(i(i(zcmk)))
| ~ p(x)
| p(enc(enc(i(x),w),enc(i(enc(i(zcmk),v)),u))) ),
inference(sor,[status(thm)],[1464,15]),
[iquote('0:SoR:1464.3,15.2')] ).
cnf(1552,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(i(i(wk)))
| ~ p(x)
| p(enc(enc(i(enc(i(zcmk),v)),w),enc(i(x),u))) ),
inference(sor,[status(thm)],[1344,15]),
[iquote('0:SoR:1344.0,15.2')] ).
cnf(1551,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(i(i(enc(i(wk),u))))
| ~ p(x)
| p(enc(enc(i(enc(i(zcmk),v)),w),x)) ),
inference(sor,[status(thm)],[1346,15]),
[iquote('0:SoR:1346.1,15.2')] ).
cnf(1550,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(i(i(zcmk)))
| ~ p(x)
| p(enc(enc(i(x),w),enc(i(enc(i(wk),u)),v))) ),
inference(sor,[status(thm)],[1348,15]),
[iquote('0:SoR:1348.2,15.2')] ).
cnf(1547,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(i(i(enc(i(tmk),u))))
| ~ p(x)
| p(enc(enc(i(enc(i(zcmk),v)),w),x)) ),
inference(sor,[status(thm)],[1324,15]),
[iquote('0:SoR:1324.1,15.2')] ).
cnf(1546,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(i(i(zcmk)))
| ~ p(x)
| p(enc(enc(i(x),w),enc(i(enc(i(tmk),u)),v))) ),
inference(sor,[status(thm)],[1326,15]),
[iquote('0:SoR:1326.2,15.2')] ).
cnf(1475,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(i(i(zcmk)))
| ~ p(x)
| p(enc(enc(i(wk),u),enc(i(enc(i(x),w)),v))) ),
inference(sor,[status(thm)],[930,15]),
[iquote('0:SoR:930.3,15.2')] ).
cnf(1485,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(enc(i(i(zcmk)),x))
| p(enc(enc(i(tmk),v),enc(i(enc(i(x),w)),u))) ),
inference(spr,[status(thm),theory(equality)],[13,1021]),
[iquote('0:SpR:13.0,1021.4')] ).
cnf(1367,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(i(i(enc(i(enc(i(zcmk),w)),v))))
| ~ p(x)
| p(enc(enc(i(wk),u),x)) ),
inference(sor,[status(thm)],[934,15]),
[iquote('0:SoR:934.1,15.2')] ).
cnf(1487,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(i(i(enc(i(zcmk),w))),x))
| ~ p(w)
| p(enc(enc(i(tmk),v),enc(i(x),u))) ),
inference(spr,[status(thm),theory(equality)],[13,1021]),
[iquote('0:SpR:13.0,1021.4')] ).
cnf(1489,plain,
( ~ p(enc(i(i(enc(i(enc(i(zcmk),u)),v))),w))
| ~ p(x)
| ~ p(v)
| ~ p(u)
| p(enc(enc(i(tmk),x),w)) ),
inference(spr,[status(thm),theory(equality)],[13,1021]),
[iquote('0:SpR:13.0,1021.4')] ).
cnf(1491,plain,
( ~ p(u)
| ~ p(enc(i(i(tmk)),v))
| ~ p(w)
| ~ p(x)
| p(enc(v,enc(i(enc(i(enc(i(zcmk),x)),w)),u))) ),
inference(spr,[status(thm),theory(equality)],[13,1021]),
[iquote('0:SpR:13.0,1021.4')] ).
cnf(1460,plain,
( ~ p(u)
| ~ p(enc(i(i(zcmk)),v))
| ~ p(w)
| ~ p(x)
| p(enc(enc(i(enc(i(zcmk),x)),w),enc(i(v),u))) ),
inference(spr,[status(thm),theory(equality)],[13,965]),
[iquote('0:SpR:13.0,965.4')] ).
cnf(1362,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(i(i(wk)))
| ~ p(x)
| p(enc(x,enc(i(enc(i(enc(i(zcmk),w)),v)),u))) ),
inference(sor,[status(thm)],[936,15]),
[iquote('0:SoR:936.0,15.2')] ).
cnf(1462,plain,
( ~ p(enc(i(i(enc(i(zcmk),u))),v))
| ~ p(u)
| ~ p(w)
| ~ p(x)
| p(enc(enc(i(enc(i(zcmk),x)),w),v)) ),
inference(spr,[status(thm),theory(equality)],[13,965]),
[iquote('0:SpR:13.0,965.4')] ).
cnf(1464,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(enc(i(i(zcmk)),x))
| p(enc(enc(i(x),w),enc(i(enc(i(zcmk),v)),u))) ),
inference(spr,[status(thm),theory(equality)],[13,965]),
[iquote('0:SpR:13.0,965.4')] ).
cnf(1466,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(i(i(enc(i(zcmk),w))),x))
| ~ p(w)
| p(enc(x,enc(i(enc(i(zcmk),v)),u))) ),
inference(spr,[status(thm),theory(equality)],[13,965]),
[iquote('0:SpR:13.0,965.4')] ).
cnf(1344,plain,
( ~ p(enc(i(i(wk)),u))
| ~ p(v)
| ~ p(w)
| ~ p(x)
| p(enc(enc(i(enc(i(zcmk),w)),x),enc(i(u),v))) ),
inference(spr,[status(thm),theory(equality)],[13,379]),
[iquote('0:SpR:13.0,379.4')] ).
cnf(1346,plain,
( ~ p(u)
| ~ p(enc(i(i(enc(i(wk),u))),v))
| ~ p(w)
| ~ p(x)
| p(enc(enc(i(enc(i(zcmk),w)),x),v)) ),
inference(spr,[status(thm),theory(equality)],[13,379]),
[iquote('0:SpR:13.0,379.4')] ).
cnf(1348,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(i(i(zcmk)),w))
| ~ p(x)
| p(enc(enc(i(w),x),enc(i(enc(i(wk),u)),v))) ),
inference(spr,[status(thm),theory(equality)],[13,379]),
[iquote('0:SpR:13.0,379.4')] ).
cnf(1350,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(enc(i(i(enc(i(zcmk),w))),x))
| p(enc(x,enc(i(enc(i(wk),u)),v))) ),
inference(spr,[status(thm),theory(equality)],[13,379]),
[iquote('0:SpR:13.0,379.4')] ).
cnf(1322,plain,
( ~ p(enc(i(i(tmk)),u))
| ~ p(v)
| ~ p(w)
| ~ p(x)
| p(enc(enc(i(enc(i(zcmk),w)),x),enc(i(u),v))) ),
inference(spr,[status(thm),theory(equality)],[13,326]),
[iquote('0:SpR:13.0,326.4')] ).
cnf(1324,plain,
( ~ p(u)
| ~ p(enc(i(i(enc(i(tmk),u))),v))
| ~ p(w)
| ~ p(x)
| p(enc(enc(i(enc(i(zcmk),w)),x),v)) ),
inference(spr,[status(thm),theory(equality)],[13,326]),
[iquote('0:SpR:13.0,326.4')] ).
cnf(1326,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(i(i(zcmk)),w))
| ~ p(x)
| p(enc(enc(i(w),x),enc(i(enc(i(tmk),u)),v))) ),
inference(spr,[status(thm),theory(equality)],[13,326]),
[iquote('0:SpR:13.0,326.4')] ).
cnf(1486,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(enc(zcmk,x))
| p(enc(enc(i(tmk),v),enc(i(enc(i(x),w)),u))) ),
inference(spr,[status(thm),theory(equality)],[12,1021]),
[iquote('0:SpR:12.0,1021.4')] ).
cnf(1488,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(enc(i(zcmk),w),x))
| ~ p(w)
| p(enc(enc(i(tmk),v),enc(i(x),u))) ),
inference(spr,[status(thm),theory(equality)],[12,1021]),
[iquote('0:SpR:12.0,1021.4')] ).
cnf(1490,plain,
( ~ p(enc(enc(i(enc(i(zcmk),u)),v),w))
| ~ p(x)
| ~ p(v)
| ~ p(u)
| p(enc(enc(i(tmk),x),w)) ),
inference(spr,[status(thm),theory(equality)],[12,1021]),
[iquote('0:SpR:12.0,1021.4')] ).
cnf(1492,plain,
( ~ p(u)
| ~ p(enc(tmk,v))
| ~ p(w)
| ~ p(x)
| p(enc(v,enc(i(enc(i(enc(i(zcmk),x)),w)),u))) ),
inference(spr,[status(thm),theory(equality)],[12,1021]),
[iquote('0:SpR:12.0,1021.4')] ).
cnf(1328,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(enc(i(i(enc(i(zcmk),w))),x))
| p(enc(x,enc(i(enc(i(tmk),u)),v))) ),
inference(spr,[status(thm),theory(equality)],[13,326]),
[iquote('0:SpR:13.0,326.4')] ).
cnf(1021,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(x)
| p(enc(enc(i(tmk),v),enc(i(enc(i(enc(i(zcmk),x)),w)),u))) ),
inference(sor,[status(thm)],[850,18]),
[iquote('0:SoR:850.0,18.2')] ).
cnf(1461,plain,
( ~ p(u)
| ~ p(enc(zcmk,v))
| ~ p(w)
| ~ p(x)
| p(enc(enc(i(enc(i(zcmk),x)),w),enc(i(v),u))) ),
inference(spr,[status(thm),theory(equality)],[12,965]),
[iquote('0:SpR:12.0,965.4')] ).
cnf(1463,plain,
( ~ p(enc(enc(i(zcmk),u),v))
| ~ p(u)
| ~ p(w)
| ~ p(x)
| p(enc(enc(i(enc(i(zcmk),x)),w),v)) ),
inference(spr,[status(thm),theory(equality)],[12,965]),
[iquote('0:SpR:12.0,965.4')] ).
cnf(1465,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(enc(zcmk,x))
| p(enc(enc(i(x),w),enc(i(enc(i(zcmk),v)),u))) ),
inference(spr,[status(thm),theory(equality)],[12,965]),
[iquote('0:SpR:12.0,965.4')] ).
cnf(930,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(enc(i(i(zcmk)),x))
| p(enc(enc(i(wk),u),enc(i(enc(i(x),w)),v))) ),
inference(spr,[status(thm),theory(equality)],[13,368]),
[iquote('0:SpR:13.0,368.4')] ).
cnf(1467,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(enc(i(zcmk),w),x))
| ~ p(w)
| p(enc(x,enc(i(enc(i(zcmk),v)),u))) ),
inference(spr,[status(thm),theory(equality)],[12,965]),
[iquote('0:SpR:12.0,965.4')] ).
cnf(965,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(x)
| p(enc(enc(i(enc(i(zcmk),x)),w),enc(i(enc(i(zcmk),v)),u))) ),
inference(sor,[status(thm)],[823,18]),
[iquote('0:SoR:823.0,18.2')] ).
cnf(1345,plain,
( ~ p(enc(wk,u))
| ~ p(v)
| ~ p(w)
| ~ p(x)
| p(enc(enc(i(enc(i(zcmk),w)),x),enc(i(u),v))) ),
inference(spr,[status(thm),theory(equality)],[12,379]),
[iquote('0:SpR:12.0,379.4')] ).
cnf(1347,plain,
( ~ p(u)
| ~ p(enc(enc(i(wk),u),v))
| ~ p(w)
| ~ p(x)
| p(enc(enc(i(enc(i(zcmk),w)),x),v)) ),
inference(spr,[status(thm),theory(equality)],[12,379]),
[iquote('0:SpR:12.0,379.4')] ).
cnf(932,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(i(i(enc(i(zcmk),w))),x))
| ~ p(w)
| p(enc(enc(i(wk),u),enc(i(x),v))) ),
inference(spr,[status(thm),theory(equality)],[13,368]),
[iquote('0:SpR:13.0,368.4')] ).
cnf(1349,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(zcmk,w))
| ~ p(x)
| p(enc(enc(i(w),x),enc(i(enc(i(wk),u)),v))) ),
inference(spr,[status(thm),theory(equality)],[12,379]),
[iquote('0:SpR:12.0,379.4')] ).
cnf(1351,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(enc(enc(i(zcmk),w),x))
| p(enc(x,enc(i(enc(i(wk),u)),v))) ),
inference(spr,[status(thm),theory(equality)],[12,379]),
[iquote('0:SpR:12.0,379.4')] ).
cnf(1323,plain,
( ~ p(enc(tmk,u))
| ~ p(v)
| ~ p(w)
| ~ p(x)
| p(enc(enc(i(enc(i(zcmk),w)),x),enc(i(u),v))) ),
inference(spr,[status(thm),theory(equality)],[12,326]),
[iquote('0:SpR:12.0,326.4')] ).
cnf(1325,plain,
( ~ p(u)
| ~ p(enc(enc(i(tmk),u),v))
| ~ p(w)
| ~ p(x)
| p(enc(enc(i(enc(i(zcmk),w)),x),v)) ),
inference(spr,[status(thm),theory(equality)],[12,326]),
[iquote('0:SpR:12.0,326.4')] ).
cnf(934,plain,
( ~ p(u)
| ~ p(enc(i(i(enc(i(enc(i(zcmk),v)),w))),x))
| ~ p(w)
| ~ p(v)
| p(enc(enc(i(wk),u),x)) ),
inference(spr,[status(thm),theory(equality)],[13,368]),
[iquote('0:SpR:13.0,368.4')] ).
cnf(1327,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(zcmk,w))
| ~ p(x)
| p(enc(enc(i(w),x),enc(i(enc(i(tmk),u)),v))) ),
inference(spr,[status(thm),theory(equality)],[12,326]),
[iquote('0:SpR:12.0,326.4')] ).
cnf(1329,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(enc(enc(i(zcmk),w),x))
| p(enc(x,enc(i(enc(i(tmk),u)),v))) ),
inference(spr,[status(thm),theory(equality)],[12,326]),
[iquote('0:SpR:12.0,326.4')] ).
cnf(1262,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(i(zcmk)))
| ~ p(w)
| p(enc(i(enc(i(zcmk),u)),enc(i(w),v))) ),
inference(sor,[status(thm)],[889,15]),
[iquote('0:SoR:889.2,15.2')] ).
cnf(1252,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(i(zcmk)))
| ~ p(w)
| p(enc(i(w),enc(i(enc(i(zcmk),v)),u))) ),
inference(sor,[status(thm)],[893,15]),
[iquote('0:SoR:893.0,15.2')] ).
cnf(936,plain,
( ~ p(enc(i(i(wk)),u))
| ~ p(v)
| ~ p(w)
| ~ p(x)
| p(enc(u,enc(i(enc(i(enc(i(zcmk),x)),w)),v))) ),
inference(spr,[status(thm),theory(equality)],[13,368]),
[iquote('0:SpR:13.0,368.4')] ).
cnf(1274,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(i(w__dfg)))
| ~ p(w)
| p(enc(enc(i(enc(i(zcmk),u)),v),w)) ),
inference(sor,[status(thm)],[1210,15]),
[iquote('0:SoR:1210.0,15.2')] ).
cnf(1273,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(i(zcmk)))
| ~ p(w)
| p(enc(enc(i(w),v),enc(i(w__dfg),u))) ),
inference(sor,[status(thm)],[1212,15]),
[iquote('0:SoR:1212.1,15.2')] ).
cnf(1266,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(i(pp)))
| ~ p(w)
| p(enc(enc(i(enc(i(zcmk),u)),v),w)) ),
inference(sor,[status(thm)],[1180,15]),
[iquote('0:SoR:1180.0,15.2')] ).
cnf(1265,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(i(zcmk)))
| ~ p(w)
| p(enc(enc(i(w),v),enc(i(pp),u))) ),
inference(sor,[status(thm)],[1182,15]),
[iquote('0:SoR:1182.1,15.2')] ).
cnf(379,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(x)
| p(enc(enc(i(enc(i(zcmk),w)),x),enc(i(enc(i(wk),u)),v))) ),
inference(sor,[status(thm)],[149,104]),
[iquote('0:SoR:149.0,104.2')] ).
cnf(1263,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(i(zcmk)))
| ~ p(w)
| p(enc(enc(i(wk),u),enc(i(w),v))) ),
inference(sor,[status(thm)],[1155,15]),
[iquote('0:SoR:1155.2,15.2')] ).
cnf(1260,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(i(wk)))
| ~ p(w)
| p(enc(w,enc(i(enc(i(zcmk),v)),u))) ),
inference(sor,[status(thm)],[1159,15]),
[iquote('0:SoR:1159.0,15.2')] ).
cnf(1259,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(i(zcmk)))
| ~ p(w)
| p(enc(w__dfg,enc(i(enc(i(w),v)),u))) ),
inference(sor,[status(thm)],[1119,15]),
[iquote('0:SoR:1119.2,15.2')] ).
cnf(1256,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(i(enc(i(enc(i(zcmk),v)),u))))
| ~ p(w)
| p(enc(w__dfg,w)) ),
inference(sor,[status(thm)],[1123,15]),
[iquote('0:SoR:1123.0,15.2')] ).
cnf(326,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(x)
| p(enc(enc(i(enc(i(zcmk),w)),x),enc(i(enc(i(tmk),u)),v))) ),
inference(sor,[status(thm)],[132,104]),
[iquote('0:SoR:132.0,104.2')] ).
cnf(1255,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(i(zcmk)))
| ~ p(w)
| p(enc(pp,enc(i(enc(i(w),v)),u))) ),
inference(sor,[status(thm)],[1084,15]),
[iquote('0:SoR:1084.2,15.2')] ).
cnf(1253,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(i(enc(i(enc(i(zcmk),v)),u))))
| ~ p(w)
| p(enc(pp,w)) ),
inference(sor,[status(thm)],[1088,15]),
[iquote('0:SoR:1088.0,15.2')] ).
cnf(1314,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(i(lp))
| p(enc(enc(i(enc(i(zcmk),u)),v),w)) ),
inference(sor,[status(thm)],[1251,11]),
[iquote('0:SoR:1251.2,11.1')] ).
cnf(1251,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(i(lp)))
| ~ p(w)
| p(enc(enc(i(enc(i(zcmk),u)),v),w)) ),
inference(sor,[status(thm)],[1069,15]),
[iquote('0:SoR:1069.0,15.2')] ).
cnf(931,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(enc(zcmk,x))
| p(enc(enc(i(wk),u),enc(i(enc(i(x),w)),v))) ),
inference(spr,[status(thm),theory(equality)],[12,368]),
[iquote('0:SpR:12.0,368.4')] ).
cnf(1250,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(i(zcmk)))
| ~ p(w)
| p(enc(enc(i(w),v),enc(i(lp),u))) ),
inference(sor,[status(thm)],[1071,15]),
[iquote('0:SoR:1071.1,15.2')] ).
cnf(1248,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(i(wk)))
| ~ p(w)
| p(enc(enc(i(tmk),v),enc(i(w),u))) ),
inference(sor,[status(thm)],[870,15]),
[iquote('0:SoR:870.0,15.2')] ).
cnf(1247,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(i(enc(i(wk),u))))
| ~ p(w)
| p(enc(enc(i(tmk),v),w)) ),
inference(sor,[status(thm)],[872,15]),
[iquote('0:SoR:872.1,15.2')] ).
cnf(1244,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(i(enc(i(tmk),u))))
| ~ p(w)
| p(enc(enc(i(tmk),v),w)) ),
inference(sor,[status(thm)],[851,15]),
[iquote('0:SoR:851.1,15.2')] ).
cnf(933,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(enc(i(zcmk),w),x))
| ~ p(w)
| p(enc(enc(i(wk),u),enc(i(x),v))) ),
inference(spr,[status(thm),theory(equality)],[12,368]),
[iquote('0:SpR:12.0,368.4')] ).
cnf(1241,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(i(zcmk)))
| ~ p(w)
| p(enc(enc(i(w),v),enc(i(tmk),u))) ),
inference(sor,[status(thm)],[837,15]),
[iquote('0:SoR:837.2,15.2')] ).
cnf(1239,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(i(zcmk)))
| ~ p(w)
| p(enc(enc(i(tmk),u),enc(i(w),v))) ),
inference(sor,[status(thm)],[818,15]),
[iquote('0:SoR:818.2,15.2')] ).
cnf(1304,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(i(tc))
| p(enc(enc(i(enc(i(zcmk),v)),u),w)) ),
inference(sor,[status(thm)],[1222,11]),
[iquote('0:SoR:1222.2,11.1')] ).
cnf(1222,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(i(tc)))
| ~ p(w)
| p(enc(enc(i(enc(i(zcmk),v)),u),w)) ),
inference(sor,[status(thm)],[777,15]),
[iquote('0:SoR:777.0,15.2')] ).
cnf(935,plain,
( ~ p(u)
| ~ p(enc(enc(i(enc(i(zcmk),v)),w),x))
| ~ p(w)
| ~ p(v)
| p(enc(enc(i(wk),u),x)) ),
inference(spr,[status(thm),theory(equality)],[12,368]),
[iquote('0:SpR:12.0,368.4')] ).
cnf(1192,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(i(zcmk)))
| ~ p(w)
| p(enc(enc(i(w),v),enc(i(tc),u))) ),
inference(sor,[status(thm)],[779,15]),
[iquote('0:SoR:779.2,15.2')] ).
cnf(1210,plain,
( ~ p(enc(i(i(w__dfg)),u))
| ~ p(v)
| ~ p(w)
| p(enc(enc(i(enc(i(zcmk),v)),w),u)) ),
inference(spr,[status(thm),theory(equality)],[13,721]),
[iquote('0:SpR:13.0,721.3')] ).
cnf(1212,plain,
( ~ p(u)
| ~ p(enc(i(i(zcmk)),v))
| ~ p(w)
| p(enc(enc(i(v),w),enc(i(w__dfg),u))) ),
inference(spr,[status(thm),theory(equality)],[13,721]),
[iquote('0:SpR:13.0,721.3')] ).
cnf(1214,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(i(i(enc(i(zcmk),v))),w))
| p(enc(w,enc(i(w__dfg),u))) ),
inference(spr,[status(thm),theory(equality)],[13,721]),
[iquote('0:SpR:13.0,721.3')] ).
cnf(937,plain,
( ~ p(enc(wk,u))
| ~ p(v)
| ~ p(w)
| ~ p(x)
| p(enc(u,enc(i(enc(i(enc(i(zcmk),x)),w)),v))) ),
inference(spr,[status(thm),theory(equality)],[12,368]),
[iquote('0:SpR:12.0,368.4')] ).
cnf(1180,plain,
( ~ p(enc(i(i(pp)),u))
| ~ p(v)
| ~ p(w)
| p(enc(enc(i(enc(i(zcmk),v)),w),u)) ),
inference(spr,[status(thm),theory(equality)],[13,557]),
[iquote('0:SpR:13.0,557.3')] ).
cnf(1182,plain,
( ~ p(u)
| ~ p(enc(i(i(zcmk)),v))
| ~ p(w)
| p(enc(enc(i(v),w),enc(i(pp),u))) ),
inference(spr,[status(thm),theory(equality)],[13,557]),
[iquote('0:SpR:13.0,557.3')] ).
cnf(1184,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(i(i(enc(i(zcmk),v))),w))
| p(enc(w,enc(i(pp),u))) ),
inference(spr,[status(thm),theory(equality)],[13,557]),
[iquote('0:SpR:13.0,557.3')] ).
cnf(1155,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(i(i(zcmk)),w))
| p(enc(enc(i(wk),u),enc(i(w),v))) ),
inference(spr,[status(thm),theory(equality)],[13,532]),
[iquote('0:SpR:13.0,532.3')] ).
cnf(889,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(i(i(zcmk)),w))
| p(enc(i(enc(i(zcmk),u)),enc(i(w),v))) ),
inference(spr,[status(thm),theory(equality)],[13,233]),
[iquote('0:SpR:13.0,233.3')] ).
cnf(1157,plain,
( ~ p(u)
| ~ p(enc(i(i(enc(i(zcmk),v))),w))
| ~ p(v)
| p(enc(enc(i(wk),u),w)) ),
inference(spr,[status(thm),theory(equality)],[13,532]),
[iquote('0:SpR:13.0,532.3')] ).
cnf(1159,plain,
( ~ p(enc(i(i(wk)),u))
| ~ p(v)
| ~ p(w)
| p(enc(u,enc(i(enc(i(zcmk),w)),v))) ),
inference(spr,[status(thm),theory(equality)],[13,532]),
[iquote('0:SpR:13.0,532.3')] ).
cnf(1119,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(i(i(zcmk)),w))
| p(enc(w__dfg,enc(i(enc(i(w),v)),u))) ),
inference(spr,[status(thm),theory(equality)],[13,456]),
[iquote('0:SpR:13.0,456.3')] ).
cnf(1121,plain,
( ~ p(u)
| ~ p(enc(i(i(enc(i(zcmk),v))),w))
| ~ p(v)
| p(enc(w__dfg,enc(i(w),u))) ),
inference(spr,[status(thm),theory(equality)],[13,456]),
[iquote('0:SpR:13.0,456.3')] ).
cnf(891,plain,
( ~ p(u)
| ~ p(enc(i(i(enc(i(zcmk),v))),w))
| ~ p(v)
| p(enc(i(enc(i(zcmk),u)),w)) ),
inference(spr,[status(thm),theory(equality)],[13,233]),
[iquote('0:SpR:13.0,233.3')] ).
cnf(1123,plain,
( ~ p(enc(i(i(enc(i(enc(i(zcmk),u)),v))),w))
| ~ p(v)
| ~ p(u)
| p(enc(w__dfg,w)) ),
inference(spr,[status(thm),theory(equality)],[13,456]),
[iquote('0:SpR:13.0,456.3')] ).
cnf(1084,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(i(i(zcmk)),w))
| p(enc(pp,enc(i(enc(i(w),v)),u))) ),
inference(spr,[status(thm),theory(equality)],[13,431]),
[iquote('0:SpR:13.0,431.3')] ).
cnf(1086,plain,
( ~ p(u)
| ~ p(enc(i(i(enc(i(zcmk),v))),w))
| ~ p(v)
| p(enc(pp,enc(i(w),u))) ),
inference(spr,[status(thm),theory(equality)],[13,431]),
[iquote('0:SpR:13.0,431.3')] ).
cnf(1088,plain,
( ~ p(enc(i(i(enc(i(enc(i(zcmk),u)),v))),w))
| ~ p(v)
| ~ p(u)
| p(enc(pp,w)) ),
inference(spr,[status(thm),theory(equality)],[13,431]),
[iquote('0:SpR:13.0,431.3')] ).
cnf(893,plain,
( ~ p(enc(i(i(zcmk)),u))
| ~ p(v)
| ~ p(w)
| p(enc(i(u),enc(i(enc(i(zcmk),w)),v))) ),
inference(spr,[status(thm),theory(equality)],[13,233]),
[iquote('0:SpR:13.0,233.3')] ).
cnf(1069,plain,
( ~ p(enc(i(i(lp)),u))
| ~ p(v)
| ~ p(w)
| p(enc(enc(i(enc(i(zcmk),v)),w),u)) ),
inference(spr,[status(thm),theory(equality)],[13,272]),
[iquote('0:SpR:13.0,272.3')] ).
cnf(1071,plain,
( ~ p(u)
| ~ p(enc(i(i(zcmk)),v))
| ~ p(w)
| p(enc(enc(i(v),w),enc(i(lp),u))) ),
inference(spr,[status(thm),theory(equality)],[13,272]),
[iquote('0:SpR:13.0,272.3')] ).
cnf(1073,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(i(i(enc(i(zcmk),v))),w))
| p(enc(w,enc(i(lp),u))) ),
inference(spr,[status(thm),theory(equality)],[13,272]),
[iquote('0:SpR:13.0,272.3')] ).
cnf(870,plain,
( ~ p(enc(i(i(wk)),u))
| ~ p(v)
| ~ p(w)
| p(enc(enc(i(tmk),w),enc(i(u),v))) ),
inference(spr,[status(thm),theory(equality)],[13,382]),
[iquote('0:SpR:13.0,382.3')] ).
cnf(872,plain,
( ~ p(u)
| ~ p(enc(i(i(enc(i(wk),u))),v))
| ~ p(w)
| p(enc(enc(i(tmk),w),v)) ),
inference(spr,[status(thm),theory(equality)],[13,382]),
[iquote('0:SpR:13.0,382.3')] ).
cnf(874,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(i(i(tmk)),w))
| p(enc(w,enc(i(enc(i(wk),u)),v))) ),
inference(spr,[status(thm),theory(equality)],[13,382]),
[iquote('0:SpR:13.0,382.3')] ).
cnf(849,plain,
( ~ p(enc(i(i(tmk)),u))
| ~ p(v)
| ~ p(w)
| p(enc(enc(i(tmk),w),enc(i(u),v))) ),
inference(spr,[status(thm),theory(equality)],[13,329]),
[iquote('0:SpR:13.0,329.3')] ).
cnf(851,plain,
( ~ p(u)
| ~ p(enc(i(i(enc(i(tmk),u))),v))
| ~ p(w)
| p(enc(enc(i(tmk),w),v)) ),
inference(spr,[status(thm),theory(equality)],[13,329]),
[iquote('0:SpR:13.0,329.3')] ).
cnf(853,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(i(i(tmk)),w))
| p(enc(w,enc(i(enc(i(tmk),u)),v))) ),
inference(spr,[status(thm),theory(equality)],[13,329]),
[iquote('0:SpR:13.0,329.3')] ).
cnf(835,plain,
( ~ p(enc(i(i(tmk)),u))
| ~ p(v)
| ~ p(w)
| p(enc(enc(i(enc(i(zcmk),w)),v),u)) ),
inference(spr,[status(thm),theory(equality)],[13,203]),
[iquote('0:SpR:13.0,203.3')] ).
cnf(837,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(i(i(zcmk)),w))
| p(enc(enc(i(w),v),enc(i(tmk),u))) ),
inference(spr,[status(thm),theory(equality)],[13,203]),
[iquote('0:SpR:13.0,203.3')] ).
cnf(839,plain,
( ~ p(u)
| ~ p(enc(i(i(enc(i(zcmk),v))),w))
| ~ p(v)
| p(enc(w,enc(i(tmk),u))) ),
inference(spr,[status(thm),theory(equality)],[13,203]),
[iquote('0:SpR:13.0,203.3')] ).
cnf(818,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(i(i(zcmk)),w))
| p(enc(enc(i(tmk),u),enc(i(w),v))) ),
inference(spr,[status(thm),theory(equality)],[13,188]),
[iquote('0:SpR:13.0,188.3')] ).
cnf(820,plain,
( ~ p(u)
| ~ p(enc(i(i(enc(i(zcmk),v))),w))
| ~ p(v)
| p(enc(enc(i(tmk),u),w)) ),
inference(spr,[status(thm),theory(equality)],[13,188]),
[iquote('0:SpR:13.0,188.3')] ).
cnf(822,plain,
( ~ p(enc(i(i(tmk)),u))
| ~ p(v)
| ~ p(w)
| p(enc(u,enc(i(enc(i(zcmk),w)),v))) ),
inference(spr,[status(thm),theory(equality)],[13,188]),
[iquote('0:SpR:13.0,188.3')] ).
cnf(1078,plain,
( ~ p(u)
| ~ p(v)
| ~ p(lp)
| ~ p(w)
| p(enc(enc(i(enc(i(zcmk),u)),v),w)) ),
inference(sor,[status(thm)],[1070,15]),
[iquote('0:SoR:1070.0,15.2')] ).
cnf(958,plain,
( ~ p(u)
| ~ p(v)
| ~ p(tc)
| ~ p(w)
| p(enc(enc(i(enc(i(zcmk),v)),u),w)) ),
inference(sor,[status(thm)],[778,15]),
[iquote('0:SoR:778.0,15.2')] ).
cnf(1211,plain,
( ~ p(enc(w__dfg,u))
| ~ p(v)
| ~ p(w)
| p(enc(enc(i(enc(i(zcmk),v)),w),u)) ),
inference(spr,[status(thm),theory(equality)],[12,721]),
[iquote('0:SpR:12.0,721.3')] ).
cnf(1213,plain,
( ~ p(u)
| ~ p(enc(zcmk,v))
| ~ p(w)
| p(enc(enc(i(v),w),enc(i(w__dfg),u))) ),
inference(spr,[status(thm),theory(equality)],[12,721]),
[iquote('0:SpR:12.0,721.3')] ).
cnf(777,plain,
( ~ p(enc(i(i(tc)),u))
| ~ p(v)
| ~ p(w)
| p(enc(enc(i(enc(i(zcmk),w)),v),u)) ),
inference(spr,[status(thm),theory(equality)],[13,180]),
[iquote('0:SpR:13.0,180.3')] ).
cnf(1215,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(enc(i(zcmk),v),w))
| p(enc(w,enc(i(w__dfg),u))) ),
inference(spr,[status(thm),theory(equality)],[12,721]),
[iquote('0:SpR:12.0,721.3')] ).
cnf(721,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| p(enc(enc(i(enc(i(zcmk),v)),w),enc(i(w__dfg),u))) ),
inference(sor,[status(thm)],[607,104]),
[iquote('0:SoR:607.0,104.2')] ).
cnf(1181,plain,
( ~ p(enc(pp,u))
| ~ p(v)
| ~ p(w)
| p(enc(enc(i(enc(i(zcmk),v)),w),u)) ),
inference(spr,[status(thm),theory(equality)],[12,557]),
[iquote('0:SpR:12.0,557.3')] ).
cnf(1183,plain,
( ~ p(u)
| ~ p(enc(zcmk,v))
| ~ p(w)
| p(enc(enc(i(v),w),enc(i(pp),u))) ),
inference(spr,[status(thm),theory(equality)],[12,557]),
[iquote('0:SpR:12.0,557.3')] ).
cnf(779,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(i(i(zcmk)),w))
| p(enc(enc(i(w),v),enc(i(tc),u))) ),
inference(spr,[status(thm),theory(equality)],[13,180]),
[iquote('0:SpR:13.0,180.3')] ).
cnf(1185,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(enc(i(zcmk),v),w))
| p(enc(w,enc(i(pp),u))) ),
inference(spr,[status(thm),theory(equality)],[12,557]),
[iquote('0:SpR:12.0,557.3')] ).
cnf(557,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| p(enc(enc(i(enc(i(zcmk),v)),w),enc(i(pp),u))) ),
inference(sor,[status(thm)],[545,104]),
[iquote('0:SoR:545.0,104.2')] ).
cnf(1156,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(zcmk,w))
| p(enc(enc(i(wk),u),enc(i(w),v))) ),
inference(spr,[status(thm),theory(equality)],[12,532]),
[iquote('0:SpR:12.0,532.3')] ).
cnf(1158,plain,
( ~ p(u)
| ~ p(enc(enc(i(zcmk),v),w))
| ~ p(v)
| p(enc(enc(i(wk),u),w)) ),
inference(spr,[status(thm),theory(equality)],[12,532]),
[iquote('0:SpR:12.0,532.3')] ).
cnf(781,plain,
( ~ p(u)
| ~ p(enc(i(i(enc(i(zcmk),v))),w))
| ~ p(v)
| p(enc(w,enc(i(tc),u))) ),
inference(spr,[status(thm),theory(equality)],[13,180]),
[iquote('0:SpR:13.0,180.3')] ).
cnf(1160,plain,
( ~ p(enc(wk,u))
| ~ p(v)
| ~ p(w)
| p(enc(u,enc(i(enc(i(zcmk),w)),v))) ),
inference(spr,[status(thm),theory(equality)],[12,532]),
[iquote('0:SpR:12.0,532.3')] ).
cnf(532,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| p(enc(enc(i(wk),u),enc(i(enc(i(zcmk),w)),v))) ),
inference(sor,[status(thm)],[526,18]),
[iquote('0:SoR:526.1,18.2')] ).
cnf(1120,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(zcmk,w))
| p(enc(w__dfg,enc(i(enc(i(w),v)),u))) ),
inference(spr,[status(thm),theory(equality)],[12,456]),
[iquote('0:SpR:12.0,456.3')] ).
cnf(1122,plain,
( ~ p(u)
| ~ p(enc(enc(i(zcmk),v),w))
| ~ p(v)
| p(enc(w__dfg,enc(i(w),u))) ),
inference(spr,[status(thm),theory(equality)],[12,456]),
[iquote('0:SpR:12.0,456.3')] ).
cnf(890,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(zcmk,w))
| p(enc(i(enc(i(zcmk),u)),enc(i(w),v))) ),
inference(spr,[status(thm),theory(equality)],[12,233]),
[iquote('0:SpR:12.0,233.3')] ).
cnf(1124,plain,
( ~ p(enc(enc(i(enc(i(zcmk),u)),v),w))
| ~ p(v)
| ~ p(u)
| p(enc(w__dfg,w)) ),
inference(spr,[status(thm),theory(equality)],[12,456]),
[iquote('0:SpR:12.0,456.3')] ).
cnf(456,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| p(enc(w__dfg,enc(i(enc(i(enc(i(zcmk),w)),v)),u))) ),
inference(sor,[status(thm)],[452,18]),
[iquote('0:SoR:452.0,18.2')] ).
cnf(1085,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(zcmk,w))
| p(enc(pp,enc(i(enc(i(w),v)),u))) ),
inference(spr,[status(thm),theory(equality)],[12,431]),
[iquote('0:SpR:12.0,431.3')] ).
cnf(1087,plain,
( ~ p(u)
| ~ p(enc(enc(i(zcmk),v),w))
| ~ p(v)
| p(enc(pp,enc(i(w),u))) ),
inference(spr,[status(thm),theory(equality)],[12,431]),
[iquote('0:SpR:12.0,431.3')] ).
cnf(892,plain,
( ~ p(u)
| ~ p(enc(enc(i(zcmk),v),w))
| ~ p(v)
| p(enc(i(enc(i(zcmk),u)),w)) ),
inference(spr,[status(thm),theory(equality)],[12,233]),
[iquote('0:SpR:12.0,233.3')] ).
cnf(1089,plain,
( ~ p(enc(enc(i(enc(i(zcmk),u)),v),w))
| ~ p(v)
| ~ p(u)
| p(enc(pp,w)) ),
inference(spr,[status(thm),theory(equality)],[12,431]),
[iquote('0:SpR:12.0,431.3')] ).
cnf(431,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| p(enc(pp,enc(i(enc(i(enc(i(zcmk),w)),v)),u))) ),
inference(sor,[status(thm)],[422,18]),
[iquote('0:SoR:422.0,18.2')] ).
cnf(1070,plain,
( ~ p(enc(lp,u))
| ~ p(v)
| ~ p(w)
| p(enc(enc(i(enc(i(zcmk),v)),w),u)) ),
inference(spr,[status(thm),theory(equality)],[12,272]),
[iquote('0:SpR:12.0,272.3')] ).
cnf(1072,plain,
( ~ p(u)
| ~ p(enc(zcmk,v))
| ~ p(w)
| p(enc(enc(i(v),w),enc(i(lp),u))) ),
inference(spr,[status(thm),theory(equality)],[12,272]),
[iquote('0:SpR:12.0,272.3')] ).
cnf(894,plain,
( ~ p(enc(zcmk,u))
| ~ p(v)
| ~ p(w)
| p(enc(i(u),enc(i(enc(i(zcmk),w)),v))) ),
inference(spr,[status(thm),theory(equality)],[12,233]),
[iquote('0:SpR:12.0,233.3')] ).
cnf(1074,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(enc(i(zcmk),v),w))
| p(enc(w,enc(i(lp),u))) ),
inference(spr,[status(thm),theory(equality)],[12,272]),
[iquote('0:SpR:12.0,272.3')] ).
cnf(272,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| p(enc(enc(i(enc(i(zcmk),v)),w),enc(i(lp),u))) ),
inference(sor,[status(thm)],[77,104]),
[iquote('0:SoR:77.0,104.2')] ).
cnf(871,plain,
( ~ p(enc(wk,u))
| ~ p(v)
| ~ p(w)
| p(enc(enc(i(tmk),w),enc(i(u),v))) ),
inference(spr,[status(thm),theory(equality)],[12,382]),
[iquote('0:SpR:12.0,382.3')] ).
cnf(873,plain,
( ~ p(u)
| ~ p(enc(enc(i(wk),u),v))
| ~ p(w)
| p(enc(enc(i(tmk),w),v)) ),
inference(spr,[status(thm),theory(equality)],[12,382]),
[iquote('0:SpR:12.0,382.3')] ).
cnf(875,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(tmk,w))
| p(enc(w,enc(i(enc(i(wk),u)),v))) ),
inference(spr,[status(thm),theory(equality)],[12,382]),
[iquote('0:SpR:12.0,382.3')] ).
cnf(850,plain,
( ~ p(enc(tmk,u))
| ~ p(v)
| ~ p(w)
| p(enc(enc(i(tmk),w),enc(i(u),v))) ),
inference(spr,[status(thm),theory(equality)],[12,329]),
[iquote('0:SpR:12.0,329.3')] ).
cnf(852,plain,
( ~ p(u)
| ~ p(enc(enc(i(tmk),u),v))
| ~ p(w)
| p(enc(enc(i(tmk),w),v)) ),
inference(spr,[status(thm),theory(equality)],[12,329]),
[iquote('0:SpR:12.0,329.3')] ).
cnf(854,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(tmk,w))
| p(enc(w,enc(i(enc(i(tmk),u)),v))) ),
inference(spr,[status(thm),theory(equality)],[12,329]),
[iquote('0:SpR:12.0,329.3')] ).
cnf(836,plain,
( ~ p(enc(tmk,u))
| ~ p(v)
| ~ p(w)
| p(enc(enc(i(enc(i(zcmk),w)),v),u)) ),
inference(spr,[status(thm),theory(equality)],[12,203]),
[iquote('0:SpR:12.0,203.3')] ).
cnf(838,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(zcmk,w))
| p(enc(enc(i(w),v),enc(i(tmk),u))) ),
inference(spr,[status(thm),theory(equality)],[12,203]),
[iquote('0:SpR:12.0,203.3')] ).
cnf(840,plain,
( ~ p(u)
| ~ p(enc(enc(i(zcmk),v),w))
| ~ p(v)
| p(enc(w,enc(i(tmk),u))) ),
inference(spr,[status(thm),theory(equality)],[12,203]),
[iquote('0:SpR:12.0,203.3')] ).
cnf(819,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(zcmk,w))
| p(enc(enc(i(tmk),u),enc(i(w),v))) ),
inference(spr,[status(thm),theory(equality)],[12,188]),
[iquote('0:SpR:12.0,188.3')] ).
cnf(920,plain,
( ~ p(u)
| ~ p(i(i(w__dfg)))
| ~ p(v)
| p(enc(enc(i(tmk),u),v)) ),
inference(sor,[status(thm)],[787,15]),
[iquote('0:SoR:787.0,15.2')] ).
cnf(918,plain,
( ~ p(u)
| ~ p(i(i(zcmk)))
| ~ p(v)
| p(enc(enc(i(v),u),t1)) ),
inference(sor,[status(thm)],[770,15]),
[iquote('0:SoR:770.0,15.2')] ).
cnf(821,plain,
( ~ p(u)
| ~ p(enc(enc(i(zcmk),v),w))
| ~ p(v)
| p(enc(enc(i(tmk),u),w)) ),
inference(spr,[status(thm),theory(equality)],[12,188]),
[iquote('0:SpR:12.0,188.3')] ).
cnf(915,plain,
( ~ p(u)
| ~ p(i(i(pp)))
| ~ p(v)
| p(enc(enc(i(tmk),u),v)) ),
inference(sor,[status(thm)],[741,15]),
[iquote('0:SoR:741.0,15.2')] ).
cnf(913,plain,
( ~ p(u)
| ~ p(i(i(zcmk)))
| ~ p(v)
| p(enc(w__dfg,enc(i(v),u))) ),
inference(sor,[status(thm)],[730,15]),
[iquote('0:SoR:730.0,15.2')] ).
cnf(909,plain,
( ~ p(u)
| ~ p(i(i(wk)))
| ~ p(v)
| p(enc(v,enc(i(w__dfg),u))) ),
inference(sor,[status(thm)],[606,15]),
[iquote('0:SoR:606.0,15.2')] ).
cnf(908,plain,
( ~ p(u)
| ~ p(i(i(w__dfg)))
| ~ p(v)
| p(enc(enc(i(wk),u),v)) ),
inference(sor,[status(thm)],[604,15]),
[iquote('0:SoR:604.1,15.2')] ).
cnf(823,plain,
( ~ p(enc(tmk,u))
| ~ p(v)
| ~ p(w)
| p(enc(u,enc(i(enc(i(zcmk),w)),v))) ),
inference(spr,[status(thm),theory(equality)],[12,188]),
[iquote('0:SpR:12.0,188.3')] ).
cnf(907,plain,
( ~ p(u)
| ~ p(i(i(enc(i(wk),u))))
| ~ p(v)
| p(enc(w__dfg,v)) ),
inference(sor,[status(thm)],[573,15]),
[iquote('0:SoR:573.1,15.2')] ).
cnf(905,plain,
( ~ p(u)
| ~ p(i(i(wk)))
| ~ p(v)
| p(enc(w__dfg,enc(i(v),u))) ),
inference(sor,[status(thm)],[571,15]),
[iquote('0:SoR:571.0,15.2')] ).
cnf(904,plain,
( ~ p(u)
| ~ p(i(i(enc(i(wk),u))))
| ~ p(v)
| p(enc(pp,v)) ),
inference(sor,[status(thm)],[568,15]),
[iquote('0:SoR:568.1,15.2')] ).
cnf(903,plain,
( ~ p(u)
| ~ p(i(i(wk)))
| ~ p(v)
| p(enc(pp,enc(i(v),u))) ),
inference(sor,[status(thm)],[566,15]),
[iquote('0:SoR:566.0,15.2')] ).
cnf(778,plain,
( ~ p(enc(tc,u))
| ~ p(v)
| ~ p(w)
| p(enc(enc(i(enc(i(zcmk),w)),v),u)) ),
inference(spr,[status(thm),theory(equality)],[12,180]),
[iquote('0:SpR:12.0,180.3')] ).
cnf(902,plain,
( ~ p(u)
| ~ p(i(i(wk)))
| ~ p(v)
| p(enc(v,enc(i(pp),u))) ),
inference(sor,[status(thm)],[544,15]),
[iquote('0:SoR:544.0,15.2')] ).
cnf(900,plain,
( ~ p(u)
| ~ p(i(i(pp)))
| ~ p(v)
| p(enc(enc(i(wk),u),v)) ),
inference(sor,[status(thm)],[542,15]),
[iquote('0:SoR:542.1,15.2')] ).
cnf(899,plain,
( ~ p(u)
| ~ p(i(i(wk)))
| ~ p(v)
| p(enc(v,enc(i(tmk),u))) ),
inference(sor,[status(thm)],[527,15]),
[iquote('0:SoR:527.0,15.2')] ).
cnf(897,plain,
( ~ p(u)
| ~ p(i(i(wk)))
| ~ p(v)
| p(enc(v,enc(i(tc),u))) ),
inference(sor,[status(thm)],[511,15]),
[iquote('0:SoR:511.0,15.2')] ).
cnf(780,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(zcmk,w))
| p(enc(enc(i(w),v),enc(i(tc),u))) ),
inference(spr,[status(thm),theory(equality)],[12,180]),
[iquote('0:SpR:12.0,180.3')] ).
cnf(951,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(tc))
| p(enc(enc(i(wk),u),v)) ),
inference(sor,[status(thm)],[885,11]),
[iquote('0:SoR:885.1,11.1')] ).
cnf(885,plain,
( ~ p(u)
| ~ p(i(i(tc)))
| ~ p(v)
| p(enc(enc(i(wk),u),v)) ),
inference(sor,[status(thm)],[509,15]),
[iquote('0:SoR:509.1,15.2')] ).
cnf(884,plain,
( ~ p(u)
| ~ p(i(i(enc(i(tmk),u))))
| ~ p(v)
| p(enc(w__dfg,v)) ),
inference(sor,[status(thm)],[453,15]),
[iquote('0:SoR:453.1,15.2')] ).
cnf(882,plain,
( ~ p(u)
| ~ p(i(i(enc(i(tmk),u))))
| ~ p(v)
| p(enc(pp,v)) ),
inference(sor,[status(thm)],[423,15]),
[iquote('0:SoR:423.1,15.2')] ).
cnf(782,plain,
( ~ p(u)
| ~ p(enc(enc(i(zcmk),v),w))
| ~ p(v)
| p(enc(w,enc(i(tc),u))) ),
inference(spr,[status(thm),theory(equality)],[12,180]),
[iquote('0:SpR:12.0,180.3')] ).
cnf(863,plain,
( ~ p(u)
| ~ p(i(i(zcmk)))
| ~ p(v)
| p(enc(pp,enc(i(v),u))) ),
inference(sor,[status(thm)],[321,15]),
[iquote('0:SoR:321.1,15.2')] ).
cnf(844,plain,
( ~ p(u)
| ~ p(i(i(zcmk)))
| ~ p(v)
| p(enc(enc(i(v),u),pp)) ),
inference(sor,[status(thm)],[312,15]),
[iquote('0:SoR:312.1,15.2')] ).
cnf(842,plain,
( ~ p(u)
| ~ p(i(i(zcmk)))
| ~ p(v)
| p(enc(enc(i(v),u),k)) ),
inference(sor,[status(thm)],[305,15]),
[iquote('0:SoR:305.1,15.2')] ).
cnf(833,plain,
( ~ p(u)
| ~ p(i(i(zcmk)))
| ~ p(v)
| p(enc(enc(i(v),u),t2)) ),
inference(sor,[status(thm)],[297,15]),
[iquote('0:SoR:297.1,15.2')] ).
cnf(368,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| ~ p(x)
| p(enc(enc(i(wk),u),enc(i(enc(i(enc(i(zcmk),x)),w)),v))) ),
inference(sor,[status(thm)],[128,18]),
[iquote('0:SoR:128.1,18.2')] ).
cnf(924,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(lp))
| p(enc(enc(i(tmk),u),v)) ),
inference(sor,[status(thm)],[831,11]),
[iquote('0:SoR:831.1,11.1')] ).
cnf(831,plain,
( ~ p(u)
| ~ p(i(i(lp)))
| ~ p(v)
| p(enc(enc(i(tmk),u),v)) ),
inference(sor,[status(thm)],[286,15]),
[iquote('0:SoR:286.0,15.2')] ).
cnf(813,plain,
( ~ p(u)
| ~ p(i(i(zcmk)))
| ~ p(v)
| p(enc(wk,enc(i(v),u))) ),
inference(sor,[status(thm)],[275,15]),
[iquote('0:SoR:275.1,15.2')] ).
cnf(789,plain,
( ~ p(u)
| ~ p(enc(i(i(tmk)),v))
| p(enc(v,enc(i(w__dfg),u))) ),
inference(spr,[status(thm),theory(equality)],[13,724]),
[iquote('0:SpR:13.0,724.2')] ).
cnf(539,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(i(wk)))
| ~ p(w)
| p(enc(enc(i(wk),u),enc(i(w),v))) ),
inference(sor,[status(thm)],[144,15]),
[iquote('0:SoR:144.1,15.2')] ).
cnf(787,plain,
( ~ p(enc(i(i(w__dfg)),u))
| ~ p(v)
| p(enc(enc(i(tmk),v),u)) ),
inference(spr,[status(thm),theory(equality)],[13,724]),
[iquote('0:SpR:13.0,724.2')] ).
cnf(772,plain,
( ~ p(u)
| ~ p(enc(i(i(enc(i(zcmk),u))),v))
| p(enc(v,t1)) ),
inference(spr,[status(thm),theory(equality)],[13,616]),
[iquote('0:SpR:13.0,616.2')] ).
cnf(770,plain,
( ~ p(enc(i(i(zcmk)),u))
| ~ p(v)
| p(enc(enc(i(u),v),t1)) ),
inference(spr,[status(thm),theory(equality)],[13,616]),
[iquote('0:SpR:13.0,616.2')] ).
cnf(743,plain,
( ~ p(u)
| ~ p(enc(i(i(tmk)),v))
| p(enc(v,enc(i(pp),u))) ),
inference(spr,[status(thm),theory(equality)],[13,560]),
[iquote('0:SpR:13.0,560.2')] ).
cnf(517,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(i(enc(i(wk),v))))
| ~ p(w)
| p(enc(enc(i(wk),u),w)) ),
inference(sor,[status(thm)],[146,15]),
[iquote('0:SoR:146.2,15.2')] ).
cnf(741,plain,
( ~ p(enc(i(i(pp)),u))
| ~ p(v)
| p(enc(enc(i(tmk),v),u)) ),
inference(spr,[status(thm),theory(equality)],[13,560]),
[iquote('0:SpR:13.0,560.2')] ).
cnf(732,plain,
( ~ p(u)
| ~ p(enc(i(i(enc(i(zcmk),u))),v))
| p(enc(w__dfg,v)) ),
inference(spr,[status(thm),theory(equality)],[13,463]),
[iquote('0:SpR:13.0,463.2')] ).
cnf(730,plain,
( ~ p(enc(i(i(zcmk)),u))
| ~ p(v)
| p(enc(w__dfg,enc(i(u),v))) ),
inference(spr,[status(thm),theory(equality)],[13,463]),
[iquote('0:SpR:13.0,463.2')] ).
cnf(709,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(tc))
| p(enc(enc(i(tmk),u),v)) ),
inference(sor,[status(thm)],[258,11]),
[iquote('0:SoR:258.1,11.1')] ).
cnf(489,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(i(wk)))
| ~ p(w)
| p(enc(w,enc(i(enc(i(wk),u)),v))) ),
inference(sor,[status(thm)],[148,15]),
[iquote('0:SoR:148.0,15.2')] ).
cnf(634,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(lp))
| p(enc(enc(i(wk),u),v)) ),
inference(sor,[status(thm)],[244,11]),
[iquote('0:SoR:244.1,11.1')] ).
cnf(606,plain,
( ~ p(enc(i(i(wk)),u))
| ~ p(v)
| p(enc(u,enc(i(w__dfg),v))) ),
inference(spr,[status(thm),theory(equality)],[13,429]),
[iquote('0:SpR:13.0,429.2')] ).
cnf(604,plain,
( ~ p(u)
| ~ p(enc(i(i(w__dfg)),v))
| p(enc(enc(i(wk),u),v)) ),
inference(spr,[status(thm),theory(equality)],[13,429]),
[iquote('0:SpR:13.0,429.2')] ).
cnf(573,plain,
( ~ p(u)
| ~ p(enc(i(i(enc(i(wk),u))),v))
| p(enc(w__dfg,v)) ),
inference(spr,[status(thm),theory(equality)],[13,383]),
[iquote('0:SpR:13.0,383.2')] ).
cnf(477,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(i(enc(i(tmk),v))))
| ~ p(w)
| p(enc(enc(i(wk),u),w)) ),
inference(sor,[status(thm)],[129,15]),
[iquote('0:SoR:129.2,15.2')] ).
cnf(571,plain,
( ~ p(enc(i(i(wk)),u))
| ~ p(v)
| p(enc(w__dfg,enc(i(u),v))) ),
inference(spr,[status(thm),theory(equality)],[13,383]),
[iquote('0:SpR:13.0,383.2')] ).
cnf(568,plain,
( ~ p(u)
| ~ p(enc(i(i(enc(i(wk),u))),v))
| p(enc(pp,v)) ),
inference(spr,[status(thm),theory(equality)],[13,381]),
[iquote('0:SpR:13.0,381.2')] ).
cnf(566,plain,
( ~ p(enc(i(i(wk)),u))
| ~ p(v)
| p(enc(pp,enc(i(u),v))) ),
inference(spr,[status(thm),theory(equality)],[13,381]),
[iquote('0:SpR:13.0,381.2')] ).
cnf(544,plain,
( ~ p(enc(i(i(wk)),u))
| ~ p(v)
| p(enc(u,enc(i(pp),v))) ),
inference(spr,[status(thm),theory(equality)],[13,369]),
[iquote('0:SpR:13.0,369.2')] ).
cnf(458,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(i(wk)))
| ~ p(w)
| p(enc(w,enc(i(enc(i(tmk),u)),v))) ),
inference(sor,[status(thm)],[131,15]),
[iquote('0:SoR:131.0,15.2')] ).
cnf(542,plain,
( ~ p(u)
| ~ p(enc(i(i(pp)),v))
| p(enc(enc(i(wk),u),v)) ),
inference(spr,[status(thm),theory(equality)],[13,369]),
[iquote('0:SpR:13.0,369.2')] ).
cnf(527,plain,
( ~ p(enc(i(i(wk)),u))
| ~ p(v)
| p(enc(u,enc(i(tmk),v))) ),
inference(spr,[status(thm),theory(equality)],[13,352]),
[iquote('0:SpR:13.0,352.2')] ).
cnf(525,plain,
( ~ p(u)
| ~ p(enc(i(i(tmk)),v))
| p(enc(enc(i(wk),u),v)) ),
inference(spr,[status(thm),theory(equality)],[13,352]),
[iquote('0:SpR:13.0,352.2')] ).
cnf(511,plain,
( ~ p(enc(i(i(wk)),u))
| ~ p(v)
| p(enc(u,enc(i(tc),v))) ),
inference(spr,[status(thm),theory(equality)],[13,350]),
[iquote('0:SpR:13.0,350.2')] ).
cnf(233,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| p(enc(i(enc(i(zcmk),u)),enc(i(enc(i(zcmk),w)),v))) ),
inference(sor,[status(thm)],[119,18]),
[iquote('0:SoR:119.1,18.2')] ).
cnf(509,plain,
( ~ p(u)
| ~ p(enc(i(i(tc)),v))
| p(enc(enc(i(wk),u),v)) ),
inference(spr,[status(thm),theory(equality)],[13,350]),
[iquote('0:SpR:13.0,350.2')] ).
cnf(453,plain,
( ~ p(u)
| ~ p(enc(i(i(enc(i(tmk),u))),v))
| p(enc(w__dfg,v)) ),
inference(spr,[status(thm),theory(equality)],[13,330]),
[iquote('0:SpR:13.0,330.2')] ).
cnf(451,plain,
( ~ p(enc(i(i(tmk)),u))
| ~ p(v)
| p(enc(w__dfg,enc(i(u),v))) ),
inference(spr,[status(thm),theory(equality)],[13,330]),
[iquote('0:SpR:13.0,330.2')] ).
cnf(423,plain,
( ~ p(u)
| ~ p(enc(i(i(enc(i(tmk),u))),v))
| p(enc(pp,v)) ),
inference(spr,[status(thm),theory(equality)],[13,328]),
[iquote('0:SpR:13.0,328.2')] ).
cnf(382,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| p(enc(enc(i(tmk),w),enc(i(enc(i(wk),u)),v))) ),
inference(sor,[status(thm)],[149,14]),
[iquote('0:SoR:149.0,14.1')] ).
cnf(421,plain,
( ~ p(enc(i(i(tmk)),u))
| ~ p(v)
| p(enc(pp,enc(i(u),v))) ),
inference(spr,[status(thm),theory(equality)],[13,328]),
[iquote('0:SpR:13.0,328.2')] ).
cnf(323,plain,
( ~ p(enc(i(i(enc(i(zcmk),u))),v))
| ~ p(u)
| p(enc(pp,v)) ),
inference(spr,[status(thm),theory(equality)],[13,228]),
[iquote('0:SpR:13.0,228.2')] ).
cnf(321,plain,
( ~ p(u)
| ~ p(enc(i(i(zcmk)),v))
| p(enc(pp,enc(i(v),u))) ),
inference(spr,[status(thm),theory(equality)],[13,228]),
[iquote('0:SpR:13.0,228.2')] ).
cnf(314,plain,
( ~ p(enc(i(i(enc(i(zcmk),u))),v))
| ~ p(u)
| p(enc(v,pp)) ),
inference(spr,[status(thm),theory(equality)],[13,200]),
[iquote('0:SpR:13.0,200.2')] ).
cnf(329,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| p(enc(enc(i(tmk),w),enc(i(enc(i(tmk),u)),v))) ),
inference(sor,[status(thm)],[132,14]),
[iquote('0:SoR:132.0,14.1')] ).
cnf(312,plain,
( ~ p(u)
| ~ p(enc(i(i(zcmk)),v))
| p(enc(enc(i(v),u),pp)) ),
inference(spr,[status(thm),theory(equality)],[13,200]),
[iquote('0:SpR:13.0,200.2')] ).
cnf(307,plain,
( ~ p(enc(i(i(enc(i(zcmk),u))),v))
| ~ p(u)
| p(enc(v,k)) ),
inference(spr,[status(thm),theory(equality)],[13,183]),
[iquote('0:SpR:13.0,183.2')] ).
cnf(305,plain,
( ~ p(u)
| ~ p(enc(i(i(zcmk)),v))
| p(enc(enc(i(v),u),k)) ),
inference(spr,[status(thm),theory(equality)],[13,183]),
[iquote('0:SpR:13.0,183.2')] ).
cnf(299,plain,
( ~ p(enc(i(i(enc(i(zcmk),u))),v))
| ~ p(u)
| p(enc(v,t2)) ),
inference(spr,[status(thm),theory(equality)],[13,162]),
[iquote('0:SpR:13.0,162.2')] ).
cnf(203,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| p(enc(enc(i(enc(i(zcmk),w)),v),enc(i(tmk),u))) ),
inference(sor,[status(thm)],[93,18]),
[iquote('0:SoR:93.0,18.2')] ).
cnf(297,plain,
( ~ p(u)
| ~ p(enc(i(i(zcmk)),v))
| p(enc(enc(i(v),u),t2)) ),
inference(spr,[status(thm),theory(equality)],[13,162]),
[iquote('0:SpR:13.0,162.2')] ).
cnf(288,plain,
( ~ p(u)
| ~ p(enc(i(i(tmk)),v))
| p(enc(v,enc(i(lp),u))) ),
inference(spr,[status(thm),theory(equality)],[13,156]),
[iquote('0:SpR:13.0,156.2')] ).
cnf(286,plain,
( ~ p(enc(i(i(lp)),u))
| ~ p(v)
| p(enc(enc(i(tmk),v),u)) ),
inference(spr,[status(thm),theory(equality)],[13,156]),
[iquote('0:SpR:13.0,156.2')] ).
cnf(277,plain,
( ~ p(enc(i(i(enc(i(zcmk),u))),v))
| ~ p(u)
| p(enc(wk,v)) ),
inference(spr,[status(thm),theory(equality)],[13,104]),
[iquote('0:SpR:13.0,104.2')] ).
cnf(188,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| p(enc(enc(i(tmk),u),enc(i(enc(i(zcmk),w)),v))) ),
inference(sor,[status(thm)],[91,18]),
[iquote('0:SoR:91.1,18.2')] ).
cnf(275,plain,
( ~ p(u)
| ~ p(enc(i(i(zcmk)),v))
| p(enc(wk,enc(i(v),u))) ),
inference(spr,[status(thm),theory(equality)],[13,104]),
[iquote('0:SpR:13.0,104.2')] ).
cnf(790,plain,
( ~ p(u)
| ~ p(enc(tmk,v))
| p(enc(v,enc(i(w__dfg),u))) ),
inference(spr,[status(thm),theory(equality)],[12,724]),
[iquote('0:SpR:12.0,724.2')] ).
cnf(788,plain,
( ~ p(enc(w__dfg,u))
| ~ p(v)
| p(enc(enc(i(tmk),v),u)) ),
inference(spr,[status(thm),theory(equality)],[12,724]),
[iquote('0:SpR:12.0,724.2')] ).
cnf(724,plain,
( ~ p(u)
| ~ p(v)
| p(enc(enc(i(tmk),v),enc(i(w__dfg),u))) ),
inference(sor,[status(thm)],[607,14]),
[iquote('0:SoR:607.0,14.1')] ).
cnf(180,plain,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| p(enc(enc(i(enc(i(zcmk),w)),v),enc(i(tc),u))) ),
inference(sor,[status(thm)],[84,18]),
[iquote('0:SoR:84.0,18.2')] ).
cnf(773,plain,
( ~ p(u)
| ~ p(enc(enc(i(zcmk),u),v))
| p(enc(v,t1)) ),
inference(spr,[status(thm),theory(equality)],[12,616]),
[iquote('0:SpR:12.0,616.2')] ).
cnf(771,plain,
( ~ p(enc(zcmk,u))
| ~ p(v)
| p(enc(enc(i(u),v),t1)) ),
inference(spr,[status(thm),theory(equality)],[12,616]),
[iquote('0:SpR:12.0,616.2')] ).
cnf(616,plain,
( ~ p(u)
| ~ p(v)
| p(enc(enc(i(enc(i(zcmk),u)),v),t1)) ),
inference(sor,[status(thm)],[613,104]),
[iquote('0:SoR:613.0,104.2')] ).
cnf(744,plain,
( ~ p(u)
| ~ p(enc(tmk,v))
| p(enc(v,enc(i(pp),u))) ),
inference(spr,[status(thm),theory(equality)],[12,560]),
[iquote('0:SpR:12.0,560.2')] ).
cnf(317,plain,
( ~ p(u)
| ~ p(i(i(zcmk)))
| ~ p(v)
| p(enc(i(v),enc(i(tmk),u))) ),
inference(sor,[status(thm)],[120,15]),
[iquote('0:SoR:120.0,15.2')] ).
cnf(742,plain,
( ~ p(enc(pp,u))
| ~ p(v)
| p(enc(enc(i(tmk),v),u)) ),
inference(spr,[status(thm),theory(equality)],[12,560]),
[iquote('0:SpR:12.0,560.2')] ).
cnf(560,plain,
( ~ p(u)
| ~ p(v)
| p(enc(enc(i(tmk),v),enc(i(pp),u))) ),
inference(sor,[status(thm)],[545,14]),
[iquote('0:SoR:545.0,14.1')] ).
cnf(515,plain,
( ~ p(u)
| ~ p(tc)
| ~ p(v)
| p(enc(enc(i(wk),u),v)) ),
inference(sor,[status(thm)],[510,15]),
[iquote('0:SoR:510.1,15.2')] ).
cnf(733,plain,
( ~ p(u)
| ~ p(enc(enc(i(zcmk),u),v))
| p(enc(w__dfg,v)) ),
inference(spr,[status(thm),theory(equality)],[12,463]),
[iquote('0:SpR:12.0,463.2')] ).
cnf(284,plain,
( ~ p(u)
| ~ p(i(i(zcmk)))
| ~ p(v)
| p(enc(tmk,enc(i(v),u))) ),
inference(sor,[status(thm)],[106,15]),
[iquote('0:SoR:106.0,15.2')] ).
cnf(731,plain,
( ~ p(enc(zcmk,u))
| ~ p(v)
| p(enc(w__dfg,enc(i(u),v))) ),
inference(spr,[status(thm),theory(equality)],[12,463]),
[iquote('0:SpR:12.0,463.2')] ).
cnf(463,plain,
( ~ p(u)
| ~ p(v)
| p(enc(w__dfg,enc(i(enc(i(zcmk),u)),v))) ),
inference(sor,[status(thm)],[461,228]),
[iquote('0:SoR:461.0,228.2')] ).
cnf(607,plain,
( ~ p(enc(wk,u))
| ~ p(v)
| p(enc(u,enc(i(w__dfg),v))) ),
inference(spr,[status(thm),theory(equality)],[12,429]),
[iquote('0:SpR:12.0,429.2')] ).
cnf(605,plain,
( ~ p(u)
| ~ p(enc(w__dfg,v))
| p(enc(enc(i(wk),u),v)) ),
inference(spr,[status(thm),theory(equality)],[12,429]),
[iquote('0:SpR:12.0,429.2')] ).
cnf(258,plain,
( ~ p(u)
| ~ p(i(i(tc)))
| ~ p(v)
| p(enc(enc(i(tmk),u),v)) ),
inference(sor,[status(thm)],[81,15]),
[iquote('0:SoR:81.1,15.2')] ).
cnf(574,plain,
( ~ p(u)
| ~ p(enc(enc(i(wk),u),v))
| p(enc(w__dfg,v)) ),
inference(spr,[status(thm),theory(equality)],[12,383]),
[iquote('0:SpR:12.0,383.2')] ).
cnf(572,plain,
( ~ p(enc(wk,u))
| ~ p(v)
| p(enc(w__dfg,enc(i(u),v))) ),
inference(spr,[status(thm),theory(equality)],[12,383]),
[iquote('0:SpR:12.0,383.2')] ).
cnf(569,plain,
( ~ p(u)
| ~ p(enc(enc(i(wk),u),v))
| p(enc(pp,v)) ),
inference(spr,[status(thm),theory(equality)],[12,381]),
[iquote('0:SpR:12.0,381.2')] ).
cnf(636,plain,
( ~ p(i(i(wk)))
| ~ p(u)
| p(enc(u,t1)) ),
inference(sor,[status(thm)],[612,15]),
[iquote('0:SoR:612.0,15.2')] ).
cnf(254,plain,
( ~ p(u)
| ~ p(i(i(wk)))
| ~ p(v)
| p(enc(v,enc(i(lp),u))) ),
inference(sor,[status(thm)],[76,15]),
[iquote('0:SoR:76.0,15.2')] ).
cnf(635,plain,
( ~ p(i(i(w__dfg)))
| ~ p(u)
| p(enc(pp,u)) ),
inference(sor,[status(thm)],[584,15]),
[iquote('0:SoR:584.0,15.2')] ).
cnf(625,plain,
( ~ p(enc(i(i(tmk)),u))
| p(enc(u,t1)) ),
inference(spr,[status(thm),theory(equality)],[13,619]),
[iquote('0:SpR:13.0,619.1')] ).
cnf(612,plain,
( ~ p(enc(i(i(wk)),u))
| p(enc(u,t1)) ),
inference(spr,[status(thm),theory(equality)],[13,601]),
[iquote('0:SpR:13.0,601.1')] ).
cnf(584,plain,
( ~ p(enc(i(i(w__dfg)),u))
| p(enc(pp,u)) ),
inference(spr,[status(thm),theory(equality)],[13,579]),
[iquote('0:SpR:13.0,579.1')] ).
cnf(244,plain,
( ~ p(u)
| ~ p(i(i(lp)))
| ~ p(v)
| p(enc(enc(i(wk),u),v)) ),
inference(sor,[status(thm)],[74,15]),
[iquote('0:SoR:74.1,15.2')] ).
cnf(626,plain,
( ~ p(enc(tmk,u))
| p(enc(u,t1)) ),
inference(spr,[status(thm),theory(equality)],[12,619]),
[iquote('0:SpR:12.0,619.1')] ).
cnf(619,plain,
( ~ p(u)
| p(enc(enc(i(tmk),u),t1)) ),
inference(sor,[status(thm)],[613,14]),
[iquote('0:SoR:613.0,14.1')] ).
cnf(613,plain,
( ~ p(enc(wk,u))
| p(enc(u,t1)) ),
inference(spr,[status(thm),theory(equality)],[12,601]),
[iquote('0:SpR:12.0,601.1')] ).
cnf(601,plain,
( ~ p(u)
| p(enc(enc(i(wk),u),t1)) ),
inference(sor,[status(thm)],[543,595]),
[iquote('0:SoR:543.1,595.0')] ).
cnf(429,plain,
( ~ p(u)
| ~ p(v)
| p(enc(enc(i(wk),u),enc(i(w__dfg),v))) ),
inference(sor,[status(thm)],[145,5]),
[iquote('0:SoR:145.1,5.0')] ).
cnf(595,plain,
p(enc(pp,t1)),
inference(sor,[status(thm)],[585,6]),
[iquote('0:SoR:585.0,6.0')] ).
cnf(585,plain,
( ~ p(enc(w__dfg,u))
| p(enc(pp,u)) ),
inference(spr,[status(thm),theory(equality)],[12,579]),
[iquote('0:SpR:12.0,579.1')] ).
cnf(579,plain,
( ~ p(u)
| p(enc(pp,enc(i(w__dfg),u))) ),
inference(sor,[status(thm)],[567,5]),
[iquote('0:SoR:567.0,5.0')] ).
cnf(567,plain,
( ~ p(enc(wk,u))
| ~ p(v)
| p(enc(pp,enc(i(u),v))) ),
inference(spr,[status(thm),theory(equality)],[12,381]),
[iquote('0:SpR:12.0,381.2')] ).
cnf(383,plain,
( ~ p(u)
| ~ p(v)
| p(enc(w__dfg,enc(i(enc(i(wk),u)),v))) ),
inference(sor,[status(thm)],[149,5]),
[iquote('0:SoR:149.0,5.0')] ).
cnf(381,plain,
( ~ p(u)
| ~ p(v)
| p(enc(pp,enc(i(enc(i(wk),u)),v))) ),
inference(sor,[status(thm)],[149,44]),
[iquote('0:SoR:149.0,44.0')] ).
cnf(545,plain,
( ~ p(enc(wk,u))
| ~ p(v)
| p(enc(u,enc(i(pp),v))) ),
inference(spr,[status(thm),theory(equality)],[12,369]),
[iquote('0:SpR:12.0,369.2')] ).
cnf(543,plain,
( ~ p(u)
| ~ p(enc(pp,v))
| p(enc(enc(i(wk),u),v)) ),
inference(spr,[status(thm),theory(equality)],[12,369]),
[iquote('0:SpR:12.0,369.2')] ).
cnf(369,plain,
( ~ p(u)
| ~ p(v)
| p(enc(enc(i(wk),u),enc(i(pp),v))) ),
inference(sor,[status(thm)],[128,4]),
[iquote('0:SoR:128.1,4.0')] ).
cnf(144,plain,
( ~ p(u)
| ~ p(enc(i(i(wk)),v))
| ~ p(w)
| p(enc(enc(i(wk),u),enc(i(v),w))) ),
inference(spr,[status(thm),theory(equality)],[13,23]),
[iquote('0:SpR:13.0,23.3')] ).
cnf(528,plain,
( ~ p(enc(wk,u))
| ~ p(v)
| p(enc(u,enc(i(tmk),v))) ),
inference(spr,[status(thm),theory(equality)],[12,352]),
[iquote('0:SpR:12.0,352.2')] ).
cnf(526,plain,
( ~ p(u)
| ~ p(enc(tmk,v))
| p(enc(enc(i(wk),u),v)) ),
inference(spr,[status(thm),theory(equality)],[12,352]),
[iquote('0:SpR:12.0,352.2')] ).
cnf(352,plain,
( ~ p(u)
| ~ p(v)
| p(enc(enc(i(wk),u),enc(i(tmk),v))) ),
inference(con,[status(thm)],[351]),
[iquote('0:Con:351.2')] ).
cnf(512,plain,
( ~ p(enc(wk,u))
| ~ p(v)
| p(enc(u,enc(i(tc),v))) ),
inference(spr,[status(thm),theory(equality)],[12,350]),
[iquote('0:SpR:12.0,350.2')] ).
cnf(146,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(i(i(enc(i(wk),v))),w))
| p(enc(enc(i(wk),u),w)) ),
inference(spr,[status(thm),theory(equality)],[13,23]),
[iquote('0:SpR:13.0,23.3')] ).
cnf(510,plain,
( ~ p(u)
| ~ p(enc(tc,v))
| p(enc(enc(i(wk),u),v)) ),
inference(spr,[status(thm),theory(equality)],[12,350]),
[iquote('0:SpR:12.0,350.2')] ).
cnf(350,plain,
( ~ p(u)
| ~ p(v)
| p(enc(enc(i(wk),u),enc(i(tc),v))) ),
inference(con,[status(thm)],[349]),
[iquote('0:Con:349.2')] ).
cnf(454,plain,
( ~ p(u)
| ~ p(enc(enc(i(tmk),u),v))
| p(enc(w__dfg,v)) ),
inference(spr,[status(thm),theory(equality)],[12,330]),
[iquote('0:SpR:12.0,330.2')] ).
cnf(488,plain,
( ~ p(u)
| ~ p(i(tc))
| p(enc(w__dfg,u)) ),
inference(sor,[status(thm)],[486,11]),
[iquote('0:SoR:486.0,11.1')] ).
cnf(148,plain,
( ~ p(enc(i(i(wk)),u))
| ~ p(v)
| ~ p(w)
| p(enc(u,enc(i(enc(i(wk),v)),w))) ),
inference(spr,[status(thm),theory(equality)],[13,23]),
[iquote('0:SpR:13.0,23.3')] ).
cnf(486,plain,
( ~ p(i(i(tc)))
| ~ p(u)
| p(enc(w__dfg,u)) ),
inference(sor,[status(thm)],[479,15]),
[iquote('0:SoR:479.0,15.2')] ).
cnf(483,plain,
( ~ p(i(i(pp)))
| ~ p(u)
| p(enc(w__dfg,u)) ),
inference(sor,[status(thm)],[460,15]),
[iquote('0:SoR:460.0,15.2')] ).
cnf(479,plain,
( ~ p(enc(i(i(tc)),u))
| p(enc(w__dfg,u)) ),
inference(spr,[status(thm),theory(equality)],[13,465]),
[iquote('0:SpR:13.0,465.1')] ).
cnf(472,plain,
( ~ p(enc(i(i(tmk)),u))
| p(enc(w__dfg,u)) ),
inference(spr,[status(thm),theory(equality)],[13,464]),
[iquote('0:SpR:13.0,464.1')] ).
cnf(127,plain,
( ~ p(u)
| ~ p(enc(i(i(tmk)),v))
| ~ p(w)
| p(enc(enc(i(wk),u),enc(i(v),w))) ),
inference(spr,[status(thm),theory(equality)],[13,24]),
[iquote('0:SpR:13.0,24.3')] ).
cnf(460,plain,
( ~ p(enc(i(i(pp)),u))
| p(enc(w__dfg,u)) ),
inference(spr,[status(thm),theory(equality)],[13,457]),
[iquote('0:SpR:13.0,457.1')] ).
cnf(481,plain,
( ~ p(tc)
| ~ p(u)
| p(enc(w__dfg,u)) ),
inference(sor,[status(thm)],[480,15]),
[iquote('0:SoR:480.0,15.2')] ).
cnf(480,plain,
( ~ p(enc(tc,u))
| p(enc(w__dfg,u)) ),
inference(spr,[status(thm),theory(equality)],[12,465]),
[iquote('0:SpR:12.0,465.1')] ).
cnf(465,plain,
( ~ p(u)
| p(enc(w__dfg,enc(i(tc),u))) ),
inference(sor,[status(thm)],[461,181]),
[iquote('0:SoR:461.0,181.1')] ).
cnf(129,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(i(i(enc(i(tmk),v))),w))
| p(enc(enc(i(wk),u),w)) ),
inference(spr,[status(thm),theory(equality)],[13,24]),
[iquote('0:SpR:13.0,24.3')] ).
cnf(473,plain,
( ~ p(enc(tmk,u))
| p(enc(w__dfg,u)) ),
inference(spr,[status(thm),theory(equality)],[12,464]),
[iquote('0:SpR:12.0,464.1')] ).
cnf(464,plain,
( ~ p(u)
| p(enc(w__dfg,enc(i(tmk),u))) ),
inference(sor,[status(thm)],[461,204]),
[iquote('0:SoR:461.0,204.1')] ).
cnf(461,plain,
( ~ p(enc(pp,u))
| p(enc(w__dfg,u)) ),
inference(spr,[status(thm),theory(equality)],[12,457]),
[iquote('0:SpR:12.0,457.1')] ).
cnf(457,plain,
( ~ p(u)
| p(enc(w__dfg,enc(i(pp),u))) ),
inference(sor,[status(thm)],[452,4]),
[iquote('0:SoR:452.0,4.0')] ).
cnf(131,plain,
( ~ p(enc(i(i(wk)),u))
| ~ p(v)
| ~ p(w)
| p(enc(u,enc(i(enc(i(tmk),v)),w))) ),
inference(spr,[status(thm),theory(equality)],[13,24]),
[iquote('0:SpR:13.0,24.3')] ).
cnf(452,plain,
( ~ p(enc(tmk,u))
| ~ p(v)
| p(enc(w__dfg,enc(i(u),v))) ),
inference(spr,[status(thm),theory(equality)],[12,330]),
[iquote('0:SpR:12.0,330.2')] ).
cnf(330,plain,
( ~ p(u)
| ~ p(v)
| p(enc(w__dfg,enc(i(enc(i(tmk),u)),v))) ),
inference(sor,[status(thm)],[132,5]),
[iquote('0:SoR:132.0,5.0')] ).
cnf(424,plain,
( ~ p(u)
| ~ p(enc(enc(i(tmk),u),v))
| p(enc(pp,v)) ),
inference(spr,[status(thm),theory(equality)],[12,328]),
[iquote('0:SpR:12.0,328.2')] ).
cnf(422,plain,
( ~ p(enc(tmk,u))
| ~ p(v)
| p(enc(pp,enc(i(u),v))) ),
inference(spr,[status(thm),theory(equality)],[12,328]),
[iquote('0:SpR:12.0,328.2')] ).
cnf(145,plain,
( ~ p(u)
| ~ p(enc(wk,v))
| ~ p(w)
| p(enc(enc(i(wk),u),enc(i(v),w))) ),
inference(spr,[status(thm),theory(equality)],[12,23]),
[iquote('0:SpR:12.0,23.3')] ).
cnf(328,plain,
( ~ p(u)
| ~ p(v)
| p(enc(pp,enc(i(enc(i(tmk),u)),v))) ),
inference(sor,[status(thm)],[132,44]),
[iquote('0:SoR:132.0,44.0')] ).
cnf(332,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(i(enc(i(zcmk),u)),v)) ),
inference(sor,[status(thm)],[316,11]),
[iquote('0:SoR:316.0,11.1')] ).
cnf(389,plain,
( ~ p(i(i(wk)))
| ~ p(u)
| p(enc(u,k)) ),
inference(sor,[status(thm)],[371,15]),
[iquote('0:SoR:371.0,15.2')] ).
cnf(388,plain,
( ~ p(i(i(wk)))
| ~ p(u)
| p(enc(u,pp)) ),
inference(sor,[status(thm)],[356,15]),
[iquote('0:SoR:356.0,15.2')] ).
cnf(147,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(enc(i(wk),v),w))
| p(enc(enc(i(wk),u),w)) ),
inference(spr,[status(thm),theory(equality)],[12,23]),
[iquote('0:SpR:12.0,23.3')] ).
cnf(371,plain,
( ~ p(enc(i(i(wk)),u))
| p(enc(u,k)) ),
inference(spr,[status(thm),theory(equality)],[13,348]),
[iquote('0:SpR:13.0,348.1')] ).
cnf(356,plain,
( ~ p(enc(i(i(wk)),u))
| p(enc(u,pp)) ),
inference(spr,[status(thm),theory(equality)],[13,344]),
[iquote('0:SpR:13.0,344.1')] ).
cnf(384,plain,
( ~ p(u)
| ~ p(enc(i(wk),u)) ),
inference(sor,[status(thm)],[358,11]),
[iquote('0:SoR:358.0,11.1')] ).
cnf(358,plain,
( ~ p(i(enc(i(wk),u)))
| ~ p(u) ),
inference(mrr,[status(thm)],[355,26]),
[iquote('0:MRR:355.2,26.0')] ).
cnf(149,plain,
( ~ p(enc(wk,u))
| ~ p(v)
| ~ p(w)
| p(enc(u,enc(i(enc(i(wk),v)),w))) ),
inference(spr,[status(thm),theory(equality)],[12,23]),
[iquote('0:SpR:12.0,23.3')] ).
cnf(377,plain,
p(enc(w__dfg,k)),
inference(sor,[status(thm)],[372,5]),
[iquote('0:SoR:372.0,5.0')] ).
cnf(372,plain,
( ~ p(enc(wk,u))
| p(enc(u,k)) ),
inference(spr,[status(thm),theory(equality)],[12,348]),
[iquote('0:SpR:12.0,348.1')] ).
cnf(348,plain,
( ~ p(u)
| p(enc(enc(i(wk),u),k)) ),
inference(con,[status(thm)],[347]),
[iquote('0:Con:347.1')] ).
cnf(366,plain,
~ p(w__dfg),
inference(sor,[status(thm)],[365,11]),
[iquote('0:SoR:365.0,11.1')] ).
cnf(128,plain,
( ~ p(u)
| ~ p(enc(tmk,v))
| ~ p(w)
| p(enc(enc(i(wk),u),enc(i(v),w))) ),
inference(spr,[status(thm),theory(equality)],[12,24]),
[iquote('0:SpR:12.0,24.3')] ).
cnf(365,plain,
~ p(i(w__dfg)),
inference(mrr,[status(thm)],[364,26]),
[iquote('0:MRR:364.1,26.0')] ).
cnf(363,plain,
p(enc(w__dfg,pp)),
inference(sor,[status(thm)],[357,5]),
[iquote('0:SoR:357.0,5.0')] ).
cnf(357,plain,
( ~ p(enc(wk,u))
| p(enc(u,pp)) ),
inference(spr,[status(thm),theory(equality)],[12,344]),
[iquote('0:SpR:12.0,344.1')] ).
cnf(344,plain,
( ~ p(u)
| p(enc(enc(i(wk),u),pp)) ),
inference(con,[status(thm)],[343]),
[iquote('0:Con:343.1')] ).
cnf(130,plain,
( ~ p(u)
| ~ p(v)
| ~ p(enc(enc(i(tmk),v),w))
| p(enc(enc(i(wk),u),w)) ),
inference(spr,[status(thm),theory(equality)],[12,24]),
[iquote('0:SpR:12.0,24.3')] ).
cnf(334,plain,
~ p(i(i(tmk))),
inference(con,[status(thm)],[333]),
[iquote('0:Con:333.0')] ).
cnf(316,plain,
( ~ p(i(enc(i(enc(i(zcmk),u)),v)))
| ~ p(u)
| ~ p(v) ),
inference(mrr,[status(thm)],[311,26]),
[iquote('0:MRR:311.3,26.0')] ).
cnf(290,plain,
( ~ p(u)
| ~ p(lp)
| ~ p(v)
| p(enc(enc(i(tmk),u),v)) ),
inference(sor,[status(thm)],[287,15]),
[iquote('0:SoR:287.0,15.2')] ).
cnf(324,plain,
( ~ p(enc(enc(i(zcmk),u),v))
| ~ p(u)
| p(enc(pp,v)) ),
inference(spr,[status(thm),theory(equality)],[12,228]),
[iquote('0:SpR:12.0,228.2')] ).
cnf(132,plain,
( ~ p(enc(wk,u))
| ~ p(v)
| ~ p(w)
| p(enc(u,enc(i(enc(i(tmk),v)),w))) ),
inference(spr,[status(thm),theory(equality)],[12,24]),
[iquote('0:SpR:12.0,24.3')] ).
cnf(322,plain,
( ~ p(u)
| ~ p(enc(zcmk,v))
| p(enc(pp,enc(i(v),u))) ),
inference(spr,[status(thm),theory(equality)],[12,228]),
[iquote('0:SpR:12.0,228.2')] ).
cnf(228,plain,
( ~ p(u)
| ~ p(v)
| p(enc(pp,enc(i(enc(i(zcmk),v)),u))) ),
inference(sor,[status(thm)],[221,18]),
[iquote('0:SoR:221.0,18.2')] ).
cnf(315,plain,
( ~ p(enc(enc(i(zcmk),u),v))
| ~ p(u)
| p(enc(v,pp)) ),
inference(spr,[status(thm),theory(equality)],[12,200]),
[iquote('0:SpR:12.0,200.2')] ).
cnf(313,plain,
( ~ p(u)
| ~ p(enc(zcmk,v))
| p(enc(enc(i(v),u),pp)) ),
inference(spr,[status(thm),theory(equality)],[12,200]),
[iquote('0:SpR:12.0,200.2')] ).
cnf(120,plain,
( ~ p(enc(i(i(zcmk)),u))
| ~ p(v)
| p(enc(i(u),enc(i(tmk),v))) ),
inference(spr,[status(thm),theory(equality)],[13,22]),
[iquote('0:SpR:13.0,22.2')] ).
cnf(200,plain,
( ~ p(u)
| ~ p(v)
| p(enc(enc(i(enc(i(zcmk),v)),u),pp)) ),
inference(sor,[status(thm)],[197,18]),
[iquote('0:SoR:197.0,18.2')] ).
cnf(308,plain,
( ~ p(enc(enc(i(zcmk),u),v))
| ~ p(u)
| p(enc(v,k)) ),
inference(spr,[status(thm),theory(equality)],[12,183]),
[iquote('0:SpR:12.0,183.2')] ).
cnf(306,plain,
( ~ p(u)
| ~ p(enc(zcmk,v))
| p(enc(enc(i(v),u),k)) ),
inference(spr,[status(thm),theory(equality)],[12,183]),
[iquote('0:SpR:12.0,183.2')] ).
cnf(183,plain,
( ~ p(u)
| ~ p(v)
| p(enc(enc(i(enc(i(zcmk),v)),u),k)) ),
inference(sor,[status(thm)],[178,18]),
[iquote('0:SoR:178.0,18.2')] ).
cnf(118,plain,
( ~ p(u)
| ~ p(enc(i(i(tmk)),v))
| p(enc(i(enc(i(zcmk),u)),v)) ),
inference(spr,[status(thm),theory(equality)],[13,22]),
[iquote('0:SpR:13.0,22.2')] ).
cnf(169,plain,
( ~ p(u)
| ~ p(tc)
| ~ p(v)
| p(enc(enc(i(tmk),u),v)) ),
inference(sor,[status(thm)],[82,15]),
[iquote('0:SoR:82.1,15.2')] ).
cnf(300,plain,
( ~ p(enc(enc(i(zcmk),u),v))
| ~ p(u)
| p(enc(v,t2)) ),
inference(spr,[status(thm),theory(equality)],[12,162]),
[iquote('0:SpR:12.0,162.2')] ).
cnf(298,plain,
( ~ p(u)
| ~ p(enc(zcmk,v))
| p(enc(enc(i(v),u),t2)) ),
inference(spr,[status(thm),theory(equality)],[12,162]),
[iquote('0:SpR:12.0,162.2')] ).
cnf(162,plain,
( ~ p(u)
| ~ p(v)
| p(enc(enc(i(enc(i(zcmk),v)),u),t2)) ),
inference(sor,[status(thm)],[160,18]),
[iquote('0:SoR:160.0,18.2')] ).
cnf(108,plain,
( ~ p(u)
| ~ p(enc(i(i(enc(i(zcmk),u))),v))
| p(enc(tmk,v)) ),
inference(spr,[status(thm),theory(equality)],[13,18]),
[iquote('0:SpR:13.0,18.2')] ).
cnf(289,plain,
( ~ p(u)
| ~ p(enc(tmk,v))
| p(enc(v,enc(i(lp),u))) ),
inference(spr,[status(thm),theory(equality)],[12,156]),
[iquote('0:SpR:12.0,156.2')] ).
cnf(287,plain,
( ~ p(enc(lp,u))
| ~ p(v)
| p(enc(enc(i(tmk),v),u)) ),
inference(spr,[status(thm),theory(equality)],[12,156]),
[iquote('0:SpR:12.0,156.2')] ).
cnf(156,plain,
( ~ p(u)
| ~ p(v)
| p(enc(enc(i(tmk),v),enc(i(lp),u))) ),
inference(sor,[status(thm)],[77,14]),
[iquote('0:SoR:77.0,14.1')] ).
cnf(133,plain,
( ~ p(u)
| ~ p(lp)
| ~ p(v)
| p(enc(enc(i(wk),u),v)) ),
inference(sor,[status(thm)],[75,15]),
[iquote('0:SoR:75.1,15.2')] ).
cnf(106,plain,
( ~ p(enc(i(i(zcmk)),u))
| ~ p(v)
| p(enc(tmk,enc(i(u),v))) ),
inference(spr,[status(thm),theory(equality)],[13,18]),
[iquote('0:SpR:13.0,18.2')] ).
cnf(282,plain,
( ~ p(u)
| ~ p(v)
| ~ p(i(tc))
| p(enc(i(v),u)) ),
inference(sor,[status(thm)],[124,11]),
[iquote('0:SoR:124.1,11.1')] ).
cnf(124,plain,
( ~ p(u)
| ~ p(i(i(tc)))
| ~ p(v)
| p(enc(i(v),u)) ),
inference(sor,[status(thm)],[67,15]),
[iquote('0:SoR:67.1,15.2')] ).
cnf(278,plain,
( ~ p(enc(enc(i(zcmk),u),v))
| ~ p(u)
| p(enc(wk,v)) ),
inference(spr,[status(thm),theory(equality)],[12,104]),
[iquote('0:SpR:12.0,104.2')] ).
cnf(276,plain,
( ~ p(u)
| ~ p(enc(zcmk,v))
| p(enc(wk,enc(i(v),u))) ),
inference(spr,[status(thm),theory(equality)],[12,104]),
[iquote('0:SpR:12.0,104.2')] ).
cnf(92,plain,
( ~ p(enc(i(i(tmk)),u))
| ~ p(v)
| p(enc(u,enc(i(tmk),v))) ),
inference(spr,[status(thm),theory(equality)],[13,19]),
[iquote('0:SpR:13.0,19.2')] ).
cnf(104,plain,
( ~ p(u)
| ~ p(v)
| p(enc(wk,enc(i(enc(i(zcmk),v)),u))) ),
inference(sor,[status(thm)],[43,18]),
[iquote('0:SoR:43.0,18.2')] ).
cnf(270,plain,
( ~ p(i(i(zcmk)))
| ~ p(u)
| p(enc(i(u),pp)) ),
inference(sor,[status(thm)],[247,15]),
[iquote('0:SoR:247.0,15.2')] ).
cnf(247,plain,
( ~ p(enc(i(i(zcmk)),u))
| p(enc(i(u),pp)) ),
inference(spr,[status(thm),theory(equality)],[13,234]),
[iquote('0:SpR:13.0,234.1')] ).
cnf(90,plain,
( ~ p(u)
| ~ p(enc(i(i(tmk)),v))
| p(enc(enc(i(tmk),u),v)) ),
inference(spr,[status(thm),theory(equality)],[13,19]),
[iquote('0:SpR:13.0,19.2')] ).
cnf(265,plain,
( ~ p(u)
| ~ p(i(tc))
| p(enc(pp,u)) ),
inference(sor,[status(thm)],[238,11]),
[iquote('0:SoR:238.0,11.1')] ).
cnf(238,plain,
( ~ p(i(i(tc)))
| ~ p(u)
| p(enc(pp,u)) ),
inference(sor,[status(thm)],[191,15]),
[iquote('0:SoR:191.0,15.2')] ).
cnf(83,plain,
( ~ p(enc(i(i(tmk)),u))
| ~ p(v)
| p(enc(u,enc(i(tc),v))) ),
inference(spr,[status(thm),theory(equality)],[13,20]),
[iquote('0:SpR:13.0,20.2')] ).
cnf(261,plain,
( ~ p(u)
| ~ p(i(lp))
| p(enc(w__dfg,u)) ),
inference(sor,[status(thm)],[236,11]),
[iquote('0:SoR:236.0,11.1')] ).
cnf(236,plain,
( ~ p(i(i(lp)))
| ~ p(u)
| p(enc(w__dfg,u)) ),
inference(sor,[status(thm)],[172,15]),
[iquote('0:SoR:172.0,15.2')] ).
cnf(259,plain,
( ~ p(u)
| ~ p(i(lp))
| p(enc(pp,u)) ),
inference(sor,[status(thm)],[235,11]),
[iquote('0:SoR:235.0,11.1')] ).
cnf(235,plain,
( ~ p(i(i(lp)))
| ~ p(u)
| p(enc(pp,u)) ),
inference(sor,[status(thm)],[165,15]),
[iquote('0:SoR:165.0,15.2')] ).
cnf(81,plain,
( ~ p(u)
| ~ p(enc(i(i(tc)),v))
| p(enc(enc(i(tmk),u),v)) ),
inference(spr,[status(thm),theory(equality)],[13,20]),
[iquote('0:SpR:13.0,20.2')] ).
cnf(230,plain,
( ~ p(i(i(wk)))
| ~ p(u)
| p(enc(u,t2)) ),
inference(sor,[status(thm)],[136,15]),
[iquote('0:SoR:136.0,15.2')] ).
cnf(76,plain,
( ~ p(enc(i(i(wk)),u))
| ~ p(v)
| p(enc(u,enc(i(lp),v))) ),
inference(spr,[status(thm),theory(equality)],[13,21]),
[iquote('0:SpR:13.0,21.2')] ).
cnf(248,plain,
( ~ p(enc(zcmk,u))
| p(enc(i(u),pp)) ),
inference(spr,[status(thm),theory(equality)],[12,234]),
[iquote('0:SpR:12.0,234.1')] ).
cnf(234,plain,
( ~ p(u)
| p(enc(i(enc(i(zcmk),u)),pp)) ),
inference(sor,[status(thm)],[119,4]),
[iquote('0:SoR:119.1,4.0')] ).
cnf(74,plain,
( ~ p(u)
| ~ p(enc(i(i(lp)),v))
| p(enc(enc(i(wk),u),v)) ),
inference(spr,[status(thm),theory(equality)],[13,21]),
[iquote('0:SpR:13.0,21.2')] ).
cnf(220,plain,
( ~ p(enc(i(i(tmk)),u))
| p(enc(pp,u)) ),
inference(spr,[status(thm),theory(equality)],[13,204]),
[iquote('0:SpR:13.0,204.1')] ).
cnf(241,plain,
( ~ p(u)
| ~ p(i(enc(i(zcmk),u))) ),
inference(sor,[status(thm)],[210,11]),
[iquote('0:SoR:210.0,11.1')] ).
cnf(210,plain,
( ~ p(i(i(enc(i(zcmk),u))))
| ~ p(u) ),
inference(con,[status(thm)],[208]),
[iquote('0:Con:208.1')] ).
cnf(196,plain,
( ~ p(enc(i(i(tmk)),u))
| p(enc(u,pp)) ),
inference(spr,[status(thm),theory(equality)],[13,189]),
[iquote('0:SpR:13.0,189.1')] ).
cnf(121,plain,
( ~ p(enc(zcmk,u))
| ~ p(v)
| p(enc(i(u),enc(i(tmk),v))) ),
inference(spr,[status(thm),theory(equality)],[12,22]),
[iquote('0:SpR:12.0,22.2')] ).
cnf(191,plain,
( ~ p(enc(i(i(tc)),u))
| p(enc(pp,u)) ),
inference(spr,[status(thm),theory(equality)],[13,181]),
[iquote('0:SpR:13.0,181.1')] ).
cnf(177,plain,
( ~ p(enc(i(i(tmk)),u))
| p(enc(u,k)) ),
inference(spr,[status(thm),theory(equality)],[13,170]),
[iquote('0:SpR:13.0,170.1')] ).
cnf(172,plain,
( ~ p(enc(i(i(lp)),u))
| p(enc(w__dfg,u)) ),
inference(spr,[status(thm),theory(equality)],[13,157]),
[iquote('0:SpR:13.0,157.1')] ).
cnf(165,plain,
( ~ p(enc(i(i(lp)),u))
| p(enc(pp,u)) ),
inference(spr,[status(thm),theory(equality)],[13,155]),
[iquote('0:SpR:13.0,155.1')] ).
cnf(119,plain,
( ~ p(u)
| ~ p(enc(tmk,v))
| p(enc(i(enc(i(zcmk),u)),v)) ),
inference(spr,[status(thm),theory(equality)],[12,22]),
[iquote('0:SpR:12.0,22.2')] ).
cnf(159,plain,
( ~ p(enc(i(i(tmk)),u))
| p(enc(u,t2)) ),
inference(spr,[status(thm),theory(equality)],[13,140]),
[iquote('0:SpR:13.0,140.1')] ).
cnf(136,plain,
( ~ p(enc(i(i(wk)),u))
| p(enc(u,t2)) ),
inference(spr,[status(thm),theory(equality)],[13,134]),
[iquote('0:SpR:13.0,134.1')] ).
cnf(221,plain,
( ~ p(enc(tmk,u))
| p(enc(pp,u)) ),
inference(spr,[status(thm),theory(equality)],[12,204]),
[iquote('0:SpR:12.0,204.1')] ).
cnf(223,plain,
~ p(i(pp)),
inference(mrr,[status(thm)],[142,222]),
[iquote('0:MRR:142.1,222.1')] ).
cnf(109,plain,
( ~ p(u)
| ~ p(enc(enc(i(zcmk),u),v))
| p(enc(tmk,v)) ),
inference(spr,[status(thm),theory(equality)],[12,18]),
[iquote('0:SpR:12.0,18.2')] ).
cnf(204,plain,
( ~ p(u)
| p(enc(pp,enc(i(tmk),u))) ),
inference(sor,[status(thm)],[93,4]),
[iquote('0:SoR:93.0,4.0')] ).
cnf(218,plain,
~ p(zcmk),
inference(sor,[status(thm)],[217,11]),
[iquote('0:SoR:217.0,11.1')] ).
cnf(217,plain,
~ p(i(zcmk)),
inference(con,[status(thm)],[216]),
[iquote('0:Con:216.1')] ).
cnf(209,plain,
( ~ p(enc(i(zcmk),u))
| ~ p(u) ),
inference(con,[status(thm)],[207]),
[iquote('0:Con:207.1')] ).
cnf(107,plain,
( ~ p(enc(zcmk,u))
| ~ p(v)
| p(enc(tmk,enc(i(u),v))) ),
inference(spr,[status(thm),theory(equality)],[12,18]),
[iquote('0:SpR:12.0,18.2')] ).
cnf(206,plain,
( ~ p(u)
| ~ p(enc(i(tmk),u)) ),
inference(sor,[status(thm)],[198,11]),
[iquote('0:SoR:198.0,11.1')] ).
cnf(198,plain,
( ~ p(i(enc(i(tmk),u)))
| ~ p(u) ),
inference(mrr,[status(thm)],[195,26]),
[iquote('0:MRR:195.2,26.0')] ).
cnf(193,plain,
( ~ p(tc)
| ~ p(u)
| p(enc(pp,u)) ),
inference(sor,[status(thm)],[192,15]),
[iquote('0:SoR:192.0,15.2')] ).
cnf(201,plain,
p(enc(pp,pp)),
inference(sor,[status(thm)],[197,4]),
[iquote('0:SoR:197.0,4.0')] ).
cnf(93,plain,
( ~ p(enc(tmk,u))
| ~ p(v)
| p(enc(u,enc(i(tmk),v))) ),
inference(spr,[status(thm),theory(equality)],[12,19]),
[iquote('0:SpR:12.0,19.2')] ).
cnf(197,plain,
( ~ p(enc(tmk,u))
| p(enc(u,pp)) ),
inference(spr,[status(thm),theory(equality)],[12,189]),
[iquote('0:SpR:12.0,189.1')] ).
cnf(189,plain,
( ~ p(u)
| p(enc(enc(i(tmk),u),pp)) ),
inference(sor,[status(thm)],[91,4]),
[iquote('0:SoR:91.1,4.0')] ).
cnf(192,plain,
( ~ p(enc(tc,u))
| p(enc(pp,u)) ),
inference(spr,[status(thm),theory(equality)],[12,181]),
[iquote('0:SpR:12.0,181.1')] ).
cnf(181,plain,
( ~ p(u)
| p(enc(pp,enc(i(tc),u))) ),
inference(sor,[status(thm)],[84,4]),
[iquote('0:SoR:84.0,4.0')] ).
cnf(91,plain,
( ~ p(u)
| ~ p(enc(tmk,v))
| p(enc(enc(i(tmk),u),v)) ),
inference(spr,[status(thm),theory(equality)],[12,19]),
[iquote('0:SpR:12.0,19.2')] ).
cnf(174,plain,
( ~ p(lp)
| ~ p(u)
| p(enc(w__dfg,u)) ),
inference(sor,[status(thm)],[173,15]),
[iquote('0:SoR:173.0,15.2')] ).
cnf(184,plain,
p(enc(pp,k)),
inference(sor,[status(thm)],[178,4]),
[iquote('0:SoR:178.0,4.0')] ).
cnf(178,plain,
( ~ p(enc(tmk,u))
| p(enc(u,k)) ),
inference(spr,[status(thm),theory(equality)],[12,170]),
[iquote('0:SpR:12.0,170.1')] ).
cnf(84,plain,
( ~ p(enc(tmk,u))
| ~ p(v)
| p(enc(u,enc(i(tc),v))) ),
inference(spr,[status(thm),theory(equality)],[12,20]),
[iquote('0:SpR:12.0,20.2')] ).
cnf(170,plain,
( ~ p(u)
| p(enc(enc(i(tmk),u),k)) ),
inference(sor,[status(thm)],[82,8]),
[iquote('0:SoR:82.1,8.0')] ).
cnf(167,plain,
( ~ p(lp)
| ~ p(u)
| p(enc(pp,u)) ),
inference(sor,[status(thm)],[166,15]),
[iquote('0:SoR:166.0,15.2')] ).
cnf(173,plain,
( ~ p(enc(lp,u))
| p(enc(w__dfg,u)) ),
inference(spr,[status(thm),theory(equality)],[12,157]),
[iquote('0:SpR:12.0,157.1')] ).
cnf(157,plain,
( ~ p(u)
| p(enc(w__dfg,enc(i(lp),u))) ),
inference(sor,[status(thm)],[77,5]),
[iquote('0:SoR:77.0,5.0')] ).
cnf(82,plain,
( ~ p(u)
| ~ p(enc(tc,v))
| p(enc(enc(i(tmk),u),v)) ),
inference(spr,[status(thm),theory(equality)],[12,20]),
[iquote('0:SpR:12.0,20.2')] ).
cnf(166,plain,
( ~ p(enc(lp,u))
| p(enc(pp,u)) ),
inference(spr,[status(thm),theory(equality)],[12,155]),
[iquote('0:SpR:12.0,155.1')] ).
cnf(155,plain,
( ~ p(u)
| p(enc(pp,enc(i(lp),u))) ),
inference(sor,[status(thm)],[77,44]),
[iquote('0:SoR:77.0,44.0')] ).
cnf(160,plain,
( ~ p(enc(tmk,u))
| p(enc(u,t2)) ),
inference(spr,[status(thm),theory(equality)],[12,140]),
[iquote('0:SpR:12.0,140.1')] ).
cnf(140,plain,
( ~ p(u)
| p(enc(enc(i(tmk),u),t2)) ),
inference(sor,[status(thm)],[137,14]),
[iquote('0:SoR:137.0,14.1')] ).
cnf(77,plain,
( ~ p(enc(wk,u))
| ~ p(v)
| p(enc(u,enc(i(lp),v))) ),
inference(spr,[status(thm),theory(equality)],[12,21]),
[iquote('0:SpR:12.0,21.2')] ).
cnf(141,plain,
p(enc(w__dfg,t2)),
inference(sor,[status(thm)],[137,5]),
[iquote('0:SoR:137.0,5.0')] ).
cnf(23,axiom,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| p(enc(enc(i(wk),u),enc(i(enc(i(wk),v)),w))) ),
file('SWV238+1.p',unknown),
[] ).
cnf(139,plain,
p(enc(pp,t2)),
inference(sor,[status(thm)],[137,44]),
[iquote('0:SoR:137.0,44.0')] ).
cnf(137,plain,
( ~ p(enc(wk,u))
| p(enc(u,t2)) ),
inference(spr,[status(thm),theory(equality)],[12,134]),
[iquote('0:SpR:12.0,134.1')] ).
cnf(134,plain,
( ~ p(u)
| p(enc(enc(i(wk),u),t2)) ),
inference(sor,[status(thm)],[75,7]),
[iquote('0:SoR:75.1,7.0')] ).
cnf(75,plain,
( ~ p(u)
| ~ p(enc(lp,v))
| p(enc(enc(i(wk),u),v)) ),
inference(spr,[status(thm),theory(equality)],[12,21]),
[iquote('0:SpR:12.0,21.2')] ).
cnf(24,axiom,
( ~ p(u)
| ~ p(v)
| ~ p(w)
| p(enc(enc(i(wk),u),enc(i(enc(i(tmk),v)),w))) ),
file('SWV238+1.p',unknown),
[] ).
cnf(69,plain,
( ~ p(enc(i(i(enc(i(tc),u))),v))
| ~ p(u)
| p(v) ),
inference(spr,[status(thm),theory(equality)],[13,17]),
[iquote('0:SpR:13.0,17.2')] ).
cnf(67,plain,
( ~ p(u)
| ~ p(enc(i(i(tc)),v))
| p(enc(i(v),u)) ),
inference(spr,[status(thm),theory(equality)],[13,17]),
[iquote('0:SpR:13.0,17.2')] ).
cnf(97,plain,
( ~ p(u)
| ~ p(tc)
| ~ p(v)
| p(enc(i(v),u)) ),
inference(sor,[status(thm)],[68,15]),
[iquote('0:SoR:68.1,15.2')] ).
cnf(51,plain,
( ~ p(enc(i(enc(i(tc),u)),v))
| ~ p(u)
| p(v) ),
inference(spr,[status(thm),theory(equality)],[13,16]),
[iquote('0:SpR:13.0,16.2')] ).
cnf(22,axiom,
( ~ p(u)
| ~ p(v)
| p(enc(i(enc(i(zcmk),u)),enc(i(tmk),v))) ),
file('SWV238+1.p',unknown),
[] ).
cnf(49,plain,
( ~ p(u)
| ~ p(enc(i(i(tc)),v))
| p(enc(v,u)) ),
inference(spr,[status(thm),theory(equality)],[13,16]),
[iquote('0:SpR:13.0,16.2')] ).
cnf(70,plain,
( ~ p(enc(enc(i(tc),u),v))
| ~ p(u)
| p(v) ),
inference(spr,[status(thm),theory(equality)],[12,17]),
[iquote('0:SpR:12.0,17.2')] ).
cnf(102,plain,
( ~ p(enc(i(i(k)),u))
| p(u) ),
inference(spr,[status(thm),theory(equality)],[13,98]),
[iquote('0:SpR:13.0,98.1')] ).
cnf(103,plain,
( ~ p(enc(k,u))
| p(u) ),
inference(spr,[status(thm),theory(equality)],[12,98]),
[iquote('0:SpR:12.0,98.1')] ).
cnf(18,axiom,
( ~ p(u)
| ~ p(v)
| p(enc(tmk,enc(i(enc(i(zcmk),u)),v))) ),
file('SWV238+1.p',unknown),
[] ).
cnf(98,plain,
( ~ p(u)
| p(enc(i(k),u)) ),
inference(sor,[status(thm)],[68,8]),
[iquote('0:SoR:68.1,8.0')] ).
cnf(68,plain,
( ~ p(u)
| ~ p(enc(tc,v))
| p(enc(i(v),u)) ),
inference(spr,[status(thm),theory(equality)],[12,17]),
[iquote('0:SpR:12.0,17.2')] ).
cnf(95,plain,
( ~ p(enc(i(k),u))
| p(u) ),
inference(spr,[status(thm),theory(equality)],[13,88]),
[iquote('0:SpR:13.0,88.1')] ).
cnf(88,plain,
( ~ p(u)
| p(enc(k,u)) ),
inference(sor,[status(thm)],[50,8]),
[iquote('0:SoR:50.1,8.0')] ).
cnf(19,axiom,
( ~ p(u)
| ~ p(v)
| p(enc(enc(i(tmk),u),enc(i(tmk),v))) ),
file('SWV238+1.p',unknown),
[] ).
cnf(50,plain,
( ~ p(u)
| ~ p(enc(tc,v))
| p(enc(v,u)) ),
inference(spr,[status(thm),theory(equality)],[12,16]),
[iquote('0:SpR:12.0,16.2')] ).
cnf(85,plain,
( ~ p(tc)
| p(k) ),
inference(sor,[status(thm)],[62,11]),
[iquote('0:SoR:62.0,11.1')] ).
cnf(62,plain,
( ~ p(i(tc))
| p(k) ),
inference(sor,[status(thm)],[47,8]),
[iquote('0:SoR:47.0,8.0')] ).
cnf(20,axiom,
( ~ p(u)
| ~ p(v)
| p(enc(enc(i(tmk),u),enc(i(tc),v))) ),
file('SWV238+1.p',unknown),
[] ).
cnf(79,plain,
( ~ p(lp)
| p(t2) ),
inference(sor,[status(thm)],[61,11]),
[iquote('0:SoR:61.0,11.1')] ).
cnf(61,plain,
( ~ p(i(lp))
| p(t2) ),
inference(sor,[status(thm)],[47,7]),
[iquote('0:SoR:47.0,7.0')] ).
cnf(21,axiom,
( ~ p(u)
| ~ p(v)
| p(enc(enc(i(wk),u),enc(i(lp),v))) ),
file('SWV238+1.p',unknown),
[] ).
cnf(72,plain,
~ p(wk),
inference(sor,[status(thm)],[64,11]),
[iquote('0:SoR:64.0,11.1')] ).
cnf(64,plain,
~ p(i(wk)),
inference(mrr,[status(thm)],[57,26]),
[iquote('0:MRR:57.1,26.0')] ).
cnf(71,plain,
~ p(tmk),
inference(sor,[status(thm)],[63,11]),
[iquote('0:SoR:63.0,11.1')] ).
cnf(63,plain,
~ p(i(tmk)),
inference(mrr,[status(thm)],[56,26]),
[iquote('0:MRR:56.1,26.0')] ).
cnf(17,axiom,
( ~ p(u)
| ~ p(v)
| p(enc(i(enc(i(tc),v)),u)) ),
file('SWV238+1.p',unknown),
[] ).
cnf(47,plain,
( ~ p(enc(u,v))
| ~ p(i(u))
| p(v) ),
inference(spr,[status(thm),theory(equality)],[12,15]),
[iquote('0:SpR:12.0,15.2')] ).
cnf(46,plain,
( ~ p(enc(i(u),v))
| ~ p(u)
| p(v) ),
inference(spr,[status(thm),theory(equality)],[13,15]),
[iquote('0:SpR:13.0,15.2')] ).
cnf(42,plain,
( ~ p(enc(i(i(tmk)),u))
| p(enc(wk,u)) ),
inference(spr,[status(thm),theory(equality)],[13,14]),
[iquote('0:SpR:13.0,14.1')] ).
cnf(16,axiom,
( ~ p(u)
| ~ p(v)
| p(enc(enc(i(tc),v),u)) ),
file('SWV238+1.p',unknown),
[] ).
cnf(15,axiom,
( ~ p(u)
| ~ p(v)
| p(enc(v,u)) ),
file('SWV238+1.p',unknown),
[] ).
cnf(44,plain,
p(enc(wk,pp)),
inference(sor,[status(thm)],[43,4]),
[iquote('0:SoR:43.0,4.0')] ).
cnf(43,plain,
( ~ p(enc(tmk,u))
| p(enc(wk,u)) ),
inference(spr,[status(thm),theory(equality)],[12,14]),
[iquote('0:SpR:12.0,14.1')] ).
cnf(14,axiom,
( ~ p(u)
| p(enc(wk,enc(i(tmk),u))) ),
file('SWV238+1.p',unknown),
[] ).
cnf(13,axiom,
equal(enc(u,enc(i(u),v)),v),
file('SWV238+1.p',unknown),
[] ).
cnf(12,axiom,
equal(enc(i(u),enc(u,v)),v),
file('SWV238+1.p',unknown),
[] ).
cnf(29,plain,
( ~ p(i(u))
| p(u) ),
inference(spr,[status(thm),theory(equality)],[10,11]),
[iquote('0:SpR:10.0,11.1')] ).
cnf(11,axiom,
( ~ p(u)
| p(i(u)) ),
file('SWV238+1.p',unknown),
[] ).
cnf(10,axiom,
equal(i(i(u)),u),
file('SWV238+1.p',unknown),
[] ).
cnf(9,axiom,
~ p(enc(pp,a)),
file('SWV238+1.p',unknown),
[] ).
cnf(4,axiom,
p(enc(tmk,pp)),
file('SWV238+1.p',unknown),
[] ).
cnf(5,axiom,
p(enc(wk,w__dfg)),
file('SWV238+1.p',unknown),
[] ).
cnf(6,axiom,
p(enc(w__dfg,t1)),
file('SWV238+1.p',unknown),
[] ).
cnf(7,axiom,
p(enc(lp,t2)),
file('SWV238+1.p',unknown),
[] ).
cnf(8,axiom,
p(enc(tc,k)),
file('SWV238+1.p',unknown),
[] ).
cnf(26,plain,
~ p(pp),
inference(mrr,[status(thm)],[25,2]),
[iquote('0:MRR:25.1,2.0')] ).
cnf(3,axiom,
p(i(kk)),
file('SWV238+1.p',unknown),
[] ).
cnf(1,axiom,
p(kk),
file('SWV238+1.p',unknown),
[] ).
cnf(2,axiom,
p(a),
file('SWV238+1.p',unknown),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SWV238+1 : TPTP v8.1.0. Released v3.2.0.
% 0.14/0.14 % Command : run_spass %d %s
% 0.14/0.35 % Computer : n018.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 600
% 0.14/0.36 % DateTime : Wed Jun 15 23:40:45 EDT 2022
% 0.14/0.36 % CPUTime :
% 0.71/0.91
% 0.71/0.91 SPASS V 3.9
% 0.71/0.91 SPASS beiseite: Completion found.
% 0.71/0.91 % SZS status CounterSatisfiable
% 0.71/0.91 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.71/0.91 SPASS derived 1207 clauses, backtracked 0 clauses, performed 0 splits and kept 524 clauses.
% 0.71/0.91 SPASS allocated 99134 KBytes.
% 0.71/0.91 SPASS spent 0:00:00.54 on the problem.
% 0.71/0.91 0:00:00.04 for the input.
% 0.71/0.91 0:00:00.03 for the FLOTTER CNF translation.
% 0.71/0.91 0:00:00.04 for inferences.
% 0.71/0.91 0:00:00.00 for the backtracking.
% 0.71/0.91 0:00:00.40 for the reduction.
% 0.71/0.91
% 0.71/0.91
% 0.71/0.91 The saturated set of worked-off clauses is :
% 0.71/0.91 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------