%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : RNG049+2 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n025.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 : Mon Jul 18 20:41:19 EDT 2022
% Result : Theorem 32.74s 32.94s
% Output : Refutation 57.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 66
% Number of leaves : 31
% Syntax : Number of clauses : 265 ( 9 unt; 12 nHn; 265 RR)
% Number of literals : 1103 ( 0 equ; 842 neg)
% Maximal clause size : 9 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(2,axiom,
aScalar0(sz0z00),
file('RNG049+2.p',unknown),
[] ).
cnf(3,axiom,
aVector0(xs),
file('RNG049+2.p',unknown),
[] ).
cnf(9,axiom,
~ sdtlseqdt0(sz0z00,sdtasasdt0(xs,xs)),
file('RNG049+2.p',unknown),
[] ).
cnf(11,axiom,
( ~ aScalar0(u)
| aScalar0(smndt0(u)) ),
file('RNG049+2.p',unknown),
[] ).
cnf(12,axiom,
( ~ aScalar0(u)
| sdtlseqdt0(u,u) ),
file('RNG049+2.p',unknown),
[] ).
cnf(19,axiom,
( ~ aScalar0(u)
| equal(sdtpldt0(u,sz0z00),u) ),
file('RNG049+2.p',unknown),
[] ).
cnf(20,axiom,
( ~ aScalar0(u)
| equal(sdtpldt0(sz0z00,u),u) ),
file('RNG049+2.p',unknown),
[] ).
cnf(21,axiom,
( ~ aScalar0(u)
| equal(sdtasdt0(u,sz0z00),sz0z00) ),
file('RNG049+2.p',unknown),
[] ).
cnf(23,axiom,
( ~ aScalar0(u)
| equal(smndt0(smndt0(u)),u) ),
file('RNG049+2.p',unknown),
[] ).
cnf(24,axiom,
( ~ aScalar0(u)
| sdtlseqdt0(sz0z00,sdtasdt0(u,u)) ),
file('RNG049+2.p',unknown),
[] ).
cnf(25,axiom,
( ~ aScalar0(u)
| equal(sdtpldt0(u,smndt0(u)),sz0z00) ),
file('RNG049+2.p',unknown),
[] ).
cnf(26,axiom,
( ~ aScalar0(u)
| equal(sdtpldt0(smndt0(u),u),sz0z00) ),
file('RNG049+2.p',unknown),
[] ).
cnf(27,axiom,
( ~ aScalar0(u)
| ~ aScalar0(v)
| aScalar0(sdtpldt0(v,u)) ),
file('RNG049+2.p',unknown),
[] ).
cnf(28,axiom,
( ~ aScalar0(u)
| ~ aScalar0(v)
| aScalar0(sdtasdt0(v,u)) ),
file('RNG049+2.p',unknown),
[] ).
cnf(34,axiom,
( ~ aScalar0(u)
| ~ aScalar0(v)
| sdtlseqdt0(u,v)
| sdtlseqdt0(v,u) ),
file('RNG049+2.p',unknown),
[] ).
cnf(35,axiom,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtpldt0(v,u),sdtpldt0(u,v)) ),
file('RNG049+2.p',unknown),
[] ).
cnf(36,axiom,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtasdt0(v,u),sdtasdt0(u,v)) ),
file('RNG049+2.p',unknown),
[] ).
cnf(40,axiom,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtasdt0(v,smndt0(u)),smndt0(sdtasdt0(v,u))) ),
file('RNG049+2.p',unknown),
[] ).
cnf(41,axiom,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtasdt0(smndt0(v),u),smndt0(sdtasdt0(v,u))) ),
file('RNG049+2.p',unknown),
[] ).
cnf(43,axiom,
( ~ aVector0(u)
| ~ aVector0(v)
| ~ equal(aDimensionOf0(v),aDimensionOf0(u))
| aScalar0(sdtasasdt0(v,u)) ),
file('RNG049+2.p',unknown),
[] ).
cnf(44,axiom,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ sdtlseqdt0(v,u)
| ~ sdtlseqdt0(u,v)
| equal(v,u) ),
file('RNG049+2.p',unknown),
[] ).
cnf(46,axiom,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ sdtlseqdt0(sz0z00,v)
| ~ sdtlseqdt0(sz0z00,u)
| sdtlseqdt0(sz0z00,sdtpldt0(v,u)) ),
file('RNG049+2.p',unknown),
[] ).
cnf(48,axiom,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| ~ sdtlseqdt0(v,u)
| ~ sdtlseqdt0(w,v)
| sdtlseqdt0(w,u) ),
file('RNG049+2.p',unknown),
[] ).
cnf(49,axiom,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| equal(sdtasdt0(sdtasdt0(w,v),u),sdtasdt0(w,sdtasdt0(v,u))) ),
file('RNG049+2.p',unknown),
[] ).
cnf(50,axiom,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| equal(sdtpldt0(sdtpldt0(w,v),u),sdtpldt0(w,sdtpldt0(v,u))) ),
file('RNG049+2.p',unknown),
[] ).
cnf(53,axiom,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| equal(sdtasdt0(sdtpldt0(w,v),u),sdtpldt0(sdtasdt0(w,u),sdtasdt0(v,u))) ),
file('RNG049+2.p',unknown),
[] ).
cnf(54,axiom,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| equal(sdtasdt0(w,sdtpldt0(v,u)),sdtpldt0(sdtasdt0(w,v),sdtasdt0(w,u))) ),
file('RNG049+2.p',unknown),
[] ).
cnf(56,axiom,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ sdtlseqdt0(sz0z00,v)
| ~ sdtlseqdt0(sz0z00,u)
| ~ equal(sdtasdt0(v,v),sdtasdt0(u,u))
| equal(v,u) ),
file('RNG049+2.p',unknown),
[] ).
cnf(57,axiom,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| ~ aScalar0(x)
| ~ sdtlseqdt0(x,w)
| ~ sdtlseqdt0(v,u)
| sdtlseqdt0(sdtpldt0(x,v),sdtpldt0(w,u)) ),
file('RNG049+2.p',unknown),
[] ).
cnf(58,axiom,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| ~ aScalar0(x)
| ~ sdtlseqdt0(x,w)
| ~ sdtlseqdt0(v,u)
| ~ sdtlseqdt0(sz0z00,v)
| sdtlseqdt0(sdtasdt0(x,v),sdtasdt0(w,u)) ),
file('RNG049+2.p',unknown),
[] ).
cnf(61,axiom,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| ~ aScalar0(x)
| equal(sdtasdt0(sdtpldt0(x,w),sdtpldt0(v,u)),sdtpldt0(sdtpldt0(sdtasdt0(x,v),sdtasdt0(x,u)),sdtpldt0(sdtasdt0(w,v),sdtasdt0(w,u)))) ),
file('RNG049+2.p',unknown),
[] ).
cnf(63,plain,
( ~ aScalar0(sz0z00)
| ~ aScalar0(u)
| ~ aScalar0(sdtasasdt0(xs,xs))
| ~ sdtlseqdt0(sz0z00,u)
| ~ sdtlseqdt0(u,sdtasasdt0(xs,xs)) ),
inference(res,[status(thm),theory(equality)],[48,9]),
[iquote('0:Res:48.5,9.0')] ).
cnf(68,plain,
( ~ aScalar0(u)
| ~ aScalar0(sdtasasdt0(xs,xs))
| ~ sdtlseqdt0(u,sdtasasdt0(xs,xs))
| ~ sdtlseqdt0(sz0z00,u) ),
inference(mrr,[status(thm)],[63,2]),
[iquote('0:MRR:63.0,2.0')] ).
cnf(194,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(u))
| equal(smndt0(sdtasdt0(smndt0(u),v)),sdtasdt0(u,v)) ),
inference(spr,[status(thm),theory(equality)],[23,41]),
[iquote('0:SpR:23.1,41.2')] ).
cnf(201,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(u))
| equal(smndt0(smndt0(sdtasdt0(u,v))),sdtasdt0(u,v)) ),
inference(rew,[status(thm),theory(equality)],[41,194]),
[iquote('0:Rew:41.2,194.3')] ).
cnf(202,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(smndt0(smndt0(sdtasdt0(u,v))),sdtasdt0(u,v)) ),
inference(ssi,[status(thm)],[201,11]),
[iquote('0:SSi:201.2,11.1')] ).
cnf(295,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(sdtasdt0(u,v)))
| equal(sdtpldt0(sdtasdt0(u,v),smndt0(sdtasdt0(u,v))),sz0z00) ),
inference(spr,[status(thm),theory(equality)],[202,26]),
[iquote('0:SpR:202.2,26.1')] ).
cnf(320,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtpldt0(sdtasdt0(u,v),smndt0(sdtasdt0(u,v))),sz0z00) ),
inference(ssi,[status(thm)],[295,11,28]),
[iquote('0:SSi:295.2,11.2,28.1')] ).
cnf(583,plain,
( ~ aScalar0(u)
| ~ aScalar0(sdtasdt0(u,u))
| ~ aScalar0(sz0z00)
| ~ sdtlseqdt0(sdtasdt0(u,u),sz0z00)
| equal(sdtasdt0(u,u),sz0z00) ),
inference(res,[status(thm),theory(equality)],[24,44]),
[iquote('0:Res:24.1,44.2')] ).
cnf(593,plain,
( ~ aScalar0(u)
| ~ sdtlseqdt0(sdtasdt0(u,u),sz0z00)
| equal(sdtasdt0(u,u),sz0z00) ),
inference(ssi,[status(thm)],[583,2,28]),
[iquote('0:SSi:583.2,583.1,2.2,28.0')] ).
cnf(1028,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(u)
| ~ aScalar0(sz0z00)
| equal(sdtpldt0(sz0z00,sdtpldt0(u,v)),sdtpldt0(u,v)) ),
inference(spr,[status(thm),theory(equality)],[20,50]),
[iquote('0:SpR:20.1,50.3')] ).
cnf(1029,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(u)
| ~ aScalar0(smndt0(u))
| equal(sdtpldt0(smndt0(u),sdtpldt0(u,v)),sdtpldt0(sz0z00,v)) ),
inference(spr,[status(thm),theory(equality)],[26,50]),
[iquote('0:SpR:26.1,50.3')] ).
cnf(1032,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(u))
| ~ aScalar0(u)
| equal(sdtpldt0(u,sdtpldt0(smndt0(u),v)),sdtpldt0(sz0z00,v)) ),
inference(spr,[status(thm),theory(equality)],[25,50]),
[iquote('0:SpR:25.1,50.3')] ).
cnf(1038,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(sz0z00)
| equal(sdtpldt0(sz0z00,sdtpldt0(v,u)),sdtpldt0(v,u)) ),
inference(obv,[status(thm),theory(equality)],[1028]),
[iquote('0:Obv:1028.0')] ).
cnf(1039,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtpldt0(sz0z00,sdtpldt0(v,u)),sdtpldt0(v,u)) ),
inference(ssi,[status(thm)],[1038,2]),
[iquote('0:SSi:1038.2,2.0')] ).
cnf(1040,plain,
( ~ aScalar0(u)
| ~ aScalar0(smndt0(v))
| ~ aScalar0(v)
| equal(sdtpldt0(v,sdtpldt0(smndt0(v),u)),sdtpldt0(sz0z00,u)) ),
inference(obv,[status(thm),theory(equality)],[1032]),
[iquote('0:Obv:1032.0')] ).
cnf(1041,plain,
( ~ aScalar0(u)
| ~ aScalar0(smndt0(v))
| ~ aScalar0(v)
| equal(sdtpldt0(v,sdtpldt0(smndt0(v),u)),u) ),
inference(rew,[status(thm),theory(equality)],[20,1040]),
[iquote('0:Rew:20.1,1040.3')] ).
cnf(1042,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtpldt0(v,sdtpldt0(smndt0(v),u)),u) ),
inference(ssi,[status(thm)],[1041,11]),
[iquote('0:SSi:1041.1,11.1')] ).
cnf(1043,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(v))
| equal(sdtpldt0(smndt0(v),sdtpldt0(v,u)),sdtpldt0(sz0z00,u)) ),
inference(obv,[status(thm),theory(equality)],[1029]),
[iquote('0:Obv:1029.0')] ).
cnf(1044,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(v))
| equal(sdtpldt0(smndt0(v),sdtpldt0(v,u)),u) ),
inference(rew,[status(thm),theory(equality)],[20,1043]),
[iquote('0:Rew:20.1,1043.3')] ).
cnf(1045,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtpldt0(smndt0(v),sdtpldt0(v,u)),u) ),
inference(ssi,[status(thm)],[1044,11]),
[iquote('0:SSi:1044.2,11.1')] ).
cnf(1079,plain,
( ~ aScalar0(smndt0(u))
| ~ aScalar0(v)
| ~ aScalar0(v)
| ~ aScalar0(u)
| equal(sdtpldt0(u,sdtpldt0(v,smndt0(u))),v) ),
inference(spr,[status(thm),theory(equality)],[35,1042]),
[iquote('0:SpR:35.2,1042.2')] ).
cnf(1085,plain,
( ~ aScalar0(smndt0(u))
| ~ aScalar0(v)
| ~ aScalar0(u)
| equal(sdtpldt0(u,sdtpldt0(v,smndt0(u))),v) ),
inference(obv,[status(thm),theory(equality)],[1079]),
[iquote('0:Obv:1079.1')] ).
cnf(1086,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtpldt0(v,sdtpldt0(u,smndt0(v))),u) ),
inference(ssi,[status(thm)],[1085,11]),
[iquote('0:SSi:1085.0,11.1')] ).
cnf(1109,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(v)
| ~ aScalar0(u)
| equal(sdtpldt0(smndt0(u),sdtpldt0(v,u)),v) ),
inference(spr,[status(thm),theory(equality)],[35,1045]),
[iquote('0:SpR:35.2,1045.2')] ).
cnf(1125,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtpldt0(smndt0(v),sdtpldt0(u,v)),u) ),
inference(obv,[status(thm),theory(equality)],[1109]),
[iquote('0:Obv:1109.1')] ).
cnf(1140,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(sdtpldt0(u,smndt0(v)))
| ~ aScalar0(v)
| equal(sdtpldt0(smndt0(v),u),sdtpldt0(u,smndt0(v))) ),
inference(spr,[status(thm),theory(equality)],[1086,1045]),
[iquote('0:SpR:1086.2,1045.2')] ).
cnf(1165,plain,
( ~ aScalar0(u)
| ~ aScalar0(sdtpldt0(u,smndt0(v)))
| ~ aScalar0(v)
| equal(sdtpldt0(smndt0(v),u),sdtpldt0(u,smndt0(v))) ),
inference(obv,[status(thm),theory(equality)],[1140]),
[iquote('0:Obv:1140.1')] ).
cnf(1166,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtpldt0(smndt0(v),u),sdtpldt0(u,smndt0(v))) ),
inference(ssi,[status(thm)],[1165,27,11]),
[iquote('0:SSi:1165.1,27.1,11.2')] ).
cnf(1181,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(v))
| ~ aScalar0(sdtpldt0(u,v))
| equal(sdtpldt0(smndt0(sdtpldt0(u,v)),u),smndt0(v)) ),
inference(spr,[status(thm),theory(equality)],[1125]),
[iquote('0:SpR:1125.2,1125.2')] ).
cnf(1196,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(v))
| ~ aScalar0(sdtpldt0(v,u))
| equal(sdtpldt0(smndt0(sdtpldt0(v,u)),u),smndt0(v)) ),
inference(spr,[status(thm),theory(equality)],[1045,1125]),
[iquote('0:SpR:1045.2,1125.2')] ).
cnf(1197,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(v)
| ~ aScalar0(sdtpldt0(u,smndt0(v)))
| equal(sdtpldt0(smndt0(sdtpldt0(u,smndt0(v))),u),v) ),
inference(spr,[status(thm),theory(equality)],[1086,1125]),
[iquote('0:SpR:1086.2,1125.2')] ).
cnf(1214,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(sdtpldt0(u,smndt0(v)))
| equal(sdtpldt0(smndt0(sdtpldt0(u,smndt0(v))),u),v) ),
inference(obv,[status(thm),theory(equality)],[1197]),
[iquote('0:Obv:1197.1')] ).
cnf(1215,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(sdtpldt0(u,smndt0(v)))
| equal(sdtpldt0(u,smndt0(sdtpldt0(u,smndt0(v)))),v) ),
inference(rew,[status(thm),theory(equality)],[1166,1214]),
[iquote('0:Rew:1166.2,1214.3')] ).
cnf(1216,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtpldt0(u,smndt0(sdtpldt0(u,smndt0(v)))),v) ),
inference(ssi,[status(thm)],[1215,27,11]),
[iquote('0:SSi:1215.2,27.1,11.2')] ).
cnf(1217,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(v))
| ~ aScalar0(sdtpldt0(v,u))
| equal(sdtpldt0(u,smndt0(sdtpldt0(v,u))),smndt0(v)) ),
inference(rew,[status(thm),theory(equality)],[1166,1196]),
[iquote('0:Rew:1166.2,1196.4')] ).
cnf(1218,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtpldt0(u,smndt0(sdtpldt0(v,u))),smndt0(v)) ),
inference(ssi,[status(thm)],[1217,27,11]),
[iquote('0:SSi:1217.3,1217.2,27.1,11.2')] ).
cnf(1224,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(v))
| ~ aScalar0(sdtpldt0(u,v))
| equal(sdtpldt0(u,smndt0(sdtpldt0(u,v))),smndt0(v)) ),
inference(rew,[status(thm),theory(equality)],[1166,1181]),
[iquote('0:Rew:1166.2,1181.4')] ).
cnf(1225,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtpldt0(u,smndt0(sdtpldt0(u,v))),smndt0(v)) ),
inference(ssi,[status(thm)],[1224,27,11]),
[iquote('0:SSi:1224.3,1224.2,27.1,11.2')] ).
cnf(1243,plain,
( ~ aScalar0(sdtasdt0(u,v))
| ~ aScalar0(v)
| ~ aScalar0(u)
| ~ aScalar0(sdtasdt0(u,v))
| sdtlseqdt0(sz0z00,sdtasdt0(u,sdtasdt0(v,sdtasdt0(u,v)))) ),
inference(spr,[status(thm),theory(equality)],[49,24]),
[iquote('0:SpR:49.3,24.1')] ).
cnf(1262,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| ~ aScalar0(v)
| ~ aScalar0(u)
| equal(sdtasdt0(sdtasdt0(v,u),w),sdtasdt0(u,sdtasdt0(v,w))) ),
inference(spr,[status(thm),theory(equality)],[36,49]),
[iquote('0:SpR:36.2,49.3')] ).
cnf(1288,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(sdtasdt0(v,u))
| sdtlseqdt0(sz0z00,sdtasdt0(v,sdtasdt0(u,sdtasdt0(v,u)))) ),
inference(obv,[status(thm),theory(equality)],[1243]),
[iquote('0:Obv:1243.0')] ).
cnf(1289,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| sdtlseqdt0(sz0z00,sdtasdt0(v,sdtasdt0(u,sdtasdt0(v,u)))) ),
inference(ssi,[status(thm)],[1288,28]),
[iquote('0:SSi:1288.2,28.2')] ).
cnf(1290,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| equal(sdtasdt0(sdtasdt0(v,w),u),sdtasdt0(w,sdtasdt0(v,u))) ),
inference(obv,[status(thm),theory(equality)],[1262]),
[iquote('0:Obv:1262.1')] ).
cnf(1291,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| equal(sdtasdt0(v,sdtasdt0(w,u)),sdtasdt0(w,sdtasdt0(v,u))) ),
inference(rew,[status(thm),theory(equality)],[49,1290]),
[iquote('0:Rew:49.3,1290.3')] ).
cnf(1485,plain,
( ~ aScalar0(u)
| ~ aScalar0(u)
| ~ aScalar0(smndt0(u))
| equal(sdtpldt0(sz0z00,sz0z00),sz0z00) ),
inference(spr,[status(thm),theory(equality)],[26,1039]),
[iquote('0:SpR:26.1,1039.2')] ).
cnf(1499,plain,
( ~ aScalar0(u)
| ~ aScalar0(smndt0(u))
| equal(sdtpldt0(sz0z00,sz0z00),sz0z00) ),
inference(obv,[status(thm),theory(equality)],[1485]),
[iquote('0:Obv:1485.0')] ).
cnf(1500,plain,
( ~ aScalar0(u)
| equal(sdtpldt0(sz0z00,sz0z00),sz0z00) ),
inference(ssi,[status(thm)],[1499,11]),
[iquote('0:SSi:1499.1,11.1')] ).
cnf(1524,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| ~ sdtlseqdt0(w,v)
| sdtlseqdt0(u,v)
| sdtlseqdt0(w,u) ),
inference(res,[status(thm),theory(equality)],[34,48]),
[iquote('0:Res:34.3,48.3')] ).
cnf(1528,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| ~ sdtlseqdt0(w,v)
| sdtlseqdt0(u,v)
| sdtlseqdt0(w,u) ),
inference(obv,[status(thm),theory(equality)],[1524]),
[iquote('0:Obv:1524.1')] ).
cnf(1545,plain,
equal(sdtpldt0(sz0z00,sz0z00),sz0z00),
inference(ems,[status(thm)],[1500,2]),
[iquote('0:EmS:1500.0,2.0')] ).
cnf(1682,plain,
( ~ aScalar0(sz0z00)
| ~ aScalar0(u)
| ~ aScalar0(smndt0(sdtpldt0(sz0z00,smndt0(u))))
| equal(smndt0(sdtpldt0(sz0z00,smndt0(u))),u) ),
inference(spr,[status(thm),theory(equality)],[1216,20]),
[iquote('0:SpR:1216.2,20.1')] ).
cnf(1683,plain,
( ~ aScalar0(smndt0(u))
| ~ aScalar0(v)
| ~ aScalar0(smndt0(sdtpldt0(smndt0(u),smndt0(v))))
| ~ aScalar0(u)
| equal(smndt0(sdtpldt0(smndt0(u),smndt0(v))),sdtpldt0(u,v)) ),
inference(spr,[status(thm),theory(equality)],[1216,1042]),
[iquote('0:SpR:1216.2,1042.2')] ).
cnf(1686,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(sdtpldt0(u,smndt0(v))))
| ~ aScalar0(u)
| equal(sdtpldt0(smndt0(u),v),smndt0(sdtpldt0(u,smndt0(v)))) ),
inference(spr,[status(thm),theory(equality)],[1216,1045]),
[iquote('0:SpR:1216.2,1045.2')] ).
cnf(1714,plain,
( ~ aScalar0(u)
| equal(smndt0(sdtpldt0(sz0z00,smndt0(u))),u) ),
inference(ssi,[status(thm)],[1682,11,27,2]),
[iquote('0:SSi:1682.2,1682.0,11.0,27.1,2.0,11.2,2.1')] ).
cnf(1727,plain,
( ~ aScalar0(u)
| ~ aScalar0(smndt0(sdtpldt0(v,smndt0(u))))
| ~ aScalar0(v)
| equal(sdtpldt0(smndt0(v),u),smndt0(sdtpldt0(v,smndt0(u)))) ),
inference(obv,[status(thm),theory(equality)],[1686]),
[iquote('0:Obv:1686.0')] ).
cnf(1728,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtpldt0(smndt0(v),u),smndt0(sdtpldt0(v,smndt0(u)))) ),
inference(ssi,[status(thm)],[1727,11,27]),
[iquote('0:SSi:1727.1,11.1,27.2,11.1')] ).
cnf(1736,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(smndt0(sdtpldt0(smndt0(v),smndt0(u))),sdtpldt0(v,u)) ),
inference(ssi,[status(thm)],[1683,11,27]),
[iquote('0:SSi:1683.2,1683.0,11.1,27.1,11.1,11.2,11.1')] ).
cnf(1742,plain,
( ~ aScalar0(u)
| ~ aScalar0(sdtpldt0(sz0z00,smndt0(u)))
| equal(sdtpldt0(sz0z00,smndt0(u)),smndt0(u)) ),
inference(spr,[status(thm),theory(equality)],[1714,23]),
[iquote('0:SpR:1714.1,23.1')] ).
cnf(1773,plain,
( ~ aScalar0(u)
| equal(sdtpldt0(sz0z00,smndt0(u)),smndt0(u)) ),
inference(ssi,[status(thm)],[1742,27,2,11]),
[iquote('0:SSi:1742.1,27.1,2.0,11.2')] ).
cnf(1835,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(sdtpldt0(v,u)))
| ~ aScalar0(u)
| equal(sdtpldt0(smndt0(u),smndt0(v)),smndt0(sdtpldt0(v,u))) ),
inference(spr,[status(thm),theory(equality)],[1218,1045]),
[iquote('0:SpR:1218.2,1045.2')] ).
cnf(1843,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(u)
| ~ aScalar0(smndt0(sdtpldt0(v,u)))
| equal(sdtpldt0(smndt0(smndt0(sdtpldt0(v,u))),smndt0(v)),u) ),
inference(spr,[status(thm),theory(equality)],[1218,1125]),
[iquote('0:SpR:1218.2,1125.2')] ).
cnf(1894,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(sdtpldt0(u,v)))
| equal(sdtpldt0(smndt0(smndt0(sdtpldt0(u,v))),smndt0(u)),v) ),
inference(obv,[status(thm),theory(equality)],[1843]),
[iquote('0:Obv:1843.0')] ).
cnf(1895,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtpldt0(smndt0(smndt0(sdtpldt0(u,v))),smndt0(u)),v) ),
inference(ssi,[status(thm)],[1894,11,27]),
[iquote('0:SSi:1894.2,11.2,27.1')] ).
cnf(1896,plain,
( ~ aScalar0(u)
| ~ aScalar0(smndt0(sdtpldt0(u,v)))
| ~ aScalar0(v)
| equal(sdtpldt0(smndt0(v),smndt0(u)),smndt0(sdtpldt0(u,v))) ),
inference(obv,[status(thm),theory(equality)],[1835]),
[iquote('0:Obv:1835.0')] ).
cnf(1897,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtpldt0(smndt0(v),smndt0(u)),smndt0(sdtpldt0(u,v))) ),
inference(ssi,[status(thm)],[1896,11,27]),
[iquote('0:SSi:1896.1,11.2,27.1')] ).
cnf(2012,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(u)
| ~ aScalar0(smndt0(sdtpldt0(u,smndt0(v))))
| equal(smndt0(smndt0(sdtpldt0(u,smndt0(v)))),sdtpldt0(u,smndt0(v))) ),
inference(spr,[status(thm),theory(equality)],[1216,1225]),
[iquote('0:SpR:1216.2,1225.2')] ).
cnf(2017,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(v))
| ~ aScalar0(sdtpldt0(v,u))
| equal(sdtpldt0(smndt0(v),smndt0(u)),smndt0(sdtpldt0(v,u))) ),
inference(spr,[status(thm),theory(equality)],[1045,1225]),
[iquote('0:SpR:1045.2,1225.2')] ).
cnf(2047,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtpldt0(smndt0(v),smndt0(u)),smndt0(sdtpldt0(v,u))) ),
inference(ssi,[status(thm)],[2017,27,11]),
[iquote('0:SSi:2017.3,2017.2,27.1,11.2')] ).
cnf(2048,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(smndt0(smndt0(sdtpldt0(v,u))),sdtpldt0(v,u)) ),
inference(rew,[status(thm),theory(equality)],[2047,1736]),
[iquote('0:Rew:2047.2,1736.2')] ).
cnf(2049,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(smndt0(sdtpldt0(v,u)),smndt0(sdtpldt0(u,v))) ),
inference(rew,[status(thm),theory(equality)],[2047,1897]),
[iquote('0:Rew:2047.2,1897.2')] ).
cnf(2050,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtpldt0(sdtpldt0(u,v),smndt0(u)),v) ),
inference(rew,[status(thm),theory(equality)],[2048,1895]),
[iquote('0:Rew:2048.2,1895.2')] ).
cnf(2062,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(sdtpldt0(v,smndt0(u))))
| equal(smndt0(smndt0(sdtpldt0(v,smndt0(u)))),sdtpldt0(v,smndt0(u))) ),
inference(obv,[status(thm),theory(equality)],[2012]),
[iquote('0:Obv:2012.0')] ).
cnf(2063,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(smndt0(smndt0(sdtpldt0(v,smndt0(u)))),sdtpldt0(v,smndt0(u))) ),
inference(ssi,[status(thm)],[2062,11,27]),
[iquote('0:SSi:2062.2,11.1,27.2,11.1')] ).
cnf(2086,plain,
( ~ aScalar0(sdtpldt0(u,v))
| ~ aScalar0(v)
| ~ aScalar0(u)
| ~ aScalar0(sdtpldt0(u,v))
| sdtlseqdt0(sz0z00,sdtpldt0(sdtasdt0(u,sdtpldt0(u,v)),sdtasdt0(v,sdtpldt0(u,v)))) ),
inference(spr,[status(thm),theory(equality)],[53,24]),
[iquote('0:SpR:53.3,24.1')] ).
cnf(2148,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(sdtpldt0(v,u))
| sdtlseqdt0(sz0z00,sdtpldt0(sdtasdt0(v,sdtpldt0(v,u)),sdtasdt0(u,sdtpldt0(v,u)))) ),
inference(obv,[status(thm),theory(equality)],[2086]),
[iquote('0:Obv:2086.0')] ).
cnf(2149,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| sdtlseqdt0(sz0z00,sdtpldt0(sdtasdt0(v,sdtpldt0(v,u)),sdtasdt0(u,sdtpldt0(v,u)))) ),
inference(ssi,[status(thm)],[2148,27]),
[iquote('0:SSi:2148.2,27.2')] ).
cnf(2257,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtpldt0(sdtpldt0(v,u),smndt0(u)),v) ),
inference(spr,[status(thm),theory(equality)],[35,2050]),
[iquote('0:SpR:35.2,2050.2')] ).
cnf(2277,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtpldt0(sdtpldt0(v,u),smndt0(u)),v) ),
inference(obv,[status(thm),theory(equality)],[2257]),
[iquote('0:Obv:2257.1')] ).
cnf(2496,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(w))
| ~ aScalar0(sdtpldt0(v,u))
| ~ aScalar0(w)
| equal(sdtpldt0(sdtasdt0(smndt0(w),v),sdtasdt0(smndt0(w),u)),smndt0(sdtasdt0(w,sdtpldt0(v,u)))) ),
inference(spr,[status(thm),theory(equality)],[54,41]),
[iquote('0:SpR:54.3,41.2')] ).
cnf(2507,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| ~ aScalar0(w)
| ~ aScalar0(sdtpldt0(v,u))
| equal(sdtpldt0(sdtpldt0(sdtasdt0(w,v),sdtasdt0(w,u)),smndt0(sdtpldt0(sdtasdt0(w,v),sdtasdt0(w,u)))),sz0z00) ),
inference(spr,[status(thm),theory(equality)],[54,320]),
[iquote('0:SpR:54.3,320.2')] ).
cnf(2608,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(w))
| ~ aScalar0(sdtpldt0(v,u))
| ~ aScalar0(w)
| equal(sdtpldt0(smndt0(sdtasdt0(w,v)),smndt0(sdtasdt0(w,u))),smndt0(sdtpldt0(sdtasdt0(w,v),sdtasdt0(w,u)))) ),
inference(rew,[status(thm),theory(equality)],[41,2496,54]),
[iquote('0:Rew:41.2,2496.5,41.2,2496.5,54.3,2496.5')] ).
cnf(2609,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| equal(sdtpldt0(smndt0(sdtasdt0(w,v)),smndt0(sdtasdt0(w,u))),smndt0(sdtpldt0(sdtasdt0(w,v),sdtasdt0(w,u)))) ),
inference(ssi,[status(thm)],[2608,27,11]),
[iquote('0:SSi:2608.3,2608.2,27.1,11.2')] ).
cnf(2617,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| ~ aScalar0(sdtpldt0(v,u))
| equal(sdtpldt0(sdtpldt0(sdtasdt0(w,v),sdtasdt0(w,u)),smndt0(sdtpldt0(sdtasdt0(w,v),sdtasdt0(w,u)))),sz0z00) ),
inference(obv,[status(thm),theory(equality)],[2507]),
[iquote('0:Obv:2507.2')] ).
cnf(2618,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| equal(sdtpldt0(sdtpldt0(sdtasdt0(w,v),sdtasdt0(w,u)),smndt0(sdtpldt0(sdtasdt0(w,v),sdtasdt0(w,u)))),sz0z00) ),
inference(ssi,[status(thm)],[2617,27]),
[iquote('0:SSi:2617.3,27.2')] ).
cnf(3162,plain,
( ~ aScalar0(sz0z00)
| ~ aScalar0(sz0z00)
| ~ aScalar0(u)
| ~ sdtlseqdt0(sz0z00,u)
| ~ sdtlseqdt0(sz0z00,sz0z00)
| ~ equal(sdtasdt0(u,u),sz0z00)
| equal(u,sz0z00) ),
inference(spl,[status(thm),theory(equality)],[21,56]),
[iquote('0:SpL:21.1,56.4')] ).
cnf(3167,plain,
( ~ aScalar0(sz0z00)
| ~ aScalar0(u)
| ~ sdtlseqdt0(sz0z00,u)
| ~ sdtlseqdt0(sz0z00,sz0z00)
| ~ equal(sdtasdt0(u,u),sz0z00)
| equal(u,sz0z00) ),
inference(obv,[status(thm),theory(equality)],[3162]),
[iquote('0:Obv:3162.0')] ).
cnf(3168,plain,
( ~ aScalar0(u)
| ~ sdtlseqdt0(sz0z00,u)
| ~ sdtlseqdt0(sz0z00,sz0z00)
| ~ equal(sdtasdt0(u,u),sz0z00)
| equal(u,sz0z00) ),
inference(ssi,[status(thm)],[3167,2]),
[iquote('0:SSi:3167.0,2.0')] ).
cnf(3301,plain,
( ~ aScalar0(u)
| ~ aScalar0(sz0z00)
| ~ aScalar0(v)
| ~ aScalar0(u)
| ~ aScalar0(w)
| ~ sdtlseqdt0(w,u)
| ~ sdtlseqdt0(v,sz0z00)
| sdtlseqdt0(sdtpldt0(w,v),u) ),
inference(spr,[status(thm),theory(equality)],[19,57]),
[iquote('0:SpR:19.1,57.6')] ).
cnf(3302,plain,
( ~ aScalar0(u)
| ~ aScalar0(smndt0(u))
| ~ aScalar0(v)
| ~ aScalar0(u)
| ~ aScalar0(w)
| ~ sdtlseqdt0(w,u)
| ~ sdtlseqdt0(v,smndt0(u))
| sdtlseqdt0(sdtpldt0(w,v),sz0z00) ),
inference(spr,[status(thm),theory(equality)],[25,57]),
[iquote('0:SpR:25.1,57.6')] ).
cnf(3323,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(u))
| ~ aScalar0(w)
| ~ aScalar0(u)
| ~ sdtlseqdt0(u,w)
| ~ sdtlseqdt0(smndt0(u),v)
| sdtlseqdt0(sz0z00,sdtpldt0(w,v)) ),
inference(spr,[status(thm),theory(equality)],[25,57]),
[iquote('0:SpR:25.1,57.6')] ).
cnf(3348,plain,
( ~ aScalar0(sz0z00)
| ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| ~ sdtlseqdt0(w,v)
| ~ sdtlseqdt0(u,sz0z00)
| sdtlseqdt0(sdtpldt0(w,u),v) ),
inference(obv,[status(thm),theory(equality)],[3301]),
[iquote('0:Obv:3301.0')] ).
cnf(3349,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| ~ sdtlseqdt0(w,v)
| ~ sdtlseqdt0(u,sz0z00)
| sdtlseqdt0(sdtpldt0(w,u),v) ),
inference(ssi,[status(thm)],[3348,2]),
[iquote('0:SSi:3348.0,2.0')] ).
cnf(3352,plain,
( ~ aScalar0(u)
| ~ aScalar0(smndt0(v))
| ~ aScalar0(w)
| ~ aScalar0(v)
| ~ sdtlseqdt0(v,w)
| ~ sdtlseqdt0(smndt0(v),u)
| sdtlseqdt0(sz0z00,sdtpldt0(w,u)) ),
inference(obv,[status(thm),theory(equality)],[3323]),
[iquote('0:Obv:3323.0')] ).
cnf(3353,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| ~ sdtlseqdt0(w,v)
| ~ sdtlseqdt0(smndt0(w),u)
| sdtlseqdt0(sz0z00,sdtpldt0(v,u)) ),
inference(ssi,[status(thm)],[3352,11]),
[iquote('0:SSi:3352.1,11.1')] ).
cnf(3356,plain,
( ~ aScalar0(smndt0(u))
| ~ aScalar0(v)
| ~ aScalar0(u)
| ~ aScalar0(w)
| ~ sdtlseqdt0(w,u)
| ~ sdtlseqdt0(v,smndt0(u))
| sdtlseqdt0(sdtpldt0(w,v),sz0z00) ),
inference(obv,[status(thm),theory(equality)],[3302]),
[iquote('0:Obv:3302.0')] ).
cnf(3357,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| ~ sdtlseqdt0(w,v)
| ~ sdtlseqdt0(u,smndt0(v))
| sdtlseqdt0(sdtpldt0(w,u),sz0z00) ),
inference(ssi,[status(thm)],[3356,11]),
[iquote('0:SSi:3356.0,11.1')] ).
cnf(3897,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(sz0z00)
| ~ aScalar0(w)
| ~ aScalar0(u)
| ~ sdtlseqdt0(u,w)
| ~ sdtlseqdt0(sz0z00,v)
| ~ sdtlseqdt0(sz0z00,sz0z00)
| sdtlseqdt0(sz0z00,sdtasdt0(w,v)) ),
inference(spr,[status(thm),theory(equality)],[21,58]),
[iquote('0:SpR:21.1,58.7')] ).
cnf(3907,plain,
( ~ aScalar0(u)
| ~ aScalar0(sz0z00)
| ~ aScalar0(v)
| ~ aScalar0(w)
| ~ sdtlseqdt0(w,v)
| ~ sdtlseqdt0(sz0z00,u)
| ~ sdtlseqdt0(sz0z00,sz0z00)
| sdtlseqdt0(sz0z00,sdtasdt0(v,u)) ),
inference(obv,[status(thm),theory(equality)],[3897]),
[iquote('0:Obv:3897.0')] ).
cnf(3908,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| ~ sdtlseqdt0(w,v)
| ~ sdtlseqdt0(sz0z00,u)
| ~ sdtlseqdt0(sz0z00,sz0z00)
| sdtlseqdt0(sz0z00,sdtasdt0(v,u)) ),
inference(ssi,[status(thm)],[3907,2]),
[iquote('0:SSi:3907.1,2.0')] ).
cnf(4019,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(v))
| ~ aScalar0(u)
| equal(sdtpldt0(smndt0(sdtpldt0(v,smndt0(u))),smndt0(smndt0(v))),u) ),
inference(spr,[status(thm),theory(equality)],[1728,2050]),
[iquote('0:SpR:1728.2,2050.2')] ).
cnf(4060,plain,
( ~ aScalar0(u)
| ~ aScalar0(smndt0(u))
| ~ aScalar0(v)
| equal(sdtpldt0(smndt0(sdtpldt0(u,smndt0(v))),smndt0(smndt0(u))),v) ),
inference(obv,[status(thm),theory(equality)],[4019]),
[iquote('0:Obv:4019.0')] ).
cnf(4061,plain,
( ~ aScalar0(u)
| ~ aScalar0(smndt0(u))
| ~ aScalar0(v)
| equal(sdtpldt0(smndt0(sdtpldt0(u,smndt0(v))),u),v) ),
inference(rew,[status(thm),theory(equality)],[23,4060]),
[iquote('0:Rew:23.1,4060.3')] ).
cnf(4062,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtpldt0(smndt0(sdtpldt0(u,smndt0(v))),u),v) ),
inference(ssi,[status(thm)],[4061,11]),
[iquote('0:SSi:4061.1,11.1')] ).
cnf(4218,plain,
( ~ aScalar0(smndt0(u))
| ~ aScalar0(v)
| ~ aScalar0(v)
| ~ aScalar0(u)
| equal(sdtpldt0(smndt0(sdtpldt0(smndt0(u),v)),v),u) ),
inference(spr,[status(thm),theory(equality)],[2049,4062]),
[iquote('0:SpR:2049.2,4062.2')] ).
cnf(4231,plain,
( ~ aScalar0(smndt0(u))
| ~ aScalar0(v)
| ~ aScalar0(u)
| equal(sdtpldt0(smndt0(sdtpldt0(smndt0(u),v)),v),u) ),
inference(obv,[status(thm),theory(equality)],[4218]),
[iquote('0:Obv:4218.1')] ).
cnf(4232,plain,
( ~ aScalar0(smndt0(u))
| ~ aScalar0(v)
| ~ aScalar0(u)
| equal(sdtpldt0(smndt0(smndt0(sdtpldt0(u,smndt0(v)))),v),u) ),
inference(rew,[status(thm),theory(equality)],[1728,4231]),
[iquote('0:Rew:1728.2,4231.3')] ).
cnf(4233,plain,
( ~ aScalar0(smndt0(u))
| ~ aScalar0(v)
| ~ aScalar0(u)
| equal(sdtpldt0(sdtpldt0(u,smndt0(v)),v),u) ),
inference(rew,[status(thm),theory(equality)],[2063,4232]),
[iquote('0:Rew:2063.2,4232.3')] ).
cnf(4234,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtpldt0(sdtpldt0(v,smndt0(u)),u),v) ),
inference(ssi,[status(thm)],[4233,11]),
[iquote('0:SSi:4233.0,11.1')] ).
cnf(4357,plain,
( ~ aScalar0(smndt0(u))
| ~ aScalar0(v)
| ~ aScalar0(u)
| ~ aScalar0(smndt0(v))
| equal(sdtpldt0(smndt0(sdtpldt0(v,smndt0(smndt0(u)))),u),smndt0(v)) ),
inference(spr,[status(thm),theory(equality)],[1728,4234]),
[iquote('0:SpR:1728.2,4234.2')] ).
cnf(4399,plain,
( ~ aScalar0(smndt0(u))
| ~ aScalar0(v)
| ~ aScalar0(u)
| ~ aScalar0(smndt0(v))
| equal(sdtpldt0(smndt0(sdtpldt0(v,u)),u),smndt0(v)) ),
inference(rew,[status(thm),theory(equality)],[23,4357]),
[iquote('0:Rew:23.1,4357.4')] ).
cnf(4400,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtpldt0(smndt0(sdtpldt0(u,v)),v),smndt0(u)) ),
inference(ssi,[status(thm)],[4399,11]),
[iquote('0:SSi:4399.3,4399.0,11.1,11.1')] ).
cnf(5674,plain,
( ~ aScalar0(u)
| ~ aScalar0(smndt0(u))
| ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| equal(sdtasdt0(sdtpldt0(w,v),sz0z00),sdtpldt0(sdtpldt0(sdtasdt0(w,u),sdtasdt0(w,smndt0(u))),sdtpldt0(sdtasdt0(v,u),sdtasdt0(v,smndt0(u))))) ),
inference(spr,[status(thm),theory(equality)],[25,61]),
[iquote('0:SpR:25.1,61.4')] ).
cnf(5707,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| ~ aScalar0(smndt0(u))
| ~ aScalar0(u)
| equal(sdtasdt0(sz0z00,sdtpldt0(w,v)),sdtpldt0(sdtpldt0(sdtasdt0(u,w),sdtasdt0(u,v)),sdtpldt0(sdtasdt0(smndt0(u),w),sdtasdt0(smndt0(u),v)))) ),
inference(spr,[status(thm),theory(equality)],[25,61]),
[iquote('0:SpR:25.1,61.4')] ).
cnf(5761,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(w))
| ~ aScalar0(w)
| equal(sdtasdt0(sz0z00,sdtpldt0(v,u)),sdtpldt0(sdtpldt0(sdtasdt0(w,v),sdtasdt0(w,u)),sdtpldt0(sdtasdt0(smndt0(w),v),sdtasdt0(smndt0(w),u)))) ),
inference(obv,[status(thm),theory(equality)],[5707]),
[iquote('0:Obv:5707.0')] ).
cnf(5762,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(w))
| ~ aScalar0(w)
| equal(sdtasdt0(sz0z00,sdtpldt0(v,u)),sdtpldt0(sdtpldt0(sdtasdt0(w,v),sdtasdt0(w,u)),sdtpldt0(smndt0(sdtasdt0(w,v)),smndt0(sdtasdt0(w,u))))) ),
inference(rew,[status(thm),theory(equality)],[41,5761]),
[iquote('0:Rew:41.2,5761.4,41.2,5761.4')] ).
cnf(5763,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(w))
| ~ aScalar0(w)
| equal(sdtasdt0(sz0z00,sdtpldt0(v,u)),sz0z00) ),
inference(rew,[status(thm),theory(equality)],[2618,5762,2609]),
[iquote('0:Rew:2618.3,5762.4,2609.3,5762.4')] ).
cnf(5764,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| equal(sdtasdt0(sz0z00,sdtpldt0(v,u)),sz0z00) ),
inference(ssi,[status(thm)],[5763,11]),
[iquote('0:SSi:5763.2,11.1')] ).
cnf(5768,plain,
( ~ aScalar0(smndt0(u))
| ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| equal(sdtasdt0(sdtpldt0(w,v),sz0z00),sdtpldt0(sdtpldt0(sdtasdt0(w,u),sdtasdt0(w,smndt0(u))),sdtpldt0(sdtasdt0(v,u),sdtasdt0(v,smndt0(u))))) ),
inference(obv,[status(thm),theory(equality)],[5674]),
[iquote('0:Obv:5674.0')] ).
cnf(5769,plain,
( ~ aScalar0(smndt0(u))
| ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| equal(sdtasdt0(sdtpldt0(w,v),sz0z00),sz0z00) ),
inference(rew,[status(thm),theory(equality)],[1545,5768,320,40]),
[iquote('0:Rew:1545.0,5768.4,320.2,5768.4,40.2,5768.4,320.2,5768.4,40.2,5768.4')] ).
cnf(5770,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| equal(sdtasdt0(sdtpldt0(w,v),sz0z00),sz0z00) ),
inference(ssi,[status(thm)],[5769,11]),
[iquote('0:SSi:5769.0,11.1')] ).
cnf(6216,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtasdt0(sz0z00,sdtpldt0(v,u)),sz0z00) ),
inference(ems,[status(thm)],[5764,2]),
[iquote('0:EmS:5764.2,2.0')] ).
cnf(6248,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtasdt0(sdtpldt0(v,u),sz0z00),sz0z00) ),
inference(ems,[status(thm)],[5770,2]),
[iquote('0:EmS:5770.0,2.0')] ).
cnf(6293,plain,
( ~ aScalar0(u)
| ~ aScalar0(u)
| ~ aScalar0(smndt0(u))
| equal(sdtasdt0(sz0z00,sz0z00),sz0z00) ),
inference(spr,[status(thm),theory(equality)],[26,6216]),
[iquote('0:SpR:26.1,6216.2')] ).
cnf(6330,plain,
( ~ aScalar0(u)
| ~ aScalar0(smndt0(u))
| equal(sdtasdt0(sz0z00,sz0z00),sz0z00) ),
inference(obv,[status(thm),theory(equality)],[6293]),
[iquote('0:Obv:6293.0')] ).
cnf(6331,plain,
( ~ aScalar0(u)
| equal(sdtasdt0(sz0z00,sz0z00),sz0z00) ),
inference(ssi,[status(thm)],[6330,11]),
[iquote('0:SSi:6330.1,11.1')] ).
cnf(6381,plain,
equal(sdtasdt0(sz0z00,sz0z00),sz0z00),
inference(ems,[status(thm)],[6331,2]),
[iquote('0:EmS:6331.0,2.0')] ).
cnf(6643,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(sdtpldt0(u,v)))
| equal(sdtasdt0(smndt0(u),sz0z00),sz0z00) ),
inference(spr,[status(thm),theory(equality)],[4400,6248]),
[iquote('0:SpR:4400.2,6248.2')] ).
cnf(6656,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(sdtpldt0(u,v)))
| equal(sdtasdt0(smndt0(u),sz0z00),sz0z00) ),
inference(obv,[status(thm),theory(equality)],[6643]),
[iquote('0:Obv:6643.1')] ).
cnf(6657,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtasdt0(smndt0(u),sz0z00),sz0z00) ),
inference(ssi,[status(thm)],[6656,11,27]),
[iquote('0:SSi:6656.2,11.2,27.1')] ).
cnf(6700,plain,
( ~ aScalar0(u)
| equal(sdtasdt0(smndt0(u),sz0z00),sz0z00) ),
inference(ems,[status(thm)],[6657,2]),
[iquote('0:EmS:6657.1,2.0')] ).
cnf(6845,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(sdtasdt0(u,v)))
| equal(sdtasdt0(sdtasdt0(u,v),sz0z00),sz0z00) ),
inference(spr,[status(thm),theory(equality)],[202,6700]),
[iquote('0:SpR:202.2,6700.1')] ).
cnf(6866,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtasdt0(sdtasdt0(u,v),sz0z00),sz0z00) ),
inference(ssi,[status(thm)],[6845,11,28]),
[iquote('0:SSi:6845.2,11.2,28.1')] ).
cnf(7729,plain,
( ~ aScalar0(u)
| ~ aVector0(xs)
| ~ aVector0(xs)
| ~ sdtlseqdt0(u,sdtasasdt0(xs,xs))
| ~ sdtlseqdt0(sz0z00,u)
| ~ equal(aDimensionOf0(xs),aDimensionOf0(xs)) ),
inference(sor,[status(thm)],[68,43]),
[iquote('0:SoR:68.1,43.3')] ).
cnf(7730,plain,
( ~ aScalar0(u)
| ~ aVector0(xs)
| ~ sdtlseqdt0(u,sdtasasdt0(xs,xs))
| ~ sdtlseqdt0(sz0z00,u) ),
inference(obv,[status(thm),theory(equality)],[7729]),
[iquote('0:Obv:7729.5')] ).
cnf(7731,plain,
( ~ aScalar0(u)
| ~ sdtlseqdt0(u,sdtasasdt0(xs,xs))
| ~ sdtlseqdt0(sz0z00,u) ),
inference(ssi,[status(thm)],[7730,3]),
[iquote('0:SSi:7730.1,3.0')] ).
cnf(9396,plain,
( ~ aScalar0(u)
| ~ aScalar0(smndt0(u))
| ~ aScalar0(u)
| sdtlseqdt0(sz0z00,sdtpldt0(sdtasdt0(u,sz0z00),sdtasdt0(smndt0(u),sz0z00))) ),
inference(spr,[status(thm),theory(equality)],[25,2149]),
[iquote('0:SpR:25.1,2149.2')] ).
cnf(9455,plain,
( ~ aScalar0(smndt0(u))
| ~ aScalar0(u)
| sdtlseqdt0(sz0z00,sdtpldt0(sdtasdt0(u,sz0z00),sdtasdt0(smndt0(u),sz0z00))) ),
inference(obv,[status(thm),theory(equality)],[9396]),
[iquote('0:Obv:9396.0')] ).
cnf(9456,plain,
( ~ aScalar0(smndt0(u))
| ~ aScalar0(u)
| sdtlseqdt0(sz0z00,sz0z00) ),
inference(rew,[status(thm),theory(equality)],[1545,9455,21,6700]),
[iquote('0:Rew:1545.0,9455.2,21.1,9455.2,6700.1,9455.2')] ).
cnf(9457,plain,
( ~ aScalar0(u)
| sdtlseqdt0(sz0z00,sz0z00) ),
inference(ssi,[status(thm)],[9456,11]),
[iquote('0:SSi:9456.0,11.1')] ).
cnf(9458,plain,
( ~ aScalar0(u)
| ~ sdtlseqdt0(sz0z00,u)
| ~ equal(sdtasdt0(u,u),sz0z00)
| equal(u,sz0z00) ),
inference(mrr,[status(thm)],[3168,9457]),
[iquote('0:MRR:3168.2,9457.1')] ).
cnf(9460,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(w)
| ~ sdtlseqdt0(w,v)
| ~ sdtlseqdt0(sz0z00,u)
| sdtlseqdt0(sz0z00,sdtasdt0(v,u)) ),
inference(mrr,[status(thm)],[3908,9457]),
[iquote('0:MRR:3908.5,9457.1')] ).
cnf(9655,plain,
sdtlseqdt0(sz0z00,sz0z00),
inference(ems,[status(thm)],[9457,2]),
[iquote('0:EmS:9457.0,2.0')] ).
cnf(9772,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(sdtpldt0(v,u))
| ~ sdtlseqdt0(sz0z00,sdtpldt0(v,u))
| ~ equal(sdtpldt0(sdtpldt0(sdtasdt0(v,v),sdtasdt0(v,u)),sdtpldt0(sdtasdt0(u,v),sdtasdt0(u,u))),sz0z00)
| equal(sdtpldt0(v,u),sz0z00) ),
inference(spl,[status(thm),theory(equality)],[61,9458]),
[iquote('0:SpL:61.4,9458.2')] ).
cnf(9787,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(sdtpldt0(v,u))
| ~ sdtlseqdt0(sz0z00,sdtpldt0(v,u))
| ~ equal(sdtpldt0(sdtpldt0(sdtasdt0(v,v),sdtasdt0(v,u)),sdtpldt0(sdtasdt0(u,v),sdtasdt0(u,u))),sz0z00)
| equal(sdtpldt0(v,u),sz0z00) ),
inference(obv,[status(thm),theory(equality)],[9772]),
[iquote('0:Obv:9772.1')] ).
cnf(9788,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ sdtlseqdt0(sz0z00,sdtpldt0(v,u))
| ~ equal(sdtpldt0(sdtpldt0(sdtasdt0(v,v),sdtasdt0(v,u)),sdtpldt0(sdtasdt0(u,v),sdtasdt0(u,u))),sz0z00)
| equal(sdtpldt0(v,u),sz0z00) ),
inference(ssi,[status(thm)],[9787,27]),
[iquote('0:SSi:9787.2,27.2')] ).
cnf(11805,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(u)
| ~ aScalar0(u)
| ~ aScalar0(v)
| sdtlseqdt0(sz0z00,sdtasdt0(v,sdtasdt0(v,sdtasdt0(u,u)))) ),
inference(spr,[status(thm),theory(equality)],[1291,1289]),
[iquote('0:SpR:1291.3,1289.2')] ).
cnf(11906,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| sdtlseqdt0(sz0z00,sdtasdt0(v,sdtasdt0(v,sdtasdt0(u,u)))) ),
inference(obv,[status(thm),theory(equality)],[11805]),
[iquote('0:Obv:11805.2')] ).
cnf(12207,plain,
( ~ aScalar0(u)
| ~ aScalar0(sdtasdt0(v,v))
| ~ aScalar0(v)
| ~ aScalar0(u)
| sdtlseqdt0(sz0z00,sdtasdt0(u,sdtasdt0(sdtasdt0(v,v),u))) ),
inference(spr,[status(thm),theory(equality)],[36,11906]),
[iquote('0:SpR:36.2,11906.2')] ).
cnf(12235,plain,
( ~ aScalar0(sdtasdt0(u,u))
| ~ aScalar0(u)
| ~ aScalar0(v)
| sdtlseqdt0(sz0z00,sdtasdt0(v,sdtasdt0(sdtasdt0(u,u),v))) ),
inference(obv,[status(thm),theory(equality)],[12207]),
[iquote('0:Obv:12207.0')] ).
cnf(12236,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| sdtlseqdt0(sz0z00,sdtasdt0(v,sdtasdt0(sdtasdt0(u,u),v))) ),
inference(ssi,[status(thm)],[12235,28]),
[iquote('0:SSi:12235.0,28.2')] ).
cnf(12306,plain,
( ~ aScalar0(u)
| ~ aScalar0(u)
| ~ aScalar0(sdtasdt0(v,v))
| ~ aScalar0(v)
| ~ aScalar0(u)
| sdtlseqdt0(sz0z00,sdtasdt0(sdtasdt0(v,v),sdtasdt0(u,u))) ),
inference(spr,[status(thm),theory(equality)],[1291,12236]),
[iquote('0:SpR:1291.3,12236.2')] ).
cnf(12334,plain,
( ~ aScalar0(sdtasdt0(u,u))
| ~ aScalar0(u)
| ~ aScalar0(v)
| sdtlseqdt0(sz0z00,sdtasdt0(sdtasdt0(u,u),sdtasdt0(v,v))) ),
inference(obv,[status(thm),theory(equality)],[12306]),
[iquote('0:Obv:12306.1')] ).
cnf(12335,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| sdtlseqdt0(sz0z00,sdtasdt0(sdtasdt0(u,u),sdtasdt0(v,v))) ),
inference(ssi,[status(thm)],[12334,28]),
[iquote('0:SSi:12334.0,28.2')] ).
cnf(12379,plain,
( ~ aScalar0(u)
| ~ aScalar0(sz0z00)
| sdtlseqdt0(sz0z00,sdtasdt0(sdtasdt0(u,u),sz0z00)) ),
inference(spr,[status(thm),theory(equality)],[6381,12335]),
[iquote('0:SpR:6381.0,12335.2')] ).
cnf(12405,plain,
( ~ aScalar0(u)
| sdtlseqdt0(sz0z00,sdtasdt0(sdtasdt0(u,u),sz0z00)) ),
inference(ssi,[status(thm)],[12379,2]),
[iquote('0:SSi:12379.1,2.0')] ).
cnf(12476,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(sdtasdt0(sdtasdt0(u,u),sz0z00))
| ~ aScalar0(sz0z00)
| sdtlseqdt0(v,sdtasdt0(sdtasdt0(u,u),sz0z00))
| sdtlseqdt0(sz0z00,v) ),
inference(res,[status(thm),theory(equality)],[12405,1528]),
[iquote('0:Res:12405.1,1528.3')] ).
cnf(12490,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| sdtlseqdt0(v,sdtasdt0(sdtasdt0(u,u),sz0z00))
| sdtlseqdt0(sz0z00,v) ),
inference(ssi,[status(thm)],[12476,2,28]),
[iquote('0:SSi:12476.3,12476.2,2.0,28.2,28.2,2.0')] ).
cnf(13167,plain,
( ~ aScalar0(u)
| ~ aScalar0(u)
| ~ aScalar0(u)
| ~ aScalar0(v)
| sdtlseqdt0(v,sz0z00)
| sdtlseqdt0(sz0z00,v) ),
inference(spr,[status(thm),theory(equality)],[6866,12490]),
[iquote('0:SpR:6866.2,12490.2')] ).
cnf(13177,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| sdtlseqdt0(v,sz0z00)
| sdtlseqdt0(sz0z00,v) ),
inference(obv,[status(thm),theory(equality)],[13167]),
[iquote('0:Obv:13167.1')] ).
cnf(13178,plain,
( ~ aScalar0(u)
| sdtlseqdt0(u,sz0z00)
| sdtlseqdt0(sz0z00,u) ),
inference(con,[status(thm)],[13177]),
[iquote('0:Con:13177.0')] ).
cnf(15524,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(u)
| ~ aScalar0(u)
| ~ sdtlseqdt0(sz0z00,v)
| sdtlseqdt0(sz0z00,sdtasdt0(u,v)) ),
inference(res,[status(thm),theory(equality)],[12,9460]),
[iquote('0:Res:12.1,9460.3')] ).
cnf(15553,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ sdtlseqdt0(sz0z00,u)
| sdtlseqdt0(sz0z00,sdtasdt0(v,u)) ),
inference(obv,[status(thm),theory(equality)],[15524]),
[iquote('0:Obv:15524.2')] ).
cnf(15587,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(v)
| ~ aScalar0(u)
| ~ sdtlseqdt0(sz0z00,v)
| sdtlseqdt0(sz0z00,sdtasdt0(v,u)) ),
inference(spr,[status(thm),theory(equality)],[36,15553]),
[iquote('0:SpR:36.2,15553.3')] ).
cnf(15617,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ sdtlseqdt0(sz0z00,u)
| sdtlseqdt0(sz0z00,sdtasdt0(u,v)) ),
inference(obv,[status(thm),theory(equality)],[15587]),
[iquote('0:Obv:15587.1')] ).
cnf(15653,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(u))
| ~ sdtlseqdt0(sz0z00,v)
| sdtlseqdt0(sz0z00,smndt0(sdtasdt0(v,u))) ),
inference(spr,[status(thm),theory(equality)],[40,15617]),
[iquote('0:SpR:40.2,15617.3')] ).
cnf(15676,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(sdtasdt0(u,v))
| ~ aScalar0(sz0z00)
| ~ sdtlseqdt0(sz0z00,u)
| ~ sdtlseqdt0(sdtasdt0(u,v),sz0z00)
| equal(sdtasdt0(u,v),sz0z00) ),
inference(res,[status(thm),theory(equality)],[15617,44]),
[iquote('0:Res:15617.3,44.2')] ).
cnf(15681,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(smndt0(u))
| ~ sdtlseqdt0(sz0z00,v)
| sdtlseqdt0(sz0z00,smndt0(sdtasdt0(v,u))) ),
inference(obv,[status(thm),theory(equality)],[15653]),
[iquote('0:Obv:15653.1')] ).
cnf(15682,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ sdtlseqdt0(sz0z00,v)
| sdtlseqdt0(sz0z00,smndt0(sdtasdt0(v,u))) ),
inference(ssi,[status(thm)],[15681,11]),
[iquote('0:SSi:15681.2,11.1')] ).
cnf(15694,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ sdtlseqdt0(sz0z00,u)
| ~ sdtlseqdt0(sdtasdt0(u,v),sz0z00)
| equal(sdtasdt0(u,v),sz0z00) ),
inference(ssi,[status(thm)],[15676,2,28]),
[iquote('0:SSi:15676.3,15676.2,2.2,28.0')] ).
cnf(20387,plain,
( ~ aScalar0(u)
| ~ aScalar0(sdtasasdt0(xs,xs))
| ~ aScalar0(v)
| ~ aScalar0(sdtpldt0(v,u))
| ~ sdtlseqdt0(v,sdtasasdt0(xs,xs))
| ~ sdtlseqdt0(u,sz0z00)
| ~ sdtlseqdt0(sz0z00,sdtpldt0(v,u)) ),
inference(res,[status(thm),theory(equality)],[3349,7731]),
[iquote('0:Res:3349.5,7731.1')] ).
cnf(20399,plain,
( ~ aScalar0(u)
| ~ aScalar0(sdtasasdt0(xs,xs))
| ~ aScalar0(v)
| ~ sdtlseqdt0(v,sdtasasdt0(xs,xs))
| ~ sdtlseqdt0(u,sz0z00)
| ~ sdtlseqdt0(sz0z00,sdtpldt0(v,u)) ),
inference(ssi,[status(thm)],[20387,27]),
[iquote('0:SSi:20387.3,27.2')] ).
cnf(22728,plain,
( ~ aScalar0(smndt0(u))
| ~ aScalar0(smndt0(u))
| ~ aScalar0(v)
| ~ aScalar0(u)
| ~ sdtlseqdt0(u,v)
| sdtlseqdt0(sz0z00,sdtpldt0(v,smndt0(u))) ),
inference(res,[status(thm),theory(equality)],[12,3353]),
[iquote('0:Res:12.1,3353.4')] ).
cnf(22753,plain,
( ~ aScalar0(smndt0(u))
| ~ aScalar0(v)
| ~ aScalar0(u)
| ~ sdtlseqdt0(u,v)
| sdtlseqdt0(sz0z00,sdtpldt0(v,smndt0(u))) ),
inference(obv,[status(thm),theory(equality)],[22728]),
[iquote('0:Obv:22728.0')] ).
cnf(22754,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ sdtlseqdt0(v,u)
| sdtlseqdt0(sz0z00,sdtpldt0(u,smndt0(v))) ),
inference(ssi,[status(thm)],[22753,11]),
[iquote('0:SSi:22753.0,11.1')] ).
cnf(22823,plain,
( ~ aScalar0(u)
| ~ aScalar0(sz0z00)
| ~ aScalar0(u)
| ~ sdtlseqdt0(u,sz0z00)
| sdtlseqdt0(sz0z00,smndt0(u)) ),
inference(spr,[status(thm),theory(equality)],[1773,22754]),
[iquote('0:SpR:1773.1,22754.3')] ).
cnf(22834,plain,
( ~ aScalar0(sz0z00)
| ~ aScalar0(u)
| ~ sdtlseqdt0(u,sz0z00)
| sdtlseqdt0(sz0z00,smndt0(u)) ),
inference(obv,[status(thm),theory(equality)],[22823]),
[iquote('0:Obv:22823.0')] ).
cnf(22835,plain,
( ~ aScalar0(u)
| ~ sdtlseqdt0(u,sz0z00)
| sdtlseqdt0(sz0z00,smndt0(u)) ),
inference(ssi,[status(thm)],[22834,2]),
[iquote('0:SSi:22834.0,2.0')] ).
cnf(22879,plain,
( ~ aScalar0(u)
| ~ aScalar0(smndt0(u))
| ~ sdtlseqdt0(smndt0(u),sz0z00)
| sdtlseqdt0(sz0z00,u) ),
inference(spr,[status(thm),theory(equality)],[23,22835]),
[iquote('0:SpR:23.1,22835.2')] ).
cnf(22891,plain,
( ~ aScalar0(u)
| ~ aScalar0(smndt0(u))
| ~ aScalar0(sz0z00)
| ~ sdtlseqdt0(u,sz0z00)
| ~ sdtlseqdt0(smndt0(u),sz0z00)
| equal(smndt0(u),sz0z00) ),
inference(res,[status(thm),theory(equality)],[22835,44]),
[iquote('0:Res:22835.2,44.2')] ).
cnf(22893,plain,
( ~ aScalar0(u)
| ~ sdtlseqdt0(smndt0(u),sz0z00)
| sdtlseqdt0(sz0z00,u) ),
inference(ssi,[status(thm)],[22879,11]),
[iquote('0:SSi:22879.1,11.1')] ).
cnf(22894,plain,
( ~ aScalar0(u)
| ~ sdtlseqdt0(u,sz0z00)
| ~ sdtlseqdt0(smndt0(u),sz0z00)
| equal(smndt0(u),sz0z00) ),
inference(ssi,[status(thm)],[22891,2,11]),
[iquote('0:SSi:22891.2,22891.1,2.1,11.0')] ).
cnf(22920,plain,
( ~ aScalar0(smndt0(u))
| ~ aScalar0(u)
| sdtlseqdt0(sz0z00,smndt0(u))
| sdtlseqdt0(sz0z00,u) ),
inference(res,[status(thm),theory(equality)],[13178,22893]),
[iquote('0:Res:13178.1,22893.1')] ).
cnf(22922,plain,
( ~ aScalar0(u)
| sdtlseqdt0(sz0z00,smndt0(u))
| sdtlseqdt0(sz0z00,u) ),
inference(ssi,[status(thm)],[22920,11]),
[iquote('0:SSi:22920.0,11.1')] ).
cnf(23332,plain,
( ~ aScalar0(smndt0(u))
| ~ aScalar0(smndt0(u))
| ~ aScalar0(u)
| ~ aScalar0(v)
| ~ sdtlseqdt0(v,u)
| sdtlseqdt0(sdtpldt0(v,smndt0(u)),sz0z00) ),
inference(res,[status(thm),theory(equality)],[12,3357]),
[iquote('0:Res:12.1,3357.4')] ).
cnf(23349,plain,
( ~ aScalar0(smndt0(u))
| ~ aScalar0(u)
| ~ aScalar0(v)
| ~ sdtlseqdt0(v,u)
| sdtlseqdt0(sdtpldt0(v,smndt0(u)),sz0z00) ),
inference(obv,[status(thm),theory(equality)],[23332]),
[iquote('0:Obv:23332.0')] ).
cnf(23350,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ sdtlseqdt0(v,u)
| sdtlseqdt0(sdtpldt0(v,smndt0(u)),sz0z00) ),
inference(ssi,[status(thm)],[23349,11]),
[iquote('0:SSi:23349.0,11.1')] ).
cnf(27448,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(u)
| ~ aScalar0(sdtpldt0(v,u))
| ~ sdtlseqdt0(sdtpldt0(v,u),u)
| sdtlseqdt0(v,sz0z00) ),
inference(spr,[status(thm),theory(equality)],[2277,23350]),
[iquote('0:SpR:2277.2,23350.3')] ).
cnf(27455,plain,
( ~ aScalar0(u)
| ~ aScalar0(u)
| ~ aScalar0(sz0z00)
| ~ sdtlseqdt0(sz0z00,u)
| sdtlseqdt0(smndt0(u),sz0z00) ),
inference(spr,[status(thm),theory(equality)],[1773,23350]),
[iquote('0:SpR:1773.1,23350.3')] ).
cnf(27467,plain,
( ~ aScalar0(u)
| ~ aScalar0(sz0z00)
| ~ sdtlseqdt0(sz0z00,u)
| sdtlseqdt0(smndt0(u),sz0z00) ),
inference(obv,[status(thm),theory(equality)],[27455]),
[iquote('0:Obv:27455.0')] ).
cnf(27468,plain,
( ~ aScalar0(u)
| ~ sdtlseqdt0(sz0z00,u)
| sdtlseqdt0(smndt0(u),sz0z00) ),
inference(ssi,[status(thm)],[27467,2]),
[iquote('0:SSi:27467.1,2.0')] ).
cnf(27472,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(sdtpldt0(u,v))
| ~ sdtlseqdt0(sdtpldt0(u,v),v)
| sdtlseqdt0(u,sz0z00) ),
inference(obv,[status(thm),theory(equality)],[27448]),
[iquote('0:Obv:27448.0')] ).
cnf(27473,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ sdtlseqdt0(sdtpldt0(u,v),v)
| sdtlseqdt0(u,sz0z00) ),
inference(ssi,[status(thm)],[27472,27]),
[iquote('0:SSi:27472.2,27.2')] ).
cnf(27511,plain,
( ~ aScalar0(u)
| ~ aScalar0(smndt0(u))
| ~ sdtlseqdt0(sz0z00,smndt0(u))
| sdtlseqdt0(u,sz0z00) ),
inference(spr,[status(thm),theory(equality)],[23,27468]),
[iquote('0:SpR:23.1,27468.2')] ).
cnf(27527,plain,
( ~ aScalar0(u)
| ~ aScalar0(u)
| ~ sdtlseqdt0(sz0z00,u)
| ~ sdtlseqdt0(u,sz0z00)
| equal(smndt0(u),sz0z00) ),
inference(res,[status(thm),theory(equality)],[27468,22894]),
[iquote('0:Res:27468.2,22894.2')] ).
cnf(27532,plain,
( ~ aScalar0(u)
| ~ sdtlseqdt0(sz0z00,smndt0(u))
| sdtlseqdt0(u,sz0z00) ),
inference(ssi,[status(thm)],[27511,11]),
[iquote('0:SSi:27511.1,11.1')] ).
cnf(27534,plain,
( ~ aScalar0(u)
| ~ sdtlseqdt0(sz0z00,u)
| ~ sdtlseqdt0(u,sz0z00)
| equal(smndt0(u),sz0z00) ),
inference(obv,[status(thm),theory(equality)],[27527]),
[iquote('0:Obv:27527.0')] ).
cnf(27575,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(sdtasdt0(v,u))
| ~ sdtlseqdt0(sz0z00,v)
| sdtlseqdt0(sdtasdt0(v,u),sz0z00) ),
inference(res,[status(thm),theory(equality)],[15682,27532]),
[iquote('0:Res:15682.3,27532.1')] ).
cnf(27593,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ sdtlseqdt0(sz0z00,v)
| sdtlseqdt0(sdtasdt0(v,u),sz0z00) ),
inference(ssi,[status(thm)],[27575,28]),
[iquote('0:SSi:27575.2,28.2')] ).
cnf(27594,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ sdtlseqdt0(sz0z00,u)
| equal(sdtasdt0(u,v),sz0z00) ),
inference(mrr,[status(thm)],[15694,27593]),
[iquote('0:MRR:15694.3,27593.3')] ).
cnf(28444,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ aScalar0(u)
| ~ sdtlseqdt0(sz0z00,u)
| ~ sdtlseqdt0(u,sz0z00)
| equal(sdtpldt0(sz0z00,sdtpldt0(v,u)),v) ),
inference(spr,[status(thm),theory(equality)],[27534,1125]),
[iquote('0:SpR:27534.3,1125.2')] ).
cnf(28592,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ sdtlseqdt0(sz0z00,v)
| ~ sdtlseqdt0(v,sz0z00)
| equal(sdtpldt0(sz0z00,sdtpldt0(u,v)),u) ),
inference(obv,[status(thm),theory(equality)],[28444]),
[iquote('0:Obv:28444.0')] ).
cnf(28593,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ sdtlseqdt0(sz0z00,v)
| ~ sdtlseqdt0(v,sz0z00)
| equal(sdtpldt0(u,v),u) ),
inference(rew,[status(thm),theory(equality)],[1039,28592]),
[iquote('0:Rew:1039.2,28592.4')] ).
cnf(29023,plain,
( ~ aScalar0(u)
| ~ aScalar0(u)
| ~ aScalar0(u)
| ~ sdtlseqdt0(sz0z00,u)
| ~ sdtlseqdt0(sz0z00,sz0z00)
| equal(sdtasdt0(u,u),sz0z00) ),
inference(spl,[status(thm),theory(equality)],[27594,593]),
[iquote('0:SpL:27594.3,593.1')] ).
cnf(29097,plain,
( ~ aScalar0(u)
| ~ sdtlseqdt0(sz0z00,u)
| ~ sdtlseqdt0(sz0z00,sz0z00)
| equal(sdtasdt0(u,u),sz0z00) ),
inference(obv,[status(thm),theory(equality)],[29023]),
[iquote('0:Obv:29023.1')] ).
cnf(29098,plain,
( ~ aScalar0(u)
| ~ sdtlseqdt0(sz0z00,u)
| equal(sdtasdt0(u,u),sz0z00) ),
inference(mrr,[status(thm)],[29097,9655]),
[iquote('0:MRR:29097.2,9655.0')] ).
cnf(29100,plain,
( ~ aScalar0(u)
| ~ sdtlseqdt0(sz0z00,u)
| ~ equal(sz0z00,sz0z00)
| equal(u,sz0z00) ),
inference(rew,[status(thm),theory(equality)],[29098,9458]),
[iquote('0:Rew:29098.2,9458.2')] ).
cnf(29107,plain,
( ~ aScalar0(u)
| ~ sdtlseqdt0(sz0z00,u)
| equal(u,sz0z00) ),
inference(obv,[status(thm),theory(equality)],[29100]),
[iquote('0:Obv:29100.2')] ).
cnf(29513,plain,
( ~ aScalar0(u)
| ~ aScalar0(sdtasdt0(u,u))
| equal(sdtasdt0(u,u),sz0z00) ),
inference(res,[status(thm),theory(equality)],[24,29107]),
[iquote('0:Res:24.1,29107.1')] ).
cnf(29555,plain,
( ~ aScalar0(u)
| ~ aScalar0(smndt0(u))
| sdtlseqdt0(sz0z00,u)
| equal(smndt0(u),sz0z00) ),
inference(res,[status(thm),theory(equality)],[22922,29107]),
[iquote('0:Res:22922.1,29107.1')] ).
cnf(29622,plain,
( ~ aScalar0(u)
| equal(sdtasdt0(u,u),sz0z00) ),
inference(ssi,[status(thm)],[29513,28]),
[iquote('0:SSi:29513.1,28.2')] ).
cnf(29752,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ sdtlseqdt0(sz0z00,sdtpldt0(v,u))
| ~ equal(sdtpldt0(sdtpldt0(sz0z00,sdtasdt0(v,u)),sdtpldt0(sdtasdt0(u,v),sdtasdt0(u,u))),sz0z00)
| equal(sdtpldt0(v,u),sz0z00) ),
inference(rew,[status(thm),theory(equality)],[29622,9788]),
[iquote('0:Rew:29622.1,9788.3')] ).
cnf(30078,plain,
( ~ aScalar0(u)
| sdtlseqdt0(sz0z00,u)
| equal(smndt0(u),sz0z00) ),
inference(ssi,[status(thm)],[29555,11]),
[iquote('0:SSi:29555.1,11.1')] ).
cnf(30084,plain,
( ~ aScalar0(u)
| ~ sdtlseqdt0(sz0z00,sz0z00)
| sdtlseqdt0(sz0z00,u) ),
inference(rew,[status(thm),theory(equality)],[30078,22893]),
[iquote('0:Rew:30078.2,22893.1')] ).
cnf(30114,plain,
( ~ aScalar0(u)
| sdtlseqdt0(sz0z00,u) ),
inference(mrr,[status(thm)],[30084,9655]),
[iquote('0:MRR:30084.1,9655.0')] ).
cnf(30115,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ sdtlseqdt0(sz0z00,u)
| sdtlseqdt0(sz0z00,sdtpldt0(v,u)) ),
inference(mrr,[status(thm)],[46,30114]),
[iquote('0:MRR:46.2,30114.1')] ).
cnf(30123,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtasdt0(u,v),sz0z00) ),
inference(mrr,[status(thm)],[27594,30114]),
[iquote('0:MRR:27594.2,30114.1')] ).
cnf(30124,plain,
( ~ aScalar0(u)
| equal(u,sz0z00) ),
inference(mrr,[status(thm)],[29107,30114]),
[iquote('0:MRR:29107.1,30114.1')] ).
cnf(30156,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ sdtlseqdt0(v,sz0z00)
| equal(sdtpldt0(u,v),u) ),
inference(mrr,[status(thm)],[28593,30114]),
[iquote('0:MRR:28593.2,30114.1')] ).
cnf(30247,plain,
( ~ aScalar0(u)
| ~ aScalar0(sdtasasdt0(xs,xs))
| ~ aScalar0(v)
| ~ sdtlseqdt0(v,sz0z00)
| ~ sdtlseqdt0(u,sz0z00)
| ~ sdtlseqdt0(sz0z00,sdtpldt0(v,u)) ),
inference(rew,[status(thm),theory(equality)],[30124,20399]),
[iquote('0:Rew:30124.1,20399.3')] ).
cnf(31419,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| sdtlseqdt0(sz0z00,sdtpldt0(v,u)) ),
inference(mrr,[status(thm)],[30115,30114]),
[iquote('0:MRR:30115.2,30114.1')] ).
cnf(33677,plain,
( ~ aScalar0(u)
| ~ aScalar0(sdtasasdt0(xs,xs))
| ~ aScalar0(v)
| ~ sdtlseqdt0(v,sz0z00)
| ~ sdtlseqdt0(u,sz0z00)
| ~ sdtlseqdt0(sz0z00,v) ),
inference(rew,[status(thm),theory(equality)],[30156,30247]),
[iquote('0:Rew:30156.3,30247.5')] ).
cnf(33678,plain,
( ~ aScalar0(sdtasasdt0(xs,xs))
| ~ aScalar0(u)
| ~ sdtlseqdt0(u,sz0z00)
| ~ sdtlseqdt0(sz0z00,u) ),
inference(con,[status(thm)],[33677]),
[iquote('0:Con:33677.0')] ).
cnf(33679,plain,
( ~ aScalar0(sdtasasdt0(xs,xs))
| ~ aScalar0(u)
| ~ sdtlseqdt0(u,sz0z00) ),
inference(mrr,[status(thm)],[33678,30114]),
[iquote('0:MRR:33678.3,30114.1')] ).
cnf(34626,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ sdtlseqdt0(sz0z00,sdtpldt0(v,u))
| ~ equal(sdtpldt0(sdtpldt0(sz0z00,sz0z00),sdtpldt0(sz0z00,sz0z00)),sz0z00)
| equal(sdtpldt0(v,u),sz0z00) ),
inference(rew,[status(thm),theory(equality)],[30123,29752,29622]),
[iquote('0:Rew:30123.2,29752.3,30123.2,29752.3,29622.1,29752.3')] ).
cnf(34627,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ sdtlseqdt0(sz0z00,sdtpldt0(v,u))
| ~ equal(sz0z00,sz0z00)
| equal(sdtpldt0(v,u),sz0z00) ),
inference(rew,[status(thm),theory(equality)],[1545,34626]),
[iquote('0:Rew:1545.0,34626.3,1545.0,34626.3')] ).
cnf(34628,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ sdtlseqdt0(sz0z00,sdtpldt0(v,u))
| equal(sdtpldt0(v,u),sz0z00) ),
inference(obv,[status(thm),theory(equality)],[34627]),
[iquote('0:Obv:34627.3')] ).
cnf(34629,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| equal(sdtpldt0(v,u),sz0z00) ),
inference(mrr,[status(thm)],[34628,31419]),
[iquote('0:MRR:34628.2,31419.2')] ).
cnf(34872,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| ~ sdtlseqdt0(sz0z00,v)
| sdtlseqdt0(u,sz0z00) ),
inference(rew,[status(thm),theory(equality)],[34629,27473]),
[iquote('0:Rew:34629.2,27473.2')] ).
cnf(35053,plain,
( ~ aScalar0(u)
| ~ aScalar0(v)
| sdtlseqdt0(u,sz0z00) ),
inference(mrr,[status(thm)],[34872,30114]),
[iquote('0:MRR:34872.2,30114.1')] ).
cnf(35056,plain,
( ~ aScalar0(sdtasasdt0(xs,xs))
| ~ aScalar0(u) ),
inference(mrr,[status(thm)],[33679,35053]),
[iquote('0:MRR:33679.2,35053.2')] ).
cnf(35062,plain,
~ aScalar0(sdtasasdt0(xs,xs)),
inference(con,[status(thm)],[35056]),
[iquote('0:Con:35056.1')] ).
cnf(37307,plain,
( ~ aVector0(xs)
| ~ aVector0(xs)
| ~ equal(aDimensionOf0(xs),aDimensionOf0(xs)) ),
inference(sor,[status(thm)],[35062,43]),
[iquote('0:SoR:35062.0,43.3')] ).
cnf(37308,plain,
~ aVector0(xs),
inference(obv,[status(thm),theory(equality)],[37307]),
[iquote('0:Obv:37307.2')] ).
cnf(37309,plain,
$false,
inference(ssi,[status(thm)],[37308,3]),
[iquote('0:SSi:37308.0,3.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : RNG049+2 : TPTP v8.1.0. Released v4.0.0.
% 0.11/0.13 % Command : run_spass %d %s
% 0.14/0.33 % Computer : n025.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 600
% 0.14/0.34 % DateTime : Mon May 30 10:18:27 EDT 2022
% 0.14/0.34 % CPUTime :
% 32.74/32.94
% 32.74/32.94 SPASS V 3.9
% 32.74/32.94 SPASS beiseite: Proof found.
% 32.74/32.94 % SZS status Theorem
% 32.74/32.94 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 32.74/32.94 SPASS derived 16365 clauses, backtracked 0 clauses, performed 2 splits and kept 3091 clauses.
% 32.74/32.94 SPASS allocated 135030 KBytes.
% 32.74/32.94 SPASS spent 0:0:32.56 on the problem.
% 32.74/32.94 0:00:00.03 for the input.
% 32.74/32.94 0:00:00.04 for the FLOTTER CNF translation.
% 32.74/32.94 0:00:00.16 for inferences.
% 32.74/32.94 0:00:00.00 for the backtracking.
% 32.74/32.94 0:0:32.27 for the reduction.
% 32.74/32.94
% 32.74/32.94
% 32.74/32.94 Here is a proof with depth 13, length 265 :
% 32.74/32.94 % SZS output start Refutation
% See solution above
% 57.14/57.33 Formulae used in the proof : mSZeroSc m__1542 m__ mNegSc mLERef mScZero mSqPos mSumSc mMulSc mLETot mArith mMNeg mScPr mLEASm mPosMon mLETrn mDistr mSqrt mLEMon mLEMonM mDistr2
% 57.14/57.33
%------------------------------------------------------------------------------