%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : KRS008-1 : TPTP v8.1.0. Released v2.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n019.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 : Sun Jul 17 03:30:15 EDT 2022
% Result : Satisfiable 0.52s 0.70s
% Output : Saturation 0.76s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 4653)
% Comments :
%------------------------------------------------------------------------------
cnf(4677,plain,
( ~ r2most(u)
| ~ r(u,v)
| s2least(u6r2(u))
| f(u)
| e(u)
| equalish(u6r4(u),u6r3(u))
| equalish(v,u6r3(u))
| equalish(v,u6r4(u)) ),
inference(obv,[status(thm),theory(equality)],[4653]),
[iquote('0:Obv:4653.5')] ).
cnf(4719,plain,
( ~ r2most(u)
| s2least(u6r2(u))
| f(u)
| e(u)
| equalish(u6r3(u),u6r3(u)) ),
inference(obv,[status(thm),theory(equality)],[4701]),
[iquote('0:Obv:4701.8')] ).
cnf(547,plain,
( ~ r2most(u)
| ~ r(u,v)
| ~ r(u,w)
| s2least(u6r2(u))
| f(u)
| e(u)
| equalish(v,u6r3(u))
| equalish(w,u6r3(u))
| equalish(w,v) ),
inference(obv,[status(thm),theory(equality)],[535]),
[iquote('0:Obv:535.0')] ).
cnf(4544,plain,
( ~ r2most(u)
| ~ r(u,v)
| s2least(u6r1(u))
| f(u)
| e(u)
| equalish(u6r4(u),u6r3(u))
| equalish(v,u6r3(u))
| equalish(v,u6r4(u)) ),
inference(obv,[status(thm),theory(equality)],[4522]),
[iquote('0:Obv:4522.5')] ).
cnf(4586,plain,
( ~ r2most(u)
| s2least(u6r1(u))
| f(u)
| e(u)
| equalish(u6r3(u),u6r3(u)) ),
inference(obv,[status(thm),theory(equality)],[4570]),
[iquote('0:Obv:4570.8')] ).
cnf(517,plain,
( ~ r2most(u)
| ~ r(u,v)
| ~ r(u,w)
| s2least(u6r1(u))
| f(u)
| e(u)
| equalish(v,u6r3(u))
| equalish(w,u6r3(u))
| equalish(w,v) ),
inference(obv,[status(thm),theory(equality)],[505]),
[iquote('0:Obv:505.0')] ).
cnf(4411,plain,
( ~ r2most(u)
| ~ r(u,v)
| f(u)
| e(u)
| s2least(u6r2(u))
| equalish(u6r3(u),u6r4(u))
| equalish(v,u6r4(u))
| equalish(v,u6r3(u)) ),
inference(obv,[status(thm),theory(equality)],[4393]),
[iquote('0:Obv:4393.5')] ).
cnf(4457,plain,
( ~ r2most(u)
| f(u)
| e(u)
| s2least(u6r2(u))
| equalish(u6r4(u),u6r4(u)) ),
inference(obv,[status(thm),theory(equality)],[4433]),
[iquote('0:Obv:4433.8')] ).
cnf(534,plain,
( ~ r2most(u)
| ~ r(u,v)
| ~ r(u,w)
| f(u)
| e(u)
| s2least(u6r2(u))
| equalish(v,u6r4(u))
| equalish(w,u6r4(u))
| equalish(w,v) ),
inference(obv,[status(thm),theory(equality)],[521]),
[iquote('0:Obv:521.0')] ).
cnf(4278,plain,
( ~ r2most(u)
| ~ r(u,v)
| f(u)
| e(u)
| s2least(u6r1(u))
| equalish(u6r3(u),u6r4(u))
| equalish(v,u6r4(u))
| equalish(v,u6r3(u)) ),
inference(obv,[status(thm),theory(equality)],[4262]),
[iquote('0:Obv:4262.5')] ).
cnf(4324,plain,
( ~ r2most(u)
| f(u)
| e(u)
| s2least(u6r1(u))
| equalish(u6r4(u),u6r4(u)) ),
inference(obv,[status(thm),theory(equality)],[4302]),
[iquote('0:Obv:4302.8')] ).
cnf(504,plain,
( ~ r2most(u)
| ~ r(u,v)
| ~ r(u,w)
| f(u)
| e(u)
| s2least(u6r1(u))
| equalish(v,u6r4(u))
| equalish(w,u6r4(u))
| equalish(w,v) ),
inference(obv,[status(thm),theory(equality)],[491]),
[iquote('0:Obv:491.0')] ).
cnf(4235,plain,
( ~ e(u)
| f(u)
| r(u,u6r3(u))
| equalish(u4r1(u),u6r2(u))
| equalish(u6r1(u),u6r2(u))
| equalish(u6r1(u),u4r1(u)) ),
inference(obv,[status(thm),theory(equality)],[4211]),
[iquote('0:Obv:4211.2')] ).
cnf(4224,plain,
( ~ e(u)
| f(u)
| r(u,u6r3(u))
| equalish(u4r1(u),u6r2(u))
| equalish(u4r2(u),u6r2(u))
| equalish(u4r2(u),u4r1(u)) ),
inference(obv,[status(thm),theory(equality)],[4206]),
[iquote('0:Obv:4206.0')] ).
cnf(4193,plain,
( ~ e(u)
| f(u)
| r(u,u6r3(u))
| equalish(u4r2(u),u6r2(u))
| equalish(u6r1(u),u6r2(u))
| equalish(u6r1(u),u4r2(u)) ),
inference(obv,[status(thm),theory(equality)],[4169]),
[iquote('0:Obv:4169.2')] ).
cnf(4183,plain,
( ~ e(u)
| f(u)
| r(u,u6r3(u))
| equalish(u4r2(u),u6r2(u))
| equalish(u4r1(u),u6r2(u))
| equalish(u4r1(u),u4r2(u)) ),
inference(obv,[status(thm),theory(equality)],[4163]),
[iquote('0:Obv:4163.0')] ).
cnf(1536,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| r(u,u6r3(u))
| equalish(u4r1(u),u6r2(u))
| equalish(v,u6r2(u))
| equalish(v,u4r1(u)) ),
inference(ssi,[status(thm)],[1516,17]),
[iquote('0:SSi:1516.1,17.1')] ).
cnf(1535,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| r(u,u6r3(u))
| equalish(u4r2(u),u6r2(u))
| equalish(v,u6r2(u))
| equalish(v,u4r2(u)) ),
inference(ssi,[status(thm)],[1517,17]),
[iquote('0:SSi:1517.1,17.1')] ).
cnf(4150,plain,
( ~ e(u)
| f(u)
| r(u,u6r4(u))
| equalish(u4r1(u),u6r2(u))
| equalish(u6r1(u),u6r2(u))
| equalish(u6r1(u),u4r1(u)) ),
inference(obv,[status(thm),theory(equality)],[4128]),
[iquote('0:Obv:4128.2')] ).
cnf(4140,plain,
( ~ e(u)
| f(u)
| r(u,u6r4(u))
| equalish(u4r1(u),u6r2(u))
| equalish(u4r2(u),u6r2(u))
| equalish(u4r2(u),u4r1(u)) ),
inference(obv,[status(thm),theory(equality)],[4122]),
[iquote('0:Obv:4122.0')] ).
cnf(4108,plain,
( ~ e(u)
| f(u)
| r(u,u6r4(u))
| equalish(u4r2(u),u6r2(u))
| equalish(u6r1(u),u6r2(u))
| equalish(u6r1(u),u4r2(u)) ),
inference(obv,[status(thm),theory(equality)],[4086]),
[iquote('0:Obv:4086.2')] ).
cnf(1481,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| r(u,u6r4(u))
| equalish(u4r1(u),u6r2(u))
| equalish(v,u6r2(u))
| equalish(v,u4r1(u)) ),
inference(ssi,[status(thm)],[1461,17]),
[iquote('0:SSi:1461.1,17.1')] ).
cnf(4099,plain,
( ~ e(u)
| f(u)
| r(u,u6r4(u))
| equalish(u4r2(u),u6r2(u))
| equalish(u4r1(u),u6r2(u))
| equalish(u4r1(u),u4r2(u)) ),
inference(obv,[status(thm),theory(equality)],[4079]),
[iquote('0:Obv:4079.0')] ).
cnf(1480,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| r(u,u6r4(u))
| equalish(u4r2(u),u6r2(u))
| equalish(v,u6r2(u))
| equalish(v,u4r2(u)) ),
inference(ssi,[status(thm)],[1462,17]),
[iquote('0:SSi:1462.1,17.1')] ).
cnf(4055,plain,
( ~ e(u)
| f(u)
| r(u,u6r3(u))
| equalish(u4r1(u),u6r1(u))
| equalish(u4r2(u),u6r1(u))
| equalish(u4r2(u),u4r1(u)) ),
inference(obv,[status(thm),theory(equality)],[4037]),
[iquote('0:Obv:4037.0')] ).
cnf(4069,plain,
( ~ e(u)
| f(u)
| r(u,u6r3(u))
| equalish(u4r1(u),u6r1(u))
| equalish(u6r2(u),u4r1(u)) ),
inference(mrr,[status(thm)],[4068,31]),
[iquote('0:MRR:4068.4,31.0')] ).
cnf(1423,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| r(u,u6r3(u))
| equalish(u4r1(u),u6r1(u))
| equalish(v,u6r1(u))
| equalish(v,u4r1(u)) ),
inference(ssi,[status(thm)],[1403,17]),
[iquote('0:SSi:1403.1,17.1')] ).
cnf(4013,plain,
( ~ e(u)
| f(u)
| r(u,u6r3(u))
| equalish(u4r2(u),u6r1(u))
| equalish(u4r1(u),u6r1(u))
| equalish(u4r1(u),u4r2(u)) ),
inference(obv,[status(thm),theory(equality)],[3993]),
[iquote('0:Obv:3993.0')] ).
cnf(3969,plain,
( ~ e(u)
| f(u)
| r(u,u6r4(u))
| equalish(u4r1(u),u6r1(u))
| equalish(u4r2(u),u6r1(u))
| equalish(u4r2(u),u4r1(u)) ),
inference(obv,[status(thm),theory(equality)],[3951]),
[iquote('0:Obv:3951.0')] ).
cnf(4026,plain,
( ~ e(u)
| f(u)
| r(u,u6r3(u))
| equalish(u4r2(u),u6r1(u))
| equalish(u6r2(u),u4r2(u)) ),
inference(mrr,[status(thm)],[4025,31]),
[iquote('0:MRR:4025.4,31.0')] ).
cnf(3982,plain,
( ~ e(u)
| f(u)
| r(u,u6r4(u))
| equalish(u4r1(u),u6r1(u))
| equalish(u6r2(u),u4r1(u)) ),
inference(mrr,[status(thm)],[3981,32]),
[iquote('0:MRR:3981.4,32.0')] ).
cnf(1422,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| r(u,u6r3(u))
| equalish(u4r2(u),u6r1(u))
| equalish(v,u6r1(u))
| equalish(v,u4r2(u)) ),
inference(ssi,[status(thm)],[1404,17]),
[iquote('0:SSi:1404.1,17.1')] ).
cnf(1365,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| r(u,u6r4(u))
| equalish(u4r1(u),u6r1(u))
| equalish(v,u6r1(u))
| equalish(v,u4r1(u)) ),
inference(ssi,[status(thm)],[1345,17]),
[iquote('0:SSi:1345.1,17.1')] ).
cnf(3927,plain,
( ~ e(u)
| f(u)
| r(u,u6r4(u))
| equalish(u4r2(u),u6r1(u))
| equalish(u4r1(u),u6r1(u))
| equalish(u4r1(u),u4r2(u)) ),
inference(obv,[status(thm),theory(equality)],[3907]),
[iquote('0:Obv:3907.0')] ).
cnf(3884,plain,
( ~ e(u)
| f(u)
| r(u,u6r3(u))
| equalish(u6r2(u),u4r1(u))
| equalish(u4r2(u),u4r1(u))
| equalish(u4r2(u),u6r2(u)) ),
inference(obv,[status(thm),theory(equality)],[3866]),
[iquote('0:Obv:3866.0')] ).
cnf(3939,plain,
( ~ e(u)
| f(u)
| r(u,u6r4(u))
| equalish(u4r2(u),u6r1(u))
| equalish(u6r2(u),u4r2(u)) ),
inference(mrr,[status(thm)],[3938,32]),
[iquote('0:MRR:3938.4,32.0')] ).
cnf(1364,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| r(u,u6r4(u))
| equalish(u4r2(u),u6r1(u))
| equalish(v,u6r1(u))
| equalish(v,u4r2(u)) ),
inference(ssi,[status(thm)],[1346,17]),
[iquote('0:SSi:1346.1,17.1')] ).
cnf(3897,plain,
( ~ e(u)
| f(u)
| r(u,u6r3(u))
| equalish(u6r2(u),u4r1(u))
| equalish(u6r2(u),u6r2(u)) ),
inference(obv,[status(thm),theory(equality)],[3867]),
[iquote('0:Obv:3867.5')] ).
cnf(678,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| r(u,u6r3(u))
| equalish(u6r2(u),u4r1(u))
| equalish(v,u4r1(u))
| equalish(v,u6r2(u)) ),
inference(res,[status(thm),theory(equality)],[51,313]),
[iquote('0:Res:51.2,313.1')] ).
cnf(3842,plain,
( ~ e(u)
| f(u)
| r(u,u6r4(u))
| equalish(u6r2(u),u4r1(u))
| equalish(u4r2(u),u4r1(u))
| equalish(u4r2(u),u6r2(u)) ),
inference(obv,[status(thm),theory(equality)],[3824]),
[iquote('0:Obv:3824.0')] ).
cnf(3854,plain,
( ~ e(u)
| f(u)
| r(u,u6r4(u))
| equalish(u6r2(u),u4r1(u))
| equalish(u6r2(u),u6r2(u)) ),
inference(obv,[status(thm),theory(equality)],[3826]),
[iquote('0:Obv:3826.5')] ).
cnf(679,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| r(u,u6r4(u))
| equalish(u6r2(u),u4r1(u))
| equalish(v,u4r1(u))
| equalish(v,u6r2(u)) ),
inference(res,[status(thm),theory(equality)],[52,313]),
[iquote('0:Res:52.2,313.1')] ).
cnf(3799,plain,
( ~ e(u)
| f(u)
| r(u,u6r3(u))
| equalish(u6r1(u),u4r1(u))
| equalish(u4r2(u),u4r1(u))
| equalish(u4r2(u),u6r1(u)) ),
inference(obv,[status(thm),theory(equality)],[3781]),
[iquote('0:Obv:3781.0')] ).
cnf(3756,plain,
( ~ e(u)
| f(u)
| r(u,u6r4(u))
| equalish(u6r1(u),u4r1(u))
| equalish(u4r2(u),u4r1(u))
| equalish(u4r2(u),u6r1(u)) ),
inference(obv,[status(thm),theory(equality)],[3738]),
[iquote('0:Obv:3738.0')] ).
cnf(3813,plain,
( ~ e(u)
| f(u)
| r(u,u6r3(u))
| equalish(u6r1(u),u4r1(u))
| equalish(u6r2(u),u4r1(u)) ),
inference(mrr,[status(thm)],[3812,31]),
[iquote('0:MRR:3812.5,31.0')] ).
cnf(3810,plain,
( ~ e(u)
| f(u)
| r(u,u6r3(u))
| equalish(u6r1(u),u4r1(u))
| equalish(u6r1(u),u6r1(u)) ),
inference(obv,[status(thm),theory(equality)],[3786]),
[iquote('0:Obv:3786.5')] ).
cnf(682,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| r(u,u6r3(u))
| equalish(u6r1(u),u4r1(u))
| equalish(v,u4r1(u))
| equalish(v,u6r1(u)) ),
inference(res,[status(thm),theory(equality)],[46,313]),
[iquote('0:Res:46.2,313.1')] ).
cnf(3715,plain,
( ~ e(u)
| f(u)
| r(u,u6r3(u))
| equalish(u6r2(u),u4r2(u))
| equalish(u4r1(u),u4r2(u))
| equalish(u4r1(u),u6r2(u)) ),
inference(obv,[status(thm),theory(equality)],[3695]),
[iquote('0:Obv:3695.0')] ).
cnf(3769,plain,
( ~ e(u)
| f(u)
| r(u,u6r4(u))
| equalish(u6r1(u),u4r1(u))
| equalish(u6r2(u),u4r1(u)) ),
inference(mrr,[status(thm)],[3768,32]),
[iquote('0:MRR:3768.5,32.0')] ).
cnf(3766,plain,
( ~ e(u)
| f(u)
| r(u,u6r4(u))
| equalish(u6r1(u),u4r1(u))
| equalish(u6r1(u),u6r1(u)) ),
inference(obv,[status(thm),theory(equality)],[3744]),
[iquote('0:Obv:3744.5')] ).
cnf(3727,plain,
( ~ e(u)
| f(u)
| r(u,u6r3(u))
| equalish(u6r2(u),u4r2(u))
| equalish(u6r2(u),u6r2(u)) ),
inference(obv,[status(thm),theory(equality)],[3697]),
[iquote('0:Obv:3697.5')] ).
cnf(683,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| r(u,u6r4(u))
| equalish(u6r1(u),u4r1(u))
| equalish(v,u4r1(u))
| equalish(v,u6r1(u)) ),
inference(res,[status(thm),theory(equality)],[47,313]),
[iquote('0:Res:47.2,313.1')] ).
cnf(617,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| r(u,u6r3(u))
| equalish(u6r2(u),u4r2(u))
| equalish(v,u4r2(u))
| equalish(v,u6r2(u)) ),
inference(res,[status(thm),theory(equality)],[51,312]),
[iquote('0:Res:51.2,312.1')] ).
cnf(3673,plain,
( ~ e(u)
| f(u)
| r(u,u6r4(u))
| equalish(u6r2(u),u4r2(u))
| equalish(u4r1(u),u4r2(u))
| equalish(u4r1(u),u6r2(u)) ),
inference(obv,[status(thm),theory(equality)],[3653]),
[iquote('0:Obv:3653.0')] ).
cnf(3630,plain,
( ~ e(u)
| f(u)
| r(u,u6r3(u))
| equalish(u6r1(u),u4r2(u))
| equalish(u4r1(u),u4r2(u))
| equalish(u4r1(u),u6r1(u)) ),
inference(obv,[status(thm),theory(equality)],[3610]),
[iquote('0:Obv:3610.0')] ).
cnf(3684,plain,
( ~ e(u)
| f(u)
| r(u,u6r4(u))
| equalish(u6r2(u),u4r2(u))
| equalish(u6r2(u),u6r2(u)) ),
inference(obv,[status(thm),theory(equality)],[3656]),
[iquote('0:Obv:3656.5')] ).
cnf(618,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| r(u,u6r4(u))
| equalish(u6r2(u),u4r2(u))
| equalish(v,u4r2(u))
| equalish(v,u6r2(u)) ),
inference(res,[status(thm),theory(equality)],[52,312]),
[iquote('0:Res:52.2,312.1')] ).
cnf(3587,plain,
( ~ e(u)
| f(u)
| r(u,u6r4(u))
| equalish(u6r1(u),u4r2(u))
| equalish(u4r1(u),u4r2(u))
| equalish(u4r1(u),u6r1(u)) ),
inference(obv,[status(thm),theory(equality)],[3567]),
[iquote('0:Obv:3567.0')] ).
cnf(3643,plain,
( ~ e(u)
| f(u)
| r(u,u6r3(u))
| equalish(u6r1(u),u4r2(u))
| equalish(u6r2(u),u4r2(u)) ),
inference(mrr,[status(thm)],[3642,31]),
[iquote('0:MRR:3642.5,31.0')] ).
cnf(3640,plain,
( ~ e(u)
| f(u)
| r(u,u6r3(u))
| equalish(u6r1(u),u4r2(u))
| equalish(u6r1(u),u6r1(u)) ),
inference(obv,[status(thm),theory(equality)],[3616]),
[iquote('0:Obv:3616.5')] ).
cnf(3599,plain,
( ~ e(u)
| f(u)
| r(u,u6r4(u))
| equalish(u6r1(u),u4r2(u))
| equalish(u6r2(u),u4r2(u)) ),
inference(mrr,[status(thm)],[3598,32]),
[iquote('0:MRR:3598.5,32.0')] ).
cnf(621,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| r(u,u6r3(u))
| equalish(u6r1(u),u4r2(u))
| equalish(v,u4r2(u))
| equalish(v,u6r1(u)) ),
inference(res,[status(thm),theory(equality)],[46,312]),
[iquote('0:Res:46.2,312.1')] ).
cnf(3596,plain,
( ~ e(u)
| f(u)
| r(u,u6r4(u))
| equalish(u6r1(u),u4r2(u))
| equalish(u6r1(u),u6r1(u)) ),
inference(obv,[status(thm),theory(equality)],[3574]),
[iquote('0:Obv:3574.5')] ).
cnf(622,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| r(u,u6r4(u))
| equalish(u6r1(u),u4r2(u))
| equalish(v,u4r2(u))
| equalish(v,u6r1(u)) ),
inference(res,[status(thm),theory(equality)],[47,312]),
[iquote('0:Res:47.2,312.1')] ).
cnf(3551,plain,
( ~ e(u)
| f(u)
| d(u6r3(u))
| equalish(u4r1(u),u6r2(u))
| equalish(u6r1(u),u6r2(u))
| equalish(u6r1(u),u4r1(u)) ),
inference(obv,[status(thm),theory(equality)],[3533]),
[iquote('0:Obv:3533.2')] ).
cnf(3544,plain,
( ~ e(u)
| f(u)
| d(u6r3(u))
| equalish(u4r1(u),u6r2(u))
| equalish(u4r2(u),u6r2(u))
| equalish(u4r2(u),u4r1(u)) ),
inference(obv,[status(thm),theory(equality)],[3526]),
[iquote('0:Obv:3526.0')] ).
cnf(1309,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| d(u6r3(u))
| equalish(u4r1(u),u6r2(u))
| equalish(v,u6r2(u))
| equalish(v,u4r1(u)) ),
inference(ssi,[status(thm)],[1289,17]),
[iquote('0:SSi:1289.1,17.1')] ).
cnf(3509,plain,
( ~ e(u)
| f(u)
| d(u6r3(u))
| equalish(u4r2(u),u6r2(u))
| equalish(u6r1(u),u6r2(u))
| equalish(u6r1(u),u4r2(u)) ),
inference(obv,[status(thm),theory(equality)],[3491]),
[iquote('0:Obv:3491.2')] ).
cnf(3503,plain,
( ~ e(u)
| f(u)
| d(u6r3(u))
| equalish(u4r2(u),u6r2(u))
| equalish(u4r1(u),u6r2(u))
| equalish(u4r1(u),u4r2(u)) ),
inference(obv,[status(thm),theory(equality)],[3483]),
[iquote('0:Obv:3483.0')] ).
cnf(3466,plain,
( ~ e(u)
| f(u)
| d(u6r4(u))
| equalish(u4r1(u),u6r2(u))
| equalish(u6r1(u),u6r2(u))
| equalish(u6r1(u),u4r1(u)) ),
inference(obv,[status(thm),theory(equality)],[3450]),
[iquote('0:Obv:3450.2')] ).
cnf(3460,plain,
( ~ e(u)
| f(u)
| d(u6r4(u))
| equalish(u4r1(u),u6r2(u))
| equalish(u4r2(u),u6r2(u))
| equalish(u4r2(u),u4r1(u)) ),
inference(obv,[status(thm),theory(equality)],[3442]),
[iquote('0:Obv:3442.0')] ).
cnf(1308,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| d(u6r3(u))
| equalish(u4r2(u),u6r2(u))
| equalish(v,u6r2(u))
| equalish(v,u4r2(u)) ),
inference(ssi,[status(thm)],[1290,17]),
[iquote('0:SSi:1290.1,17.1')] ).
cnf(1258,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| d(u6r4(u))
| equalish(u4r1(u),u6r2(u))
| equalish(v,u6r2(u))
| equalish(v,u4r1(u)) ),
inference(ssi,[status(thm)],[1238,17]),
[iquote('0:SSi:1238.1,17.1')] ).
cnf(3424,plain,
( ~ e(u)
| f(u)
| d(u6r4(u))
| equalish(u4r2(u),u6r2(u))
| equalish(u6r1(u),u6r2(u))
| equalish(u6r1(u),u4r2(u)) ),
inference(obv,[status(thm),theory(equality)],[3408]),
[iquote('0:Obv:3408.2')] ).
cnf(3419,plain,
( ~ e(u)
| f(u)
| d(u6r4(u))
| equalish(u4r2(u),u6r2(u))
| equalish(u4r1(u),u6r2(u))
| equalish(u4r1(u),u4r2(u)) ),
inference(obv,[status(thm),theory(equality)],[3399]),
[iquote('0:Obv:3399.0')] ).
cnf(3375,plain,
( ~ e(u)
| f(u)
| d(u6r3(u))
| equalish(u4r1(u),u6r1(u))
| equalish(u4r2(u),u6r1(u))
| equalish(u4r2(u),u4r1(u)) ),
inference(obv,[status(thm),theory(equality)],[3357]),
[iquote('0:Obv:3357.0')] ).
cnf(1257,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| d(u6r4(u))
| equalish(u4r2(u),u6r2(u))
| equalish(v,u6r2(u))
| equalish(v,u4r2(u)) ),
inference(ssi,[status(thm)],[1239,17]),
[iquote('0:SSi:1239.1,17.1')] ).
cnf(3385,plain,
( ~ e(u)
| f(u)
| d(u6r3(u))
| equalish(u4r1(u),u6r1(u))
| equalish(u6r2(u),u4r1(u)) ),
inference(mrr,[status(thm)],[3384,29]),
[iquote('0:MRR:3384.4,29.0')] ).
cnf(1145,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| d(u6r3(u))
| equalish(u4r1(u),u6r1(u))
| equalish(v,u6r1(u))
| equalish(v,u4r1(u)) ),
inference(ssi,[status(thm)],[1125,17]),
[iquote('0:SSi:1125.1,17.1')] ).
cnf(3333,plain,
( ~ e(u)
| f(u)
| d(u6r3(u))
| equalish(u4r2(u),u6r1(u))
| equalish(u4r1(u),u6r1(u))
| equalish(u4r1(u),u4r2(u)) ),
inference(obv,[status(thm),theory(equality)],[3313]),
[iquote('0:Obv:3313.0')] ).
cnf(3342,plain,
( ~ e(u)
| f(u)
| d(u6r3(u))
| equalish(u4r2(u),u6r1(u))
| equalish(u6r2(u),u4r2(u)) ),
inference(mrr,[status(thm)],[3341,29]),
[iquote('0:MRR:3341.4,29.0')] ).
cnf(1144,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| d(u6r3(u))
| equalish(u4r2(u),u6r1(u))
| equalish(v,u6r1(u))
| equalish(v,u4r2(u)) ),
inference(ssi,[status(thm)],[1126,17]),
[iquote('0:SSi:1126.1,17.1')] ).
cnf(3289,plain,
( ~ e(u)
| f(u)
| d(u6r4(u))
| equalish(u4r1(u),u6r1(u))
| equalish(u4r2(u),u6r1(u))
| equalish(u4r2(u),u4r1(u)) ),
inference(obv,[status(thm),theory(equality)],[3271]),
[iquote('0:Obv:3271.0')] ).
cnf(3247,plain,
( ~ e(u)
| f(u)
| d(u6r4(u))
| equalish(u4r2(u),u6r1(u))
| equalish(u4r1(u),u6r1(u))
| equalish(u4r1(u),u4r2(u)) ),
inference(obv,[status(thm),theory(equality)],[3227]),
[iquote('0:Obv:3227.0')] ).
cnf(3298,plain,
( ~ e(u)
| f(u)
| d(u6r4(u))
| equalish(u4r1(u),u6r1(u))
| equalish(u6r2(u),u4r1(u)) ),
inference(mrr,[status(thm)],[3297,30]),
[iquote('0:MRR:3297.4,30.0')] ).
cnf(3255,plain,
( ~ e(u)
| f(u)
| d(u6r4(u))
| equalish(u4r2(u),u6r1(u))
| equalish(u6r2(u),u4r2(u)) ),
inference(mrr,[status(thm)],[3254,30]),
[iquote('0:MRR:3254.4,30.0')] ).
cnf(1087,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| d(u6r4(u))
| equalish(u4r1(u),u6r1(u))
| equalish(v,u6r1(u))
| equalish(v,u4r1(u)) ),
inference(ssi,[status(thm)],[1067,17]),
[iquote('0:SSi:1067.1,17.1')] ).
cnf(1086,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| d(u6r4(u))
| equalish(u4r2(u),u6r1(u))
| equalish(v,u6r1(u))
| equalish(v,u4r2(u)) ),
inference(ssi,[status(thm)],[1068,17]),
[iquote('0:SSi:1068.1,17.1')] ).
cnf(3207,plain,
( ~ e(u)
| f(u)
| c(u6r1(u))
| equalish(u4r1(u),u6r4(u))
| equalish(u6r3(u),u6r4(u))
| equalish(u6r3(u),u4r1(u)) ),
inference(obv,[status(thm),theory(equality)],[3201]),
[iquote('0:Obv:3201.2')] ).
cnf(3204,plain,
( ~ e(u)
| f(u)
| c(u6r1(u))
| equalish(u4r1(u),u6r4(u))
| equalish(u4r2(u),u6r4(u))
| equalish(u4r2(u),u4r1(u)) ),
inference(obv,[status(thm),theory(equality)],[3186]),
[iquote('0:Obv:3186.0')] ).
cnf(3165,plain,
( ~ e(u)
| f(u)
| c(u6r1(u))
| equalish(u4r2(u),u6r4(u))
| equalish(u6r3(u),u6r4(u))
| equalish(u6r3(u),u4r2(u)) ),
inference(obv,[status(thm),theory(equality)],[3159]),
[iquote('0:Obv:3159.2')] ).
cnf(976,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| c(u6r1(u))
| equalish(u4r1(u),u6r4(u))
| equalish(v,u6r4(u))
| equalish(v,u4r1(u)) ),
inference(ssi,[status(thm)],[956,17]),
[iquote('0:SSi:956.1,17.1')] ).
cnf(3163,plain,
( ~ e(u)
| f(u)
| c(u6r1(u))
| equalish(u4r2(u),u6r4(u))
| equalish(u4r1(u),u6r4(u))
| equalish(u4r1(u),u4r2(u)) ),
inference(obv,[status(thm),theory(equality)],[3143]),
[iquote('0:Obv:3143.0')] ).
cnf(975,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| c(u6r1(u))
| equalish(u4r2(u),u6r4(u))
| equalish(v,u6r4(u))
| equalish(v,u4r2(u)) ),
inference(ssi,[status(thm)],[957,17]),
[iquote('0:SSi:957.1,17.1')] ).
cnf(3122,plain,
( ~ e(u)
| f(u)
| c(u6r2(u))
| equalish(u4r1(u),u6r4(u))
| equalish(u6r3(u),u6r4(u))
| equalish(u6r3(u),u4r1(u)) ),
inference(obv,[status(thm),theory(equality)],[3118]),
[iquote('0:Obv:3118.2')] ).
cnf(3120,plain,
( ~ e(u)
| f(u)
| c(u6r2(u))
| equalish(u4r1(u),u6r4(u))
| equalish(u4r2(u),u6r4(u))
| equalish(u4r2(u),u4r1(u)) ),
inference(obv,[status(thm),theory(equality)],[3102]),
[iquote('0:Obv:3102.0')] ).
cnf(926,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| c(u6r2(u))
| equalish(u4r1(u),u6r4(u))
| equalish(v,u6r4(u))
| equalish(v,u4r1(u)) ),
inference(ssi,[status(thm)],[906,17]),
[iquote('0:SSi:906.1,17.1')] ).
cnf(3080,plain,
( ~ e(u)
| f(u)
| c(u6r2(u))
| equalish(u4r2(u),u6r4(u))
| equalish(u6r3(u),u6r4(u))
| equalish(u6r3(u),u4r2(u)) ),
inference(obv,[status(thm),theory(equality)],[3076]),
[iquote('0:Obv:3076.2')] ).
cnf(3079,plain,
( ~ e(u)
| f(u)
| c(u6r2(u))
| equalish(u4r2(u),u6r4(u))
| equalish(u4r1(u),u6r4(u))
| equalish(u4r1(u),u4r2(u)) ),
inference(obv,[status(thm),theory(equality)],[3059]),
[iquote('0:Obv:3059.0')] ).
cnf(3035,plain,
( ~ e(u)
| f(u)
| c(u6r1(u))
| equalish(u4r1(u),u6r3(u))
| equalish(u4r2(u),u6r3(u))
| equalish(u4r2(u),u4r1(u)) ),
inference(obv,[status(thm),theory(equality)],[3017]),
[iquote('0:Obv:3017.0')] ).
cnf(3041,plain,
( ~ e(u)
| f(u)
| c(u6r1(u))
| equalish(u4r1(u),u6r3(u))
| equalish(u6r4(u),u4r1(u)) ),
inference(mrr,[status(thm)],[3040,33]),
[iquote('0:MRR:3040.4,33.0')] ).
cnf(925,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| c(u6r2(u))
| equalish(u4r2(u),u6r4(u))
| equalish(v,u6r4(u))
| equalish(v,u4r2(u)) ),
inference(ssi,[status(thm)],[907,17]),
[iquote('0:SSi:907.1,17.1')] ).
cnf(859,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| c(u6r1(u))
| equalish(u4r1(u),u6r3(u))
| equalish(v,u6r3(u))
| equalish(v,u4r1(u)) ),
inference(ssi,[status(thm)],[839,17]),
[iquote('0:SSi:839.1,17.1')] ).
cnf(2993,plain,
( ~ e(u)
| f(u)
| c(u6r1(u))
| equalish(u4r2(u),u6r3(u))
| equalish(u4r1(u),u6r3(u))
| equalish(u4r1(u),u4r2(u)) ),
inference(obv,[status(thm),theory(equality)],[2973]),
[iquote('0:Obv:2973.0')] ).
cnf(2949,plain,
( ~ e(u)
| f(u)
| c(u6r2(u))
| equalish(u4r1(u),u6r3(u))
| equalish(u4r2(u),u6r3(u))
| equalish(u4r2(u),u4r1(u)) ),
inference(obv,[status(thm),theory(equality)],[2931]),
[iquote('0:Obv:2931.0')] ).
cnf(2998,plain,
( ~ e(u)
| f(u)
| c(u6r1(u))
| equalish(u4r2(u),u6r3(u))
| equalish(u6r4(u),u4r2(u)) ),
inference(mrr,[status(thm)],[2997,33]),
[iquote('0:MRR:2997.4,33.0')] ).
cnf(858,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| c(u6r1(u))
| equalish(u4r2(u),u6r3(u))
| equalish(v,u6r3(u))
| equalish(v,u4r2(u)) ),
inference(ssi,[status(thm)],[840,17]),
[iquote('0:SSi:840.1,17.1')] ).
cnf(2954,plain,
( ~ e(u)
| f(u)
| c(u6r2(u))
| equalish(u4r1(u),u6r3(u))
| equalish(u6r4(u),u4r1(u)) ),
inference(mrr,[status(thm)],[2953,38]),
[iquote('0:MRR:2953.4,38.0')] ).
cnf(785,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| c(u6r2(u))
| equalish(u4r1(u),u6r3(u))
| equalish(v,u6r3(u))
| equalish(v,u4r1(u)) ),
inference(ssi,[status(thm)],[765,17]),
[iquote('0:SSi:765.1,17.1')] ).
cnf(2907,plain,
( ~ e(u)
| f(u)
| c(u6r2(u))
| equalish(u4r2(u),u6r3(u))
| equalish(u4r1(u),u6r3(u))
| equalish(u4r1(u),u4r2(u)) ),
inference(obv,[status(thm),theory(equality)],[2887]),
[iquote('0:Obv:2887.0')] ).
cnf(2911,plain,
( ~ e(u)
| f(u)
| c(u6r2(u))
| equalish(u4r2(u),u6r3(u))
| equalish(u6r4(u),u4r2(u)) ),
inference(mrr,[status(thm)],[2910,38]),
[iquote('0:MRR:2910.4,38.0')] ).
cnf(784,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| c(u6r2(u))
| equalish(u4r2(u),u6r3(u))
| equalish(v,u6r3(u))
| equalish(v,u4r2(u)) ),
inference(ssi,[status(thm)],[766,17]),
[iquote('0:SSi:766.1,17.1')] ).
cnf(1622,plain,
( ~ e(u)
| f(u)
| r(u,u6r3(u))
| equalish(u4r2(u),u4r1(u))
| equalish(u6r2(u),u4r1(u))
| equalish(u6r2(u),u4r2(u)) ),
inference(res,[status(thm),theory(equality)],[51,695]),
[iquote('0:Res:51.2,695.1')] ).
cnf(1623,plain,
( ~ e(u)
| f(u)
| r(u,u6r4(u))
| equalish(u4r2(u),u4r1(u))
| equalish(u6r2(u),u4r1(u))
| equalish(u6r2(u),u4r2(u)) ),
inference(res,[status(thm),theory(equality)],[52,695]),
[iquote('0:Res:52.2,695.1')] ).
cnf(2864,plain,
( ~ e(u)
| f(u)
| d(u6r3(u))
| equalish(u6r2(u),u4r1(u))
| equalish(u4r2(u),u4r1(u))
| equalish(u4r2(u),u6r2(u)) ),
inference(obv,[status(thm),theory(equality)],[2846]),
[iquote('0:Obv:2846.0')] ).
cnf(2873,plain,
( ~ e(u)
| f(u)
| d(u6r3(u))
| equalish(u6r2(u),u4r1(u))
| equalish(u6r2(u),u6r2(u)) ),
inference(obv,[status(thm),theory(equality)],[2849]),
[iquote('0:Obv:2849.5')] ).
cnf(680,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| d(u6r3(u))
| equalish(u6r2(u),u4r1(u))
| equalish(v,u4r1(u))
| equalish(v,u6r2(u)) ),
inference(res,[status(thm),theory(equality)],[49,313]),
[iquote('0:Res:49.2,313.1')] ).
cnf(1626,plain,
( ~ e(u)
| f(u)
| r(u,u6r3(u))
| equalish(u4r2(u),u4r1(u))
| equalish(u6r1(u),u4r1(u))
| equalish(u6r1(u),u4r2(u)) ),
inference(res,[status(thm),theory(equality)],[46,695]),
[iquote('0:Res:46.2,695.1')] ).
cnf(1627,plain,
( ~ e(u)
| f(u)
| r(u,u6r4(u))
| equalish(u4r2(u),u4r1(u))
| equalish(u6r1(u),u4r1(u))
| equalish(u6r1(u),u4r2(u)) ),
inference(res,[status(thm),theory(equality)],[47,695]),
[iquote('0:Res:47.2,695.1')] ).
cnf(2822,plain,
( ~ e(u)
| f(u)
| d(u6r4(u))
| equalish(u6r2(u),u4r1(u))
| equalish(u4r2(u),u4r1(u))
| equalish(u4r2(u),u6r2(u)) ),
inference(obv,[status(thm),theory(equality)],[2804]),
[iquote('0:Obv:2804.0')] ).
cnf(2830,plain,
( ~ e(u)
| f(u)
| d(u6r4(u))
| equalish(u6r2(u),u4r1(u))
| equalish(u6r2(u),u6r2(u)) ),
inference(obv,[status(thm),theory(equality)],[2808]),
[iquote('0:Obv:2808.5')] ).
cnf(681,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| d(u6r4(u))
| equalish(u6r2(u),u4r1(u))
| equalish(v,u4r1(u))
| equalish(v,u6r2(u)) ),
inference(res,[status(thm),theory(equality)],[50,313]),
[iquote('0:Res:50.2,313.1')] ).
cnf(1584,plain,
( ~ e(u)
| f(u)
| r(u,u6r3(u))
| equalish(u4r1(u),u4r2(u))
| equalish(u6r2(u),u4r2(u))
| equalish(u6r2(u),u4r1(u)) ),
inference(res,[status(thm),theory(equality)],[51,635]),
[iquote('0:Res:51.2,635.1')] ).
cnf(2779,plain,
( ~ e(u)
| f(u)
| d(u6r3(u))
| equalish(u6r1(u),u4r1(u))
| equalish(u4r2(u),u4r1(u))
| equalish(u4r2(u),u6r1(u)) ),
inference(obv,[status(thm),theory(equality)],[2761]),
[iquote('0:Obv:2761.0')] ).
cnf(2789,plain,
( ~ e(u)
| f(u)
| d(u6r3(u))
| equalish(u6r1(u),u4r1(u))
| equalish(u6r2(u),u4r1(u)) ),
inference(mrr,[status(thm)],[2788,29]),
[iquote('0:MRR:2788.5,29.0')] ).
cnf(2786,plain,
( ~ e(u)
| f(u)
| d(u6r3(u))
| equalish(u6r1(u),u4r1(u))
| equalish(u6r1(u),u6r1(u)) ),
inference(obv,[status(thm),theory(equality)],[2768]),
[iquote('0:Obv:2768.5')] ).
cnf(684,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| d(u6r3(u))
| equalish(u6r1(u),u4r1(u))
| equalish(v,u4r1(u))
| equalish(v,u6r1(u)) ),
inference(res,[status(thm),theory(equality)],[44,313]),
[iquote('0:Res:44.2,313.1')] ).
cnf(1585,plain,
( ~ e(u)
| f(u)
| r(u,u6r4(u))
| equalish(u4r1(u),u4r2(u))
| equalish(u6r2(u),u4r2(u))
| equalish(u6r2(u),u4r1(u)) ),
inference(res,[status(thm),theory(equality)],[52,635]),
[iquote('0:Res:52.2,635.1')] ).
cnf(2736,plain,
( ~ e(u)
| f(u)
| d(u6r4(u))
| equalish(u6r1(u),u4r1(u))
| equalish(u4r2(u),u4r1(u))
| equalish(u4r2(u),u6r1(u)) ),
inference(obv,[status(thm),theory(equality)],[2718]),
[iquote('0:Obv:2718.0')] ).
cnf(2745,plain,
( ~ e(u)
| f(u)
| d(u6r4(u))
| equalish(u6r1(u),u4r1(u))
| equalish(u6r2(u),u4r1(u)) ),
inference(mrr,[status(thm)],[2744,30]),
[iquote('0:MRR:2744.5,30.0')] ).
cnf(2742,plain,
( ~ e(u)
| f(u)
| d(u6r4(u))
| equalish(u6r1(u),u4r1(u))
| equalish(u6r1(u),u6r1(u)) ),
inference(obv,[status(thm),theory(equality)],[2726]),
[iquote('0:Obv:2726.5')] ).
cnf(685,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| d(u6r4(u))
| equalish(u6r1(u),u4r1(u))
| equalish(v,u4r1(u))
| equalish(v,u6r1(u)) ),
inference(res,[status(thm),theory(equality)],[45,313]),
[iquote('0:Res:45.2,313.1')] ).
cnf(1588,plain,
( ~ e(u)
| f(u)
| r(u,u6r3(u))
| equalish(u4r1(u),u4r2(u))
| equalish(u6r1(u),u4r2(u))
| equalish(u6r1(u),u4r1(u)) ),
inference(res,[status(thm),theory(equality)],[46,635]),
[iquote('0:Res:46.2,635.1')] ).
cnf(1589,plain,
( ~ e(u)
| f(u)
| r(u,u6r4(u))
| equalish(u4r1(u),u4r2(u))
| equalish(u6r1(u),u4r2(u))
| equalish(u6r1(u),u4r1(u)) ),
inference(res,[status(thm),theory(equality)],[47,635]),
[iquote('0:Res:47.2,635.1')] ).
cnf(2694,plain,
( ~ e(u)
| f(u)
| c(u6r1(u))
| equalish(u6r4(u),u4r1(u))
| equalish(u4r2(u),u4r1(u))
| equalish(u4r2(u),u6r4(u)) ),
inference(obv,[status(thm),theory(equality)],[2676]),
[iquote('0:Obv:2676.0')] ).
cnf(2699,plain,
( ~ e(u)
| f(u)
| c(u6r1(u))
| equalish(u6r4(u),u4r1(u))
| equalish(u6r4(u),u6r4(u)) ),
inference(obv,[status(thm),theory(equality)],[2687]),
[iquote('0:Obv:2687.5')] ).
cnf(688,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| c(u6r1(u))
| equalish(u6r4(u),u4r1(u))
| equalish(v,u4r1(u))
| equalish(v,u6r4(u)) ),
inference(res,[status(thm),theory(equality)],[37,313]),
[iquote('0:Res:37.2,313.1')] ).
cnf(2652,plain,
( ~ e(u)
| f(u)
| c(u6r2(u))
| equalish(u6r4(u),u4r1(u))
| equalish(u4r2(u),u4r1(u))
| equalish(u4r2(u),u6r4(u)) ),
inference(obv,[status(thm),theory(equality)],[2634]),
[iquote('0:Obv:2634.0')] ).
cnf(2609,plain,
( ~ e(u)
| f(u)
| c(u6r1(u))
| equalish(u6r3(u),u4r1(u))
| equalish(u4r2(u),u4r1(u))
| equalish(u4r2(u),u6r3(u)) ),
inference(obv,[status(thm),theory(equality)],[2591]),
[iquote('0:Obv:2591.0')] ).
cnf(2566,plain,
( ~ e(u)
| f(u)
| c(u6r2(u))
| equalish(u6r3(u),u4r1(u))
| equalish(u4r2(u),u4r1(u))
| equalish(u4r2(u),u6r3(u)) ),
inference(obv,[status(thm),theory(equality)],[2548]),
[iquote('0:Obv:2548.0')] ).
cnf(2656,plain,
( ~ e(u)
| f(u)
| c(u6r2(u))
| equalish(u6r4(u),u4r1(u))
| equalish(u6r4(u),u6r4(u)) ),
inference(obv,[status(thm),theory(equality)],[2646]),
[iquote('0:Obv:2646.5')] ).
cnf(689,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| c(u6r2(u))
| equalish(u6r4(u),u4r1(u))
| equalish(v,u4r1(u))
| equalish(v,u6r4(u)) ),
inference(res,[status(thm),theory(equality)],[42,313]),
[iquote('0:Res:42.2,313.1')] ).
cnf(2525,plain,
( ~ e(u)
| f(u)
| d(u6r3(u))
| equalish(u6r2(u),u4r2(u))
| equalish(u4r1(u),u4r2(u))
| equalish(u4r1(u),u6r2(u)) ),
inference(obv,[status(thm),theory(equality)],[2505]),
[iquote('0:Obv:2505.0')] ).
cnf(2483,plain,
( ~ e(u)
| f(u)
| d(u6r4(u))
| equalish(u6r2(u),u4r2(u))
| equalish(u4r1(u),u4r2(u))
| equalish(u4r1(u),u6r2(u)) ),
inference(obv,[status(thm),theory(equality)],[2463]),
[iquote('0:Obv:2463.0')] ).
cnf(2615,plain,
( ~ e(u)
| f(u)
| c(u6r1(u))
| equalish(u6r3(u),u4r1(u))
| equalish(u6r4(u),u4r1(u)) ),
inference(mrr,[status(thm)],[2614,33]),
[iquote('0:MRR:2614.5,33.0')] ).
cnf(2612,plain,
( ~ e(u)
| f(u)
| c(u6r1(u))
| equalish(u6r3(u),u4r1(u))
| equalish(u6r3(u),u6r3(u)) ),
inference(obv,[status(thm),theory(equality)],[2606]),
[iquote('0:Obv:2606.5')] ).
cnf(692,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| c(u6r1(u))
| equalish(u6r3(u),u4r1(u))
| equalish(v,u4r1(u))
| equalish(v,u6r3(u)) ),
inference(res,[status(thm),theory(equality)],[36,313]),
[iquote('0:Res:36.2,313.1')] ).
cnf(2440,plain,
( ~ e(u)
| f(u)
| d(u6r3(u))
| equalish(u6r1(u),u4r2(u))
| equalish(u4r1(u),u4r2(u))
| equalish(u4r1(u),u6r1(u)) ),
inference(obv,[status(thm),theory(equality)],[2420]),
[iquote('0:Obv:2420.0')] ).
cnf(2397,plain,
( ~ e(u)
| f(u)
| d(u6r4(u))
| equalish(u6r1(u),u4r2(u))
| equalish(u4r1(u),u4r2(u))
| equalish(u4r1(u),u6r1(u)) ),
inference(obv,[status(thm),theory(equality)],[2377]),
[iquote('0:Obv:2377.0')] ).
cnf(2571,plain,
( ~ e(u)
| f(u)
| c(u6r2(u))
| equalish(u6r3(u),u4r1(u))
| equalish(u6r4(u),u4r1(u)) ),
inference(mrr,[status(thm)],[2570,38]),
[iquote('0:MRR:2570.5,38.0')] ).
cnf(2568,plain,
( ~ e(u)
| f(u)
| c(u6r2(u))
| equalish(u6r3(u),u4r1(u))
| equalish(u6r3(u),u6r3(u)) ),
inference(obv,[status(thm),theory(equality)],[2564]),
[iquote('0:Obv:2564.5')] ).
cnf(693,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| c(u6r2(u))
| equalish(u6r3(u),u4r1(u))
| equalish(v,u4r1(u))
| equalish(v,u6r3(u)) ),
inference(res,[status(thm),theory(equality)],[41,313]),
[iquote('0:Res:41.2,313.1')] ).
cnf(2355,plain,
( ~ e(u)
| f(u)
| c(u6r1(u))
| equalish(u6r4(u),u4r2(u))
| equalish(u4r1(u),u4r2(u))
| equalish(u4r1(u),u6r4(u)) ),
inference(obv,[status(thm),theory(equality)],[2335]),
[iquote('0:Obv:2335.0')] ).
cnf(2313,plain,
( ~ e(u)
| f(u)
| c(u6r2(u))
| equalish(u6r4(u),u4r2(u))
| equalish(u4r1(u),u4r2(u))
| equalish(u4r1(u),u6r4(u)) ),
inference(obv,[status(thm),theory(equality)],[2293]),
[iquote('0:Obv:2293.0')] ).
cnf(2270,plain,
( ~ e(u)
| f(u)
| c(u6r1(u))
| equalish(u6r3(u),u4r2(u))
| equalish(u4r1(u),u4r2(u))
| equalish(u4r1(u),u6r3(u)) ),
inference(obv,[status(thm),theory(equality)],[2250]),
[iquote('0:Obv:2250.0')] ).
cnf(2533,plain,
( ~ e(u)
| f(u)
| d(u6r3(u))
| equalish(u6r2(u),u4r2(u))
| equalish(u6r2(u),u6r2(u)) ),
inference(obv,[status(thm),theory(equality)],[2509]),
[iquote('0:Obv:2509.5')] ).
cnf(619,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| d(u6r3(u))
| equalish(u6r2(u),u4r2(u))
| equalish(v,u4r2(u))
| equalish(v,u6r2(u)) ),
inference(res,[status(thm),theory(equality)],[49,312]),
[iquote('0:Res:49.2,312.1')] ).
cnf(2227,plain,
( ~ e(u)
| f(u)
| c(u6r2(u))
| equalish(u6r3(u),u4r2(u))
| equalish(u4r1(u),u4r2(u))
| equalish(u4r1(u),u6r3(u)) ),
inference(obv,[status(thm),theory(equality)],[2207]),
[iquote('0:Obv:2207.0')] ).
cnf(1624,plain,
( ~ e(u)
| f(u)
| d(u6r3(u))
| equalish(u4r2(u),u4r1(u))
| equalish(u6r2(u),u4r1(u))
| equalish(u6r2(u),u4r2(u)) ),
inference(res,[status(thm),theory(equality)],[49,695]),
[iquote('0:Res:49.2,695.1')] ).
cnf(1625,plain,
( ~ e(u)
| f(u)
| d(u6r4(u))
| equalish(u4r2(u),u4r1(u))
| equalish(u6r2(u),u4r1(u))
| equalish(u6r2(u),u4r2(u)) ),
inference(res,[status(thm),theory(equality)],[50,695]),
[iquote('0:Res:50.2,695.1')] ).
cnf(2490,plain,
( ~ e(u)
| f(u)
| d(u6r4(u))
| equalish(u6r2(u),u4r2(u))
| equalish(u6r2(u),u6r2(u)) ),
inference(obv,[status(thm),theory(equality)],[2468]),
[iquote('0:Obv:2468.5')] ).
cnf(620,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| d(u6r4(u))
| equalish(u6r2(u),u4r2(u))
| equalish(v,u4r2(u))
| equalish(v,u6r2(u)) ),
inference(res,[status(thm),theory(equality)],[50,312]),
[iquote('0:Res:50.2,312.1')] ).
cnf(1628,plain,
( ~ e(u)
| f(u)
| d(u6r3(u))
| equalish(u4r2(u),u4r1(u))
| equalish(u6r1(u),u4r1(u))
| equalish(u6r1(u),u4r2(u)) ),
inference(res,[status(thm),theory(equality)],[44,695]),
[iquote('0:Res:44.2,695.1')] ).
cnf(1629,plain,
( ~ e(u)
| f(u)
| d(u6r4(u))
| equalish(u4r2(u),u4r1(u))
| equalish(u6r1(u),u4r1(u))
| equalish(u6r1(u),u4r2(u)) ),
inference(res,[status(thm),theory(equality)],[45,695]),
[iquote('0:Res:45.2,695.1')] ).
cnf(2449,plain,
( ~ e(u)
| f(u)
| d(u6r3(u))
| equalish(u6r1(u),u4r2(u))
| equalish(u6r2(u),u4r2(u)) ),
inference(mrr,[status(thm)],[2448,29]),
[iquote('0:MRR:2448.5,29.0')] ).
cnf(2446,plain,
( ~ e(u)
| f(u)
| d(u6r3(u))
| equalish(u6r1(u),u4r2(u))
| equalish(u6r1(u),u6r1(u)) ),
inference(obv,[status(thm),theory(equality)],[2428]),
[iquote('0:Obv:2428.5')] ).
cnf(623,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| d(u6r3(u))
| equalish(u6r1(u),u4r2(u))
| equalish(v,u4r2(u))
| equalish(v,u6r1(u)) ),
inference(res,[status(thm),theory(equality)],[44,312]),
[iquote('0:Res:44.2,312.1')] ).
cnf(1632,plain,
( ~ e(u)
| f(u)
| c(u6r1(u))
| equalish(u4r2(u),u4r1(u))
| equalish(u6r4(u),u4r1(u))
| equalish(u6r4(u),u4r2(u)) ),
inference(res,[status(thm),theory(equality)],[37,695]),
[iquote('0:Res:37.2,695.1')] ).
cnf(1633,plain,
( ~ e(u)
| f(u)
| c(u6r2(u))
| equalish(u4r2(u),u4r1(u))
| equalish(u6r4(u),u4r1(u))
| equalish(u6r4(u),u4r2(u)) ),
inference(res,[status(thm),theory(equality)],[42,695]),
[iquote('0:Res:42.2,695.1')] ).
cnf(2405,plain,
( ~ e(u)
| f(u)
| d(u6r4(u))
| equalish(u6r1(u),u4r2(u))
| equalish(u6r2(u),u4r2(u)) ),
inference(mrr,[status(thm)],[2404,30]),
[iquote('0:MRR:2404.5,30.0')] ).
cnf(2402,plain,
( ~ e(u)
| f(u)
| d(u6r4(u))
| equalish(u6r1(u),u4r2(u))
| equalish(u6r1(u),u6r1(u)) ),
inference(obv,[status(thm),theory(equality)],[2386]),
[iquote('0:Obv:2386.5')] ).
cnf(624,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| d(u6r4(u))
| equalish(u6r1(u),u4r2(u))
| equalish(v,u4r2(u))
| equalish(v,u6r1(u)) ),
inference(res,[status(thm),theory(equality)],[45,312]),
[iquote('0:Res:45.2,312.1')] ).
cnf(1636,plain,
( ~ e(u)
| f(u)
| c(u6r1(u))
| equalish(u4r2(u),u4r1(u))
| equalish(u6r3(u),u4r1(u))
| equalish(u6r3(u),u4r2(u)) ),
inference(res,[status(thm),theory(equality)],[36,695]),
[iquote('0:Res:36.2,695.1')] ).
cnf(1637,plain,
( ~ e(u)
| f(u)
| c(u6r2(u))
| equalish(u4r2(u),u4r1(u))
| equalish(u6r3(u),u4r1(u))
| equalish(u6r3(u),u4r2(u)) ),
inference(res,[status(thm),theory(equality)],[41,695]),
[iquote('0:Res:41.2,695.1')] ).
cnf(1586,plain,
( ~ e(u)
| f(u)
| d(u6r3(u))
| equalish(u4r1(u),u4r2(u))
| equalish(u6r2(u),u4r2(u))
| equalish(u6r2(u),u4r1(u)) ),
inference(res,[status(thm),theory(equality)],[49,635]),
[iquote('0:Res:49.2,635.1')] ).
cnf(2359,plain,
( ~ e(u)
| f(u)
| c(u6r1(u))
| equalish(u6r4(u),u4r2(u))
| equalish(u6r4(u),u6r4(u)) ),
inference(obv,[status(thm),theory(equality)],[2347]),
[iquote('0:Obv:2347.5')] ).
cnf(627,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| c(u6r1(u))
| equalish(u6r4(u),u4r2(u))
| equalish(v,u4r2(u))
| equalish(v,u6r4(u)) ),
inference(res,[status(thm),theory(equality)],[37,312]),
[iquote('0:Res:37.2,312.1')] ).
cnf(1587,plain,
( ~ e(u)
| f(u)
| d(u6r4(u))
| equalish(u4r1(u),u4r2(u))
| equalish(u6r2(u),u4r2(u))
| equalish(u6r2(u),u4r1(u)) ),
inference(res,[status(thm),theory(equality)],[50,635]),
[iquote('0:Res:50.2,635.1')] ).
cnf(1590,plain,
( ~ e(u)
| f(u)
| d(u6r3(u))
| equalish(u4r1(u),u4r2(u))
| equalish(u6r1(u),u4r2(u))
| equalish(u6r1(u),u4r1(u)) ),
inference(res,[status(thm),theory(equality)],[44,635]),
[iquote('0:Res:44.2,635.1')] ).
cnf(1591,plain,
( ~ e(u)
| f(u)
| d(u6r4(u))
| equalish(u4r1(u),u4r2(u))
| equalish(u6r1(u),u4r2(u))
| equalish(u6r1(u),u4r1(u)) ),
inference(res,[status(thm),theory(equality)],[45,635]),
[iquote('0:Res:45.2,635.1')] ).
cnf(2316,plain,
( ~ e(u)
| f(u)
| c(u6r2(u))
| equalish(u6r4(u),u4r2(u))
| equalish(u6r4(u),u6r4(u)) ),
inference(obv,[status(thm),theory(equality)],[2306]),
[iquote('0:Obv:2306.5')] ).
cnf(628,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| c(u6r2(u))
| equalish(u6r4(u),u4r2(u))
| equalish(v,u4r2(u))
| equalish(v,u6r4(u)) ),
inference(res,[status(thm),theory(equality)],[42,312]),
[iquote('0:Res:42.2,312.1')] ).
cnf(1594,plain,
( ~ e(u)
| f(u)
| c(u6r1(u))
| equalish(u4r1(u),u4r2(u))
| equalish(u6r4(u),u4r2(u))
| equalish(u6r4(u),u4r1(u)) ),
inference(res,[status(thm),theory(equality)],[37,635]),
[iquote('0:Res:37.2,635.1')] ).
cnf(1595,plain,
( ~ e(u)
| f(u)
| c(u6r2(u))
| equalish(u4r1(u),u4r2(u))
| equalish(u6r4(u),u4r2(u))
| equalish(u6r4(u),u4r1(u)) ),
inference(res,[status(thm),theory(equality)],[42,635]),
[iquote('0:Res:42.2,635.1')] ).
cnf(2275,plain,
( ~ e(u)
| f(u)
| c(u6r1(u))
| equalish(u6r3(u),u4r2(u))
| equalish(u6r4(u),u4r2(u)) ),
inference(mrr,[status(thm)],[2274,33]),
[iquote('0:MRR:2274.5,33.0')] ).
cnf(2272,plain,
( ~ e(u)
| f(u)
| c(u6r1(u))
| equalish(u6r3(u),u4r2(u))
| equalish(u6r3(u),u6r3(u)) ),
inference(obv,[status(thm),theory(equality)],[2266]),
[iquote('0:Obv:2266.5')] ).
cnf(631,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| c(u6r1(u))
| equalish(u6r3(u),u4r2(u))
| equalish(v,u4r2(u))
| equalish(v,u6r3(u)) ),
inference(res,[status(thm),theory(equality)],[36,312]),
[iquote('0:Res:36.2,312.1')] ).
cnf(1598,plain,
( ~ e(u)
| f(u)
| c(u6r1(u))
| equalish(u4r1(u),u4r2(u))
| equalish(u6r3(u),u4r2(u))
| equalish(u6r3(u),u4r1(u)) ),
inference(res,[status(thm),theory(equality)],[36,635]),
[iquote('0:Res:36.2,635.1')] ).
cnf(1599,plain,
( ~ e(u)
| f(u)
| c(u6r2(u))
| equalish(u4r1(u),u4r2(u))
| equalish(u6r3(u),u4r2(u))
| equalish(u6r3(u),u4r1(u)) ),
inference(res,[status(thm),theory(equality)],[41,635]),
[iquote('0:Res:41.2,635.1')] ).
cnf(2231,plain,
( ~ e(u)
| f(u)
| c(u6r2(u))
| equalish(u6r3(u),u4r2(u))
| equalish(u6r4(u),u4r2(u)) ),
inference(mrr,[status(thm)],[2230,38]),
[iquote('0:MRR:2230.5,38.0')] ).
cnf(2228,plain,
( ~ e(u)
| f(u)
| c(u6r2(u))
| equalish(u6r3(u),u4r2(u))
| equalish(u6r3(u),u6r3(u)) ),
inference(obv,[status(thm),theory(equality)],[2224]),
[iquote('0:Obv:2224.5')] ).
cnf(632,plain,
( ~ e(u)
| ~ r(u,v)
| f(u)
| c(u6r2(u))
| equalish(u6r3(u),u4r2(u))
| equalish(v,u4r2(u))
| equalish(v,u6r3(u)) ),
inference(res,[status(thm),theory(equality)],[41,312]),
[iquote('0:Res:41.2,312.1')] ).
cnf(2181,plain,
( ~ e(u)
| f(u)
| r(u,u6r3(u))
| equalish(u6r1(u),u6r1(u))
| equalish(u4r1(u),u6r1(u)) ),
inference(ssi,[status(thm)],[2161,17]),
[iquote('0:SSi:2161.1,17.1')] ).
cnf(2180,plain,
( ~ e(u)
| f(u)
| r(u,u6r3(u))
| equalish(u6r1(u),u6r1(u))
| equalish(u4r2(u),u6r1(u)) ),
inference(ssi,[status(thm)],[2162,17]),
[iquote('0:SSi:2162.1,17.1')] ).
cnf(2135,plain,
( ~ e(u)
| f(u)
| r(u,u6r4(u))
| equalish(u6r1(u),u6r1(u))
| equalish(u4r1(u),u6r1(u)) ),
inference(ssi,[status(thm)],[2115,17]),
[iquote('0:SSi:2115.1,17.1')] ).
cnf(2191,plain,
( ~ r2most(u)
| f(u)
| r(u,u6r3(u))
| equalish(u6r1(u),u6r1(u)) ),
inference(obv,[status(thm),theory(equality)],[2167]),
[iquote('0:Obv:2167.5')] ).
cnf(2134,plain,
( ~ e(u)
| f(u)
| r(u,u6r4(u))
| equalish(u6r1(u),u6r1(u))
| equalish(u4r2(u),u6r1(u)) ),
inference(ssi,[status(thm)],[2116,17]),
[iquote('0:SSi:2116.1,17.1')] ).
cnf(2088,plain,
( ~ e(u)
| f(u)
| r(u,u6r3(u))
| equalish(u4r1(u),u6r1(u))
| equalish(u4r1(u),u6r2(u)) ),
inference(ssi,[status(thm)],[2069,17]),
[iquote('0:SSi:2069.1,17.1')] ).
cnf(2144,plain,
( ~ r2most(u)
| f(u)
| r(u,u6r4(u))
| equalish(u6r1(u),u6r1(u)) ),
inference(obv,[status(thm),theory(equality)],[2122]),
[iquote('0:Obv:2122.5')] ).
cnf(2087,plain,
( ~ e(u)
| f(u)
| r(u,u6r3(u))
| equalish(u4r2(u),u6r1(u))
| equalish(u4r2(u),u6r2(u)) ),
inference(ssi,[status(thm)],[2070,17]),
[iquote('0:SSi:2070.1,17.1')] ).
cnf(2042,plain,
( ~ e(u)
| f(u)
| r(u,u6r4(u))
| equalish(u4r1(u),u6r1(u))
| equalish(u4r1(u),u6r2(u)) ),
inference(ssi,[status(thm)],[2023,17]),
[iquote('0:SSi:2023.1,17.1')] ).
cnf(2101,plain,
( ~ r2most(u)
| f(u)
| r(u,u6r3(u))
| equalish(u6r2(u),u6r2(u)) ),
inference(mrr,[status(thm)],[2100,31]),
[iquote('0:MRR:2100.3,31.0')] ).
cnf(1436,plain,
( ~ r2most(u)
| ~ r(u,v)
| f(u)
| r(u,u6r3(u))
| equalish(v,u6r1(u))
| equalish(v,u6r2(u)) ),
inference(mrr,[status(thm)],[1435,31]),
[iquote('0:MRR:1435.4,31.0')] ).
cnf(2041,plain,
( ~ e(u)
| f(u)
| r(u,u6r4(u))
| equalish(u4r2(u),u6r1(u))
| equalish(u4r2(u),u6r2(u)) ),
inference(ssi,[status(thm)],[2024,17]),
[iquote('0:SSi:2024.1,17.1')] ).
cnf(1997,plain,
( ~ e(u)
| f(u)
| d(u6r3(u))
| equalish(u6r2(u),u6r2(u))
| equalish(u4r1(u),u6r2(u)) ),
inference(ssi,[status(thm)],[1977,17]),
[iquote('0:SSi:1977.1,17.1')] ).
cnf(1996,plain,
( ~ e(u)
| f(u)
| d(u6r3(u))
| equalish(u6r2(u),u6r2(u))
| equalish(u4r2(u),u6r2(u)) ),
inference(ssi,[status(thm)],[1978,17]),
[iquote('0:SSi:1978.1,17.1')] ).
cnf(2054,plain,
( ~ r2most(u)
| f(u)
| r(u,u6r4(u))
| equalish(u6r2(u),u6r2(u)) ),
inference(mrr,[status(thm)],[2053,32]),
[iquote('0:MRR:2053.3,32.0')] ).
cnf(1377,plain,
( ~ r2most(u)
| ~ r(u,v)
| f(u)
| r(u,u6r4(u))
| equalish(v,u6r1(u))
| equalish(v,u6r2(u)) ),
inference(mrr,[status(thm)],[1376,32]),
[iquote('0:MRR:1376.4,32.0')] ).
cnf(1951,plain,
( ~ e(u)
| f(u)
| d(u6r4(u))
| equalish(u6r2(u),u6r2(u))
| equalish(u4r1(u),u6r2(u)) ),
inference(ssi,[status(thm)],[1931,17]),
[iquote('0:SSi:1931.1,17.1')] ).
cnf(1950,plain,
( ~ e(u)
| f(u)
| d(u6r4(u))
| equalish(u6r2(u),u6r2(u))
| equalish(u4r2(u),u6r2(u)) ),
inference(ssi,[status(thm)],[1932,17]),
[iquote('0:SSi:1932.1,17.1')] ).
cnf(2005,plain,
( ~ r2most(u)
| f(u)
| d(u6r3(u))
| equalish(u6r2(u),u6r2(u)) ),
inference(obv,[status(thm),theory(equality)],[1981]),
[iquote('0:Obv:1981.5')] ).
cnf(1958,plain,
( ~ r2most(u)
| f(u)
| d(u6r4(u))
| equalish(u6r2(u),u6r2(u)) ),
inference(obv,[status(thm),theory(equality)],[1936]),
[iquote('0:Obv:1936.5')] ).
cnf(1905,plain,
( ~ e(u)
| f(u)
| d(u6r3(u))
| equalish(u6r1(u),u6r1(u))
| equalish(u4r1(u),u6r1(u)) ),
inference(ssi,[status(thm)],[1885,17]),
[iquote('0:SSi:1885.1,17.1')] ).
cnf(1904,plain,
( ~ e(u)
| f(u)
| d(u6r3(u))
| equalish(u6r1(u),u6r1(u))
| equalish(u4r2(u),u6r1(u)) ),
inference(ssi,[status(thm)],[1886,17]),
[iquote('0:SSi:1886.1,17.1')] ).
cnf(1911,plain,
( ~ r2most(u)
| f(u)
| d(u6r3(u))
| equalish(u6r1(u),u6r1(u)) ),
inference(obv,[status(thm),theory(equality)],[1893]),
[iquote('0:Obv:1893.5')] ).
cnf(1859,plain,
( ~ e(u)
| f(u)
| d(u6r4(u))
| equalish(u6r1(u),u6r1(u))
| equalish(u4r1(u),u6r1(u)) ),
inference(ssi,[status(thm)],[1839,17]),
[iquote('0:SSi:1839.1,17.1')] ).
cnf(1858,plain,
( ~ e(u)
| f(u)
| d(u6r4(u))
| equalish(u6r1(u),u6r1(u))
| equalish(u4r2(u),u6r1(u)) ),
inference(ssi,[status(thm)],[1840,17]),
[iquote('0:SSi:1840.1,17.1')] ).
cnf(1813,plain,
( ~ e(u)
| f(u)
| c(u6r1(u))
| equalish(u6r4(u),u6r4(u))
| equalish(u4r1(u),u6r4(u)) ),
inference(ssi,[status(thm)],[1793,17]),
[iquote('0:SSi:1793.1,17.1')] ).
cnf(1864,plain,
( ~ r2most(u)
| f(u)
| d(u6r4(u))
| equalish(u6r1(u),u6r1(u)) ),
inference(obv,[status(thm),theory(equality)],[1848]),
[iquote('0:Obv:1848.5')] ).
cnf(1812,plain,
( ~ e(u)
| f(u)
| c(u6r1(u))
| equalish(u6r4(u),u6r4(u))
| equalish(u4r2(u),u6r4(u)) ),
inference(ssi,[status(thm)],[1794,17]),
[iquote('0:SSi:1794.1,17.1')] ).
cnf(1767,plain,
( ~ e(u)
| f(u)
| c(u6r2(u))
| equalish(u6r4(u),u6r4(u))
| equalish(u4r1(u),u6r4(u)) ),
inference(ssi,[status(thm)],[1747,17]),
[iquote('0:SSi:1747.1,17.1')] ).
cnf(1766,plain,
( ~ e(u)
| f(u)
| c(u6r2(u))
| equalish(u6r4(u),u6r4(u))
| equalish(u4r2(u),u6r4(u)) ),
inference(ssi,[status(thm)],[1748,17]),
[iquote('0:SSi:1748.1,17.1')] ).
cnf(1817,plain,
( ~ r2most(u)
| f(u)
| c(u6r1(u))
| equalish(u6r4(u),u6r4(u)) ),
inference(obv,[status(thm),theory(equality)],[1805]),
[iquote('0:Obv:1805.5')] ).
cnf(1721,plain,
( ~ e(u)
| f(u)
| c(u6r1(u))
| equalish(u6r3(u),u6r3(u))
| equalish(u4r1(u),u6r3(u)) ),
inference(ssi,[status(thm)],[1701,17]),
[iquote('0:SSi:1701.1,17.1')] ).
cnf(1720,plain,
( ~ e(u)
| f(u)
| c(u6r1(u))
| equalish(u6r3(u),u6r3(u))
| equalish(u4r2(u),u6r3(u)) ),
inference(ssi,[status(thm)],[1702,17]),
[iquote('0:SSi:1702.1,17.1')] ).
cnf(1770,plain,
( ~ r2most(u)
| f(u)
| c(u6r2(u))
| equalish(u6r4(u),u6r4(u)) ),
inference(obv,[status(thm),theory(equality)],[1760]),
[iquote('0:Obv:1760.5')] ).
cnf(1723,plain,
( ~ r2most(u)
| f(u)
| c(u6r1(u))
| equalish(u6r3(u),u6r3(u)) ),
inference(obv,[status(thm),theory(equality)],[1717]),
[iquote('0:Obv:1717.5')] ).
cnf(1675,plain,
( ~ e(u)
| f(u)
| c(u6r2(u))
| equalish(u6r3(u),u6r3(u))
| equalish(u4r1(u),u6r3(u)) ),
inference(ssi,[status(thm)],[1655,17]),
[iquote('0:SSi:1655.1,17.1')] ).
cnf(1674,plain,
( ~ e(u)
| f(u)
| c(u6r2(u))
| equalish(u6r3(u),u6r3(u))
| equalish(u4r2(u),u6r3(u)) ),
inference(ssi,[status(thm)],[1656,17]),
[iquote('0:SSi:1656.1,17.1')] ).
cnf(1676,plain,
( ~ r2most(u)
| f(u)
| c(u6r2(u))
| equalish(u6r3(u),u6r3(u)) ),
inference(obv,[status(thm),theory(equality)],[1672]),
[iquote('0:Obv:1672.5')] ).
cnf(1154,plain,
( ~ r2most(u)
| ~ r(u,v)
| f(u)
| d(u6r3(u))
| equalish(v,u6r1(u))
| equalish(v,u6r2(u)) ),
inference(mrr,[status(thm)],[1153,29]),
[iquote('0:MRR:1153.4,29.0')] ).
cnf(1095,plain,
( ~ r2most(u)
| ~ r(u,v)
| f(u)
| d(u6r4(u))
| equalish(v,u6r1(u))
| equalish(v,u6r2(u)) ),
inference(mrr,[status(thm)],[1094,30]),
[iquote('0:MRR:1094.4,30.0')] ).
cnf(864,plain,
( ~ r2most(u)
| ~ r(u,v)
| f(u)
| c(u6r1(u))
| equalish(v,u6r3(u))
| equalish(v,u6r4(u)) ),
inference(mrr,[status(thm)],[863,33]),
[iquote('0:MRR:863.4,33.0')] ).
cnf(1645,plain,
equalish(u4r2(exist),u4r1(exist)),
inference(spt,[],[1638]),
[iquote('13:Spt:1638.0')] ).
cnf(789,plain,
( ~ r2most(u)
| ~ r(u,v)
| f(u)
| c(u6r2(u))
| equalish(v,u6r3(u))
| equalish(v,u6r4(u)) ),
inference(mrr,[status(thm)],[788,38]),
[iquote('0:MRR:788.4,38.0')] ).
cnf(695,plain,
( ~ e(u)
| ~ r(u,v)
| equalish(u4r2(u),u4r1(u))
| equalish(v,u4r1(u))
| equalish(v,u4r2(u)) ),
inference(obv,[status(thm),theory(equality)],[677]),
[iquote('0:Obv:677.0')] ).
cnf(1610,plain,
equalish(u4r1(exist),u4r2(exist)),
inference(spt,[],[1600]),
[iquote('12:Spt:1600.0')] ).
cnf(1609,plain,
( ~ f(u)
| r2most(u) ),
inference(mrr,[status(thm)],[1608,1561]),
[iquote('0:MRR:1608.2,1561.1')] ).
cnf(635,plain,
( ~ e(u)
| ~ r(u,v)
| equalish(u4r1(u),u4r2(u))
| equalish(v,u4r2(u))
| equalish(v,u4r1(u)) ),
inference(obv,[status(thm),theory(equality)],[615]),
[iquote('0:Obv:615.0')] ).
cnf(296,plain,
( ~ r2most(u)
| ~ r(u,v)
| ~ r(u,w)
| f(u)
| r(u,u6r3(u))
| equalish(v,u6r2(u))
| equalish(w,u6r2(u))
| equalish(w,v) ),
inference(res,[status(thm),theory(equality)],[51,19]),
[iquote('0:Res:51.2,19.1')] ).
cnf(297,plain,
( ~ r2most(u)
| ~ r(u,v)
| ~ r(u,w)
| f(u)
| r(u,u6r4(u))
| equalish(v,u6r2(u))
| equalish(w,u6r2(u))
| equalish(w,v) ),
inference(res,[status(thm),theory(equality)],[52,19]),
[iquote('0:Res:52.2,19.1')] ).
cnf(300,plain,
( ~ r2most(u)
| ~ r(u,v)
| ~ r(u,w)
| f(u)
| r(u,u6r3(u))
| equalish(v,u6r1(u))
| equalish(w,u6r1(u))
| equalish(w,v) ),
inference(res,[status(thm),theory(equality)],[46,19]),
[iquote('0:Res:46.2,19.1')] ).
cnf(301,plain,
( ~ r2most(u)
| ~ r(u,v)
| ~ r(u,w)
| f(u)
| r(u,u6r4(u))
| equalish(v,u6r1(u))
| equalish(w,u6r1(u))
| equalish(w,v) ),
inference(res,[status(thm),theory(equality)],[47,19]),
[iquote('0:Res:47.2,19.1')] ).
cnf(298,plain,
( ~ r2most(u)
| ~ r(u,v)
| ~ r(u,w)
| f(u)
| d(u6r3(u))
| equalish(v,u6r2(u))
| equalish(w,u6r2(u))
| equalish(w,v) ),
inference(res,[status(thm),theory(equality)],[49,19]),
[iquote('0:Res:49.2,19.1')] ).
cnf(299,plain,
( ~ r2most(u)
| ~ r(u,v)
| ~ r(u,w)
| f(u)
| d(u6r4(u))
| equalish(v,u6r2(u))
| equalish(w,u6r2(u))
| equalish(w,v) ),
inference(res,[status(thm),theory(equality)],[50,19]),
[iquote('0:Res:50.2,19.1')] ).
cnf(830,plain,
( ~ r(exist,u)
| ~ r(exist,v)
| equalish(u,u6r1(exist))
| equalish(v,u6r1(exist))
| equalish(v,u) ),
inference(ssi,[status(thm)],[821,53,59]),
[iquote('7:SSi:821.0,53.0,59.0')] ).
cnf(1196,plain,
( ~ r(exist,u)
| equalish(u,u6r2(exist)) ),
inference(spt,[],[1191]),
[iquote('11:Spt:1191.0,1191.2')] ).
cnf(302,plain,
( ~ r2most(u)
| ~ r(u,v)
| ~ r(u,w)
| f(u)
| d(u6r3(u))
| equalish(v,u6r1(u))
| equalish(w,u6r1(u))
| equalish(w,v) ),
inference(res,[status(thm),theory(equality)],[44,19]),
[iquote('0:Res:44.2,19.1')] ).
cnf(829,plain,
( ~ c(u)
| ~ f(exist)
| ~ r(exist,u)
| equalish(u,u6r1(exist)) ),
inference(ssi,[status(thm)],[824,812]),
[iquote('7:SSi:824.0,812.0')] ).
cnf(60,plain,
( ~ equalish(u6r4(exist),u6r3(exist))
| ~ equalish(u6r2(exist),u6r1(exist)) ),
inference(res,[status(thm),theory(equality)],[28,54]),
[iquote('0:Res:28.2,54.0')] ).
cnf(1115,plain,
equalish(u6r1(exist),u6r1(exist)),
inference(spt,[],[1114,1053]),
[iquote('9:Spt:1114.0,1053.1')] ).
cnf(303,plain,
( ~ r2most(u)
| ~ r(u,v)
| ~ r(u,w)
| f(u)
| d(u6r4(u))
| equalish(v,u6r1(u))
| equalish(w,u6r1(u))
| equalish(w,v) ),
inference(res,[status(thm),theory(equality)],[45,19]),
[iquote('0:Res:45.2,19.1')] ).
cnf(1025,plain,
( ~ r(exist,u)
| equalish(u,u6r4(exist)) ),
inference(spt,[],[1020]),
[iquote('8:Spt:1020.0,1020.2')] ).
cnf(304,plain,
( ~ r2most(u)
| ~ r(u,v)
| ~ r(u,w)
| f(u)
| c(u6r1(u))
| equalish(v,u6r4(u))
| equalish(w,u6r4(u))
| equalish(w,v) ),
inference(res,[status(thm),theory(equality)],[37,19]),
[iquote('0:Res:37.2,19.1')] ).
cnf(895,plain,
~ d(u6r2(exist)),
inference(sor,[status(thm)],[817,7]),
[iquote('7:SoR:817.0,7.1')] ).
cnf(891,plain,
~ d(u6r1(exist)),
inference(sor,[status(thm)],[816,7]),
[iquote('7:SoR:816.0,7.1')] ).
cnf(896,plain,
s2least(u6r2(exist)),
inference(sor,[status(thm)],[817,182]),
[iquote('7:SoR:817.0,182.1')] ).
cnf(305,plain,
( ~ r2most(u)
| ~ r(u,v)
| ~ r(u,w)
| f(u)
| c(u6r2(u))
| equalish(v,u6r4(u))
| equalish(w,u6r4(u))
| equalish(w,v) ),
inference(res,[status(thm),theory(equality)],[42,19]),
[iquote('0:Res:42.2,19.1')] ).
cnf(817,plain,
~ s1most(u6r2(exist)),
inference(ems,[status(thm)],[215,8,813]),
[iquote('7:EmS:215.0,215.1,8.1,813.0')] ).
cnf(892,plain,
s2least(u6r1(exist)),
inference(sor,[status(thm)],[816,182]),
[iquote('7:SoR:816.0,182.1')] ).
cnf(816,plain,
~ s1most(u6r1(exist)),
inference(ems,[status(thm)],[215,8,812]),
[iquote('7:EmS:215.0,215.1,8.1,812.0')] ).
cnf(815,plain,
r(exist,u6r2(exist)),
inference(mrr,[status(thm)],[805,174]),
[iquote('7:MRR:805.0,174.0')] ).
cnf(306,plain,
( ~ r2most(u)
| ~ r(u,v)
| ~ r(u,w)
| f(u)
| c(u6r1(u))
| equalish(v,u6r3(u))
| equalish(w,u6r3(u))
| equalish(w,v) ),
inference(res,[status(thm),theory(equality)],[36,19]),
[iquote('0:Res:36.2,19.1')] ).
cnf(814,plain,
r(exist,u6r1(exist)),
inference(mrr,[status(thm)],[804,174]),
[iquote('7:MRR:804.0,174.0')] ).
cnf(813,plain,
c(u6r2(exist)),
inference(mrr,[status(thm)],[807,174]),
[iquote('7:MRR:807.0,174.0')] ).
cnf(812,plain,
c(u6r1(exist)),
inference(mrr,[status(thm)],[806,174]),
[iquote('7:MRR:806.0,174.0')] ).
cnf(803,plain,
( ~ r(exist,u)
| equalish(u,u6r3(exist)) ),
inference(spt,[],[753]),
[iquote('7:Spt:753.0,753.2')] ).
cnf(307,plain,
( ~ r2most(u)
| ~ r(u,v)
| ~ r(u,w)
| f(u)
| c(u6r2(u))
| equalish(v,u6r3(u))
| equalish(w,u6r3(u))
| equalish(w,v) ),
inference(res,[status(thm),theory(equality)],[41,19]),
[iquote('0:Res:41.2,19.1')] ).
cnf(726,plain,
( ~ e(u)
| equalish(u4r1(u),u4r1(u)) ),
inference(obv,[status(thm),theory(equality)],[704]),
[iquote('0:Obv:704.2')] ).
cnf(725,plain,
equalish(u4r1(exist),u4r1(exist)),
inference(ssi,[status(thm)],[724,53,59]),
[iquote('0:SSi:724.0,53.0,59.0')] ).
cnf(313,plain,
( ~ e(u)
| ~ r(u,v)
| ~ r(u,w)
| equalish(v,u4r1(u))
| equalish(w,u4r1(u))
| equalish(w,v) ),
inference(ssi,[status(thm)],[294,17]),
[iquote('0:SSi:294.1,17.1')] ).
cnf(668,plain,
( ~ e(u)
| equalish(u4r2(u),u4r2(u)) ),
inference(obv,[status(thm),theory(equality)],[645]),
[iquote('0:Obv:645.2')] ).
cnf(666,plain,
equalish(u4r2(exist),u4r2(exist)),
inference(ssi,[status(thm)],[665,53,59]),
[iquote('0:SSi:665.0,53.0,59.0')] ).
cnf(636,plain,
( ~ r(exist,u)
| equalish(u,u4r1(exist)) ),
inference(spt,[],[606]),
[iquote('6:Spt:606.0,606.2')] ).
cnf(312,plain,
( ~ e(u)
| ~ r(u,v)
| ~ r(u,w)
| equalish(v,u4r2(u))
| equalish(w,u4r2(u))
| equalish(w,v) ),
inference(ssi,[status(thm)],[295,17]),
[iquote('0:SSi:295.1,17.1')] ).
cnf(580,plain,
( ~ r(exist,u)
| equalish(u,u4r2(exist)) ),
inference(spt,[],[578]),
[iquote('5:Spt:578.0,578.2')] ).
cnf(488,plain,
( ~ r2most(u)
| ~ s1most(u6r2(u))
| f(u)
| r(u,u6r3(u))
| e(u) ),
inference(sor,[status(thm)],[465,8]),
[iquote('0:SoR:465.0,8.1')] ).
cnf(486,plain,
( ~ r2most(u)
| ~ s1most(u6r1(u))
| f(u)
| r(u,u6r3(u))
| e(u) ),
inference(sor,[status(thm)],[463,8]),
[iquote('0:SoR:463.0,8.1')] ).
cnf(532,plain,
( ~ r2most(u)
| s2least(u6r2(u))
| f(u)
| r(u,u6r3(u))
| e(u) ),
inference(mrr,[status(thm)],[531,429]),
[iquote('0:MRR:531.0,429.2')] ).
cnf(520,plain,
( ~ r2most(u)
| f(u)
| r(u,u6r4(u))
| e(u)
| s2least(u6r2(u)) ),
inference(sor,[status(thm)],[485,182]),
[iquote('0:SoR:485.1,182.1')] ).
cnf(485,plain,
( ~ r2most(u)
| ~ s1most(u6r2(u))
| f(u)
| r(u,u6r4(u))
| e(u) ),
inference(sor,[status(thm)],[425,8]),
[iquote('0:SoR:425.0,8.1')] ).
cnf(502,plain,
( ~ r2most(u)
| s2least(u6r1(u))
| f(u)
| r(u,u6r3(u))
| e(u) ),
inference(mrr,[status(thm)],[501,432]),
[iquote('0:MRR:501.0,432.2')] ).
cnf(490,plain,
( ~ r2most(u)
| f(u)
| r(u,u6r4(u))
| e(u)
| s2least(u6r1(u)) ),
inference(sor,[status(thm)],[484,182]),
[iquote('0:SoR:484.1,182.1')] ).
cnf(484,plain,
( ~ r2most(u)
| ~ s1most(u6r1(u))
| f(u)
| r(u,u6r4(u))
| e(u) ),
inference(sor,[status(thm)],[423,8]),
[iquote('0:SoR:423.0,8.1')] ).
cnf(465,plain,
( ~ d(u6r2(u))
| ~ r2most(u)
| f(u)
| r(u,u6r3(u))
| e(u) ),
inference(obv,[status(thm),theory(equality)],[442]),
[iquote('0:Obv:442.3')] ).
cnf(463,plain,
( ~ d(u6r1(u))
| ~ r2most(u)
| f(u)
| r(u,u6r3(u))
| e(u) ),
inference(obv,[status(thm),theory(equality)],[446]),
[iquote('0:Obv:446.3')] ).
cnf(425,plain,
( ~ d(u6r2(u))
| ~ r2most(u)
| f(u)
| r(u,u6r4(u))
| e(u) ),
inference(obv,[status(thm),theory(equality)],[404]),
[iquote('0:Obv:404.3')] ).
cnf(423,plain,
( ~ d(u6r1(u))
| ~ r2most(u)
| f(u)
| r(u,u6r4(u))
| e(u) ),
inference(obv,[status(thm),theory(equality)],[408]),
[iquote('0:Obv:408.3')] ).
cnf(478,plain,
( ~ r2most(u)
| ~ c(u6r3(u))
| f(u)
| e(u)
| s2least(u6r1(u)) ),
inference(sor,[status(thm)],[473,1]),
[iquote('0:SoR:473.1,1.1')] ).
cnf(476,plain,
( ~ r2most(u)
| ~ c(u6r3(u))
| f(u)
| e(u)
| s2least(u6r2(u)) ),
inference(sor,[status(thm)],[469,1]),
[iquote('0:SoR:469.1,1.1')] ).
cnf(475,plain,
( ~ r2most(u)
| ~ c(u6r4(u))
| f(u)
| e(u)
| s2least(u6r1(u)) ),
inference(sor,[status(thm)],[466,1]),
[iquote('0:SoR:466.1,1.1')] ).
cnf(474,plain,
( ~ r2most(u)
| ~ c(u6r4(u))
| f(u)
| e(u)
| s2least(u6r2(u)) ),
inference(sor,[status(thm)],[430,1]),
[iquote('0:SoR:430.1,1.1')] ).
cnf(473,plain,
( ~ r2most(u)
| ~ s2least(u6r3(u))
| f(u)
| e(u)
| s2least(u6r1(u)) ),
inference(ems,[status(thm)],[215,471,2]),
[iquote('0:EmS:215.0,215.1,471.2,2.1')] ).
cnf(469,plain,
( ~ r2most(u)
| ~ s2least(u6r3(u))
| f(u)
| e(u)
| s2least(u6r2(u)) ),
inference(ems,[status(thm)],[215,468,2]),
[iquote('0:EmS:215.0,215.1,468.2,2.1')] ).
cnf(466,plain,
( ~ r2most(u)
| ~ s2least(u6r4(u))
| f(u)
| e(u)
| s2least(u6r1(u)) ),
inference(ems,[status(thm)],[215,432,2]),
[iquote('0:EmS:215.0,215.1,432.2,2.1')] ).
cnf(430,plain,
( ~ r2most(u)
| ~ s2least(u6r4(u))
| f(u)
| e(u)
| s2least(u6r2(u)) ),
inference(ems,[status(thm)],[215,429,2]),
[iquote('0:EmS:215.0,215.1,429.2,2.1')] ).
cnf(471,plain,
( ~ r2most(u)
| f(u)
| d(u6r3(u))
| e(u)
| s2least(u6r1(u)) ),
inference(sor,[status(thm)],[427,182]),
[iquote('0:SoR:427.1,182.1')] ).
cnf(427,plain,
( ~ r2most(u)
| ~ s1most(u6r1(u))
| f(u)
| d(u6r3(u))
| e(u) ),
inference(sor,[status(thm)],[378,8]),
[iquote('0:SoR:378.0,8.1')] ).
cnf(468,plain,
( ~ r2most(u)
| f(u)
| d(u6r3(u))
| e(u)
| s2least(u6r2(u)) ),
inference(sor,[status(thm)],[393,182]),
[iquote('0:SoR:393.1,182.1')] ).
cnf(393,plain,
( ~ r2most(u)
| ~ s1most(u6r2(u))
| f(u)
| d(u6r3(u))
| e(u) ),
inference(sor,[status(thm)],[376,8]),
[iquote('0:SoR:376.0,8.1')] ).
cnf(432,plain,
( ~ r2most(u)
| f(u)
| d(u6r4(u))
| e(u)
| s2least(u6r1(u)) ),
inference(sor,[status(thm)],[392,182]),
[iquote('0:SoR:392.1,182.1')] ).
cnf(211,plain,
( ~ d(u)
| ~ r2most(v)
| ~ r(v,u)
| f(v)
| r(v,u6r3(v))
| e(v) ),
inference(mrr,[status(thm)],[200,36]),
[iquote('0:MRR:200.1,36.1')] ).
cnf(392,plain,
( ~ r2most(u)
| ~ s1most(u6r1(u))
| f(u)
| d(u6r4(u))
| e(u) ),
inference(sor,[status(thm)],[344,8]),
[iquote('0:SoR:344.0,8.1')] ).
cnf(429,plain,
( ~ r2most(u)
| f(u)
| d(u6r4(u))
| e(u)
| s2least(u6r2(u)) ),
inference(sor,[status(thm)],[391,182]),
[iquote('0:SoR:391.1,182.1')] ).
cnf(391,plain,
( ~ r2most(u)
| ~ s1most(u6r2(u))
| f(u)
| d(u6r4(u))
| e(u) ),
inference(sor,[status(thm)],[342,8]),
[iquote('0:SoR:342.0,8.1')] ).
cnf(378,plain,
( ~ d(u6r1(u))
| ~ r2most(u)
| f(u)
| d(u6r3(u))
| e(u) ),
inference(obv,[status(thm),theory(equality)],[370]),
[iquote('0:Obv:370.3')] ).
cnf(210,plain,
( ~ d(u)
| ~ r2most(v)
| ~ r(v,u)
| f(v)
| r(v,u6r4(v))
| e(v) ),
inference(mrr,[status(thm)],[201,37]),
[iquote('0:MRR:201.1,37.1')] ).
cnf(376,plain,
( ~ d(u6r2(u))
| ~ r2most(u)
| f(u)
| d(u6r3(u))
| e(u) ),
inference(obv,[status(thm),theory(equality)],[366]),
[iquote('0:Obv:366.3')] ).
cnf(344,plain,
( ~ d(u6r1(u))
| ~ r2most(u)
| f(u)
| d(u6r4(u))
| e(u) ),
inference(obv,[status(thm),theory(equality)],[336]),
[iquote('0:Obv:336.3')] ).
cnf(342,plain,
( ~ d(u6r2(u))
| ~ r2most(u)
| f(u)
| d(u6r4(u))
| e(u) ),
inference(obv,[status(thm),theory(equality)],[332]),
[iquote('0:Obv:332.3')] ).
cnf(282,plain,
( ~ e(u)
| ~ d(v)
| ~ f(u)
| ~ r(u,v)
| equalish(v,u4r2(u)) ),
inference(ssi,[status(thm)],[266,13]),
[iquote('0:SSi:266.1,13.1')] ).
cnf(386,plain,
( ~ c(u6r4(u))
| f(u)
| c(u6r1(u)) ),
inference(sor,[status(thm)],[224,1]),
[iquote('0:SoR:224.0,1.1')] ).
cnf(251,plain,
( ~ e(u)
| ~ c(v)
| ~ f(u)
| ~ r(u,v)
| equalish(v,u4r1(u)) ),
inference(ssi,[status(thm)],[236,15]),
[iquote('0:SSi:236.1,15.1')] ).
cnf(354,plain,
( ~ c(u6r4(u))
| f(u)
| c(u6r2(u)) ),
inference(sor,[status(thm)],[223,1]),
[iquote('0:SoR:223.0,1.1')] ).
cnf(353,plain,
( ~ c(u6r3(u))
| f(u)
| c(u6r1(u)) ),
inference(sor,[status(thm)],[221,1]),
[iquote('0:SoR:221.0,1.1')] ).
cnf(352,plain,
( ~ c(u6r3(u))
| f(u)
| c(u6r2(u)) ),
inference(sor,[status(thm)],[220,1]),
[iquote('0:SoR:220.0,1.1')] ).
cnf(224,plain,
( ~ s2least(u6r4(u))
| f(u)
| c(u6r1(u)) ),
inference(ems,[status(thm)],[215,35,2]),
[iquote('0:EmS:215.0,215.1,35.1,2.1')] ).
cnf(209,plain,
( ~ d(u)
| ~ r2most(v)
| ~ r(v,u)
| f(v)
| d(u6r3(v))
| e(v) ),
inference(mrr,[status(thm)],[202,34]),
[iquote('0:MRR:202.1,34.2')] ).
cnf(223,plain,
( ~ s2least(u6r4(u))
| f(u)
| c(u6r2(u)) ),
inference(ems,[status(thm)],[215,40,2]),
[iquote('0:EmS:215.0,215.1,40.1,2.1')] ).
cnf(221,plain,
( ~ s2least(u6r3(u))
| f(u)
| c(u6r1(u)) ),
inference(ems,[status(thm)],[215,34,2]),
[iquote('0:EmS:215.0,215.1,34.1,2.1')] ).
cnf(220,plain,
( ~ s2least(u6r3(u))
| f(u)
| c(u6r2(u)) ),
inference(ems,[status(thm)],[215,39,2]),
[iquote('0:EmS:215.0,215.1,39.1,2.1')] ).
cnf(315,plain,
( ~ e(u)
| ~ d(u4r1(u)) ),
inference(sor,[status(thm)],[226,7]),
[iquote('0:SoR:226.0,7.1')] ).
cnf(208,plain,
( ~ d(u)
| ~ r2most(v)
| ~ r(v,u)
| f(v)
| d(u6r4(v))
| e(v) ),
inference(mrr,[status(thm)],[203,35]),
[iquote('0:MRR:203.1,35.2')] ).
cnf(314,plain,
( ~ e(u)
| ~ c(u4r2(u)) ),
inference(sor,[status(thm)],[217,1]),
[iquote('0:SoR:217.1,1.1')] ).
cnf(316,plain,
( ~ e(u)
| s2least(u4r1(u)) ),
inference(sor,[status(thm)],[226,182]),
[iquote('0:SoR:226.0,182.1')] ).
cnf(226,plain,
( ~ s1most(u4r1(u))
| ~ e(u) ),
inference(ems,[status(thm)],[215,8,15]),
[iquote('0:EmS:215.0,215.1,8.1,15.1')] ).
cnf(217,plain,
( ~ e(u)
| ~ s2least(u4r2(u)) ),
inference(ems,[status(thm)],[215,13,2]),
[iquote('0:EmS:215.0,215.1,13.1,2.1')] ).
cnf(19,axiom,
( ~ r2most(u)
| ~ r(u,v)
| ~ r(u,w)
| ~ r(u,x)
| equalish(w,v)
| equalish(x,v)
| equalish(x,w) ),
file('KRS008-1.p',unknown),
[] ).
cnf(254,plain,
~ d(u4r1(exist)),
inference(sor,[status(thm)],[227,7]),
[iquote('0:SoR:227.0,7.1')] ).
cnf(253,plain,
~ c(u6r4(exist)),
inference(sor,[status(thm)],[225,1]),
[iquote('1:SoR:225.0,1.1')] ).
cnf(252,plain,
~ c(u6r3(exist)),
inference(sor,[status(thm)],[222,1]),
[iquote('2:SoR:222.0,1.1')] ).
cnf(228,plain,
~ c(u4r2(exist)),
inference(sor,[status(thm)],[218,1]),
[iquote('0:SoR:218.0,1.1')] ).
cnf(26,axiom,
( ~ d(u)
| ~ d(v)
| ~ f(w)
| ~ r(w,u)
| ~ r(w,v)
| equalish(v,u) ),
file('KRS008-1.p',unknown),
[] ).
cnf(255,plain,
s2least(u4r1(exist)),
inference(sor,[status(thm)],[227,182]),
[iquote('0:SoR:227.0,182.1')] ).
cnf(227,plain,
~ s1most(u4r1(exist)),
inference(ems,[status(thm)],[215,8,58]),
[iquote('0:EmS:215.0,215.1,8.1,58.0')] ).
cnf(225,plain,
~ s2least(u6r4(exist)),
inference(ems,[status(thm)],[215,172,2]),
[iquote('1:EmS:215.0,215.1,172.0,2.1')] ).
cnf(222,plain,
~ s2least(u6r3(exist)),
inference(ems,[status(thm)],[215,173,2]),
[iquote('2:EmS:215.0,215.1,173.0,2.1')] ).
cnf(27,axiom,
( ~ c(u)
| ~ c(v)
| ~ f(w)
| ~ r(w,u)
| ~ r(w,v)
| equalish(v,u) ),
file('KRS008-1.p',unknown),
[] ).
cnf(218,plain,
~ s2least(u4r2(exist)),
inference(ems,[status(thm)],[215,57,2]),
[iquote('0:EmS:215.0,215.1,57.0,2.1')] ).
cnf(215,plain,
( ~ d(u)
| ~ c(u) ),
inference(ems,[status(thm)],[214,7,1]),
[iquote('0:EmS:214.0,214.1,7.1,1.1')] ).
cnf(214,plain,
( ~ s1most(u)
| ~ s2least(u) ),
inference(mrr,[status(thm)],[213,5]),
[iquote('0:MRR:213.2,5.1')] ).
cnf(18,axiom,
( ~ d(u)
| ~ c(v)
| ~ r2most(w)
| ~ r(w,v)
| ~ r(w,u)
| e(w) ),
file('KRS008-1.p',unknown),
[] ).
cnf(9,axiom,
( ~ s1most(u)
| ~ s(u,v)
| ~ s(u,w)
| equalish(w,v) ),
file('KRS008-1.p',unknown),
[] ).
cnf(182,plain,
( s2least(u)
| s1most(u) ),
inference(mrr,[status(thm)],[181,12]),
[iquote('0:MRR:181.0,12.1')] ).
cnf(28,axiom,
( ~ equalish(u6r4(u),u6r3(u))
| ~ equalish(u6r2(u),u6r1(u))
| f(u) ),
file('KRS008-1.p',unknown),
[] ).
cnf(6,axiom,
( ~ s(u,v)
| ~ s(u,w)
| s2least(u)
| equalish(w,v) ),
file('KRS008-1.p',unknown),
[] ).
cnf(31,axiom,
( ~ equalish(u6r2(u),u6r1(u))
| f(u)
| r(u,u6r3(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(32,axiom,
( ~ equalish(u6r2(u),u6r1(u))
| f(u)
| r(u,u6r4(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(43,axiom,
( ~ equalish(u6r4(u),u6r3(u))
| f(u)
| r(u,u6r1(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(48,axiom,
( ~ equalish(u6r4(u),u6r3(u))
| f(u)
| r(u,u6r2(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(29,axiom,
( ~ equalish(u6r2(u),u6r1(u))
| f(u)
| d(u6r3(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(30,axiom,
( ~ equalish(u6r2(u),u6r1(u))
| f(u)
| d(u6r4(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(33,axiom,
( ~ equalish(u6r4(u),u6r3(u))
| f(u)
| c(u6r1(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(38,axiom,
( ~ equalish(u6r4(u),u6r3(u))
| f(u)
| c(u6r2(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(46,axiom,
( f(u)
| r(u,u6r3(u))
| r(u,u6r1(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(47,axiom,
( f(u)
| r(u,u6r4(u))
| r(u,u6r1(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(51,axiom,
( f(u)
| r(u,u6r3(u))
| r(u,u6r2(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(52,axiom,
( f(u)
| r(u,u6r4(u))
| r(u,u6r2(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(36,axiom,
( f(u)
| c(u6r1(u))
| r(u,u6r3(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(37,axiom,
( f(u)
| c(u6r1(u))
| r(u,u6r4(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(41,axiom,
( f(u)
| c(u6r2(u))
| r(u,u6r3(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(42,axiom,
( f(u)
| c(u6r2(u))
| r(u,u6r4(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(44,axiom,
( f(u)
| d(u6r3(u))
| r(u,u6r1(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(45,axiom,
( f(u)
| d(u6r4(u))
| r(u,u6r1(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(49,axiom,
( f(u)
| d(u6r3(u))
| r(u,u6r2(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(50,axiom,
( f(u)
| d(u6r4(u))
| r(u,u6r2(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(3,axiom,
( ~ s2least(u)
| ~ equalish(u1r2(u),u1r1(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(20,axiom,
( ~ equalish(u5r2(u),u5r1(u))
| r2most(u) ),
file('KRS008-1.p',unknown),
[] ).
cnf(21,axiom,
( ~ equalish(u5r3(u),u5r1(u))
| r2most(u) ),
file('KRS008-1.p',unknown),
[] ).
cnf(22,axiom,
( ~ equalish(u5r3(u),u5r2(u))
| r2most(u) ),
file('KRS008-1.p',unknown),
[] ).
cnf(10,axiom,
( ~ equalish(u3r2(u),u3r1(u))
| s1most(u) ),
file('KRS008-1.p',unknown),
[] ).
cnf(34,axiom,
( f(u)
| d(u6r3(u))
| c(u6r1(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(35,axiom,
( f(u)
| d(u6r4(u))
| c(u6r1(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(39,axiom,
( f(u)
| d(u6r3(u))
| c(u6r2(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(40,axiom,
( f(u)
| d(u6r4(u))
| c(u6r2(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(14,axiom,
( ~ e(u)
| r(u,u4r2(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(16,axiom,
( ~ e(u)
| r(u,u4r1(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(4,axiom,
( ~ s2least(u)
| s(u,u1r1(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(5,axiom,
( ~ s2least(u)
| s(u,u1r2(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(23,axiom,
( r2most(u)
| r(u,u5r1(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(24,axiom,
( r2most(u)
| r(u,u5r2(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(25,axiom,
( r2most(u)
| r(u,u5r3(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(11,axiom,
( s1most(u)
| s(u,u3r1(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(12,axiom,
( s1most(u)
| s(u,u3r2(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(13,axiom,
( ~ e(u)
| d(u4r2(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(15,axiom,
( ~ e(u)
| c(u4r1(u)) ),
file('KRS008-1.p',unknown),
[] ).
cnf(2,axiom,
( ~ s2least(u)
| c(u) ),
file('KRS008-1.p',unknown),
[] ).
cnf(8,axiom,
( ~ s1most(u)
| d(u) ),
file('KRS008-1.p',unknown),
[] ).
cnf(17,axiom,
( ~ e(u)
| r2most(u) ),
file('KRS008-1.p',unknown),
[] ).
cnf(1,axiom,
( ~ c(u)
| s2least(u) ),
file('KRS008-1.p',unknown),
[] ).
cnf(55,plain,
r(exist,u4r2(exist)),
inference(res,[status(thm),theory(equality)],[53,14]),
[iquote('0:Res:53.0,14.0')] ).
cnf(56,plain,
r(exist,u4r1(exist)),
inference(res,[status(thm),theory(equality)],[53,16]),
[iquote('0:Res:53.0,16.0')] ).
cnf(57,plain,
d(u4r2(exist)),
inference(res,[status(thm),theory(equality)],[53,13]),
[iquote('0:Res:53.0,13.0')] ).
cnf(7,axiom,
( ~ d(u)
| s1most(u) ),
file('KRS008-1.p',unknown),
[] ).
cnf(58,plain,
c(u4r1(exist)),
inference(res,[status(thm),theory(equality)],[53,15]),
[iquote('0:Res:53.0,15.0')] ).
cnf(54,axiom,
~ f(exist),
file('KRS008-1.p',unknown),
[] ).
cnf(59,plain,
r2most(exist),
inference(res,[status(thm),theory(equality)],[53,17]),
[iquote('0:Res:53.0,17.0')] ).
cnf(175,plain,
r(exist,u6r3(exist)),
inference(spt,[],[75]),
[iquote('4:Spt:75.1')] ).
cnf(53,axiom,
e(exist),
file('KRS008-1.p',unknown),
[] ).
cnf(174,plain,
r(exist,u6r4(exist)),
inference(spt,[],[76]),
[iquote('3:Spt:76.1')] ).
cnf(173,plain,
d(u6r3(exist)),
inference(spt,[],[83]),
[iquote('2:Spt:83.0')] ).
cnf(172,plain,
d(u6r4(exist)),
inference(spt,[],[84]),
[iquote('1:Spt:84.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : KRS008-1 : TPTP v8.1.0. Released v2.0.0.
% 0.06/0.12 % Command : run_spass %d %s
% 0.11/0.33 % Computer : n019.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 600
% 0.11/0.33 % DateTime : Tue Jun 7 14:34:25 EDT 2022
% 0.11/0.33 % CPUTime :
% 0.52/0.70
% 0.52/0.70 SPASS V 3.9
% 0.52/0.70 SPASS beiseite: Completion found.
% 0.52/0.70 % SZS status CounterSatisfiable
% 0.52/0.70 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.52/0.70 SPASS derived 3034 clauses, backtracked 5 clauses, performed 13 splits and kept 554 clauses.
% 0.52/0.70 SPASS allocated 79295 KBytes.
% 0.52/0.70 SPASS spent 0:00:00.37 on the problem.
% 0.52/0.70 0:00:00.04 for the input.
% 0.52/0.70 0:00:00.00 for the FLOTTER CNF translation.
% 0.52/0.70 0:00:00.06 for inferences.
% 0.52/0.70 0:00:00.00 for the backtracking.
% 0.52/0.70 0:00:00.23 for the reduction.
% 0.52/0.70
% 0.52/0.70
% 0.52/0.70 The saturated set of worked-off clauses is :
% 0.52/0.70 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------