%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV555-1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:25:45 PM UTC 2026
% Result : Unsatisfiable 192.40s 27.48s
% Output : Refutation 192.40s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : select(store(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1) ).
fof(f2,axiom,
! [X2,X3,X0,X1] :
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2) ).
fof(f3,axiom,
a_44 = store(a1,i1,e_43),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp0) ).
fof(f4,axiom,
a_46 = store(a2,i1,e_45),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp1) ).
fof(f5,axiom,
a_48 = store(a_44,i2,e_47),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp2) ).
fof(f6,axiom,
a_50 = store(a_46,i2,e_49),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp3) ).
fof(f7,axiom,
a_52 = store(a_48,i3,e_51),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp4) ).
fof(f8,axiom,
a_54 = store(a_50,i3,e_53),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp5) ).
fof(f9,axiom,
a_56 = store(a_52,i4,e_55),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp6) ).
fof(f10,axiom,
a_58 = store(a_54,i4,e_57),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp7) ).
fof(f11,axiom,
a_60 = store(a_56,i5,e_59),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp8) ).
fof(f12,axiom,
a_62 = store(a_58,i5,e_61),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp9) ).
fof(f13,axiom,
a_64 = store(a_60,i6,e_63),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp10) ).
fof(f14,axiom,
a_66 = store(a_62,i6,e_65),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp11) ).
fof(f15,axiom,
a_68 = store(a_64,i7,e_67),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp12) ).
fof(f16,axiom,
a_70 = store(a_66,i7,e_69),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp13) ).
fof(f17,axiom,
a_72 = store(a_68,i8,e_71),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp14) ).
fof(f18,axiom,
a_74 = store(a_70,i8,e_73),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp15) ).
fof(f19,axiom,
a_76 = store(a_72,i9,e_75),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp16) ).
fof(f20,axiom,
a_78 = store(a_74,i9,e_77),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp17) ).
fof(f21,axiom,
a_80 = store(a_76,i10,e_79),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp18) ).
fof(f22,axiom,
a_82 = store(a_78,i10,e_81),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp19) ).
fof(f23,axiom,
e_43 = select(a2,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp20) ).
fof(f24,axiom,
e_45 = select(a1,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp21) ).
fof(f25,axiom,
e_47 = select(a_46,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp22) ).
fof(f26,axiom,
e_49 = select(a_44,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp23) ).
fof(f27,axiom,
e_51 = select(a_50,i3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp24) ).
fof(f28,axiom,
e_53 = select(a_48,i3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp25) ).
fof(f29,axiom,
e_55 = select(a_54,i4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp26) ).
fof(f30,axiom,
e_57 = select(a_52,i4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp27) ).
fof(f31,axiom,
e_59 = select(a_58,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp28) ).
fof(f32,axiom,
e_61 = select(a_56,i5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp29) ).
fof(f33,axiom,
e_63 = select(a_62,i6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp30) ).
fof(f34,axiom,
e_65 = select(a_60,i6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp31) ).
fof(f35,axiom,
e_67 = select(a_66,i7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp32) ).
fof(f36,axiom,
e_69 = select(a_64,i7),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp33) ).
fof(f37,axiom,
e_71 = select(a_70,i8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp34) ).
fof(f38,axiom,
e_73 = select(a_68,i8),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp35) ).
fof(f39,axiom,
e_75 = select(a_74,i9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp36) ).
fof(f40,axiom,
e_77 = select(a_72,i9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp37) ).
fof(f41,axiom,
e_79 = select(a_78,i10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp38) ).
fof(f42,axiom,
e_81 = select(a_76,i10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp39) ).
fof(f43,axiom,
e_84 = select(a1,i_83),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp40) ).
fof(f44,axiom,
e_85 = select(a2,i_83),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp41) ).
fof(f46,axiom,
a_80 = a_82,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp43) ).
fof(f47,negated_conjecture,
e_84 != e_85,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f48,plain,
store(a_76,i10,e_79) = a_82,
inference(definition_unfolding,[],[f21,f46]) ).
fof(f49,plain,
e_43 = select(a_44,i1),
inference(superposition,[],[f1,f3]) ).
fof(f50,plain,
e_45 = select(a_46,i1),
inference(superposition,[],[f1,f4]) ).
fof(f51,plain,
e_47 = select(a_48,i2),
inference(superposition,[],[f1,f5]) ).
fof(f52,plain,
e_49 = select(a_50,i2),
inference(superposition,[],[f1,f6]) ).
fof(f53,plain,
e_51 = select(a_52,i3),
inference(superposition,[],[f1,f7]) ).
fof(f54,plain,
e_53 = select(a_54,i3),
inference(superposition,[],[f1,f8]) ).
fof(f55,plain,
e_55 = select(a_56,i4),
inference(superposition,[],[f1,f9]) ).
fof(f56,plain,
e_57 = select(a_58,i4),
inference(superposition,[],[f1,f10]) ).
fof(f57,plain,
e_59 = select(a_60,i5),
inference(superposition,[],[f1,f11]) ).
fof(f58,plain,
e_61 = select(a_62,i5),
inference(superposition,[],[f1,f12]) ).
fof(f59,plain,
e_63 = select(a_64,i6),
inference(superposition,[],[f1,f13]) ).
fof(f60,plain,
e_65 = select(a_66,i6),
inference(superposition,[],[f1,f14]) ).
fof(f61,plain,
e_67 = select(a_68,i7),
inference(superposition,[],[f1,f15]) ).
fof(f62,plain,
e_69 = select(a_70,i7),
inference(superposition,[],[f1,f16]) ).
fof(f63,plain,
e_71 = select(a_72,i8),
inference(superposition,[],[f1,f17]) ).
fof(f64,plain,
e_73 = select(a_74,i8),
inference(superposition,[],[f1,f18]) ).
fof(f65,plain,
e_75 = select(a_76,i9),
inference(superposition,[],[f1,f19]) ).
fof(f66,plain,
e_77 = select(a_78,i9),
inference(superposition,[],[f1,f20]) ).
fof(f67,plain,
e_81 = select(a_82,i10),
inference(superposition,[],[f1,f22]) ).
fof(f68,plain,
e_79 = select(a_82,i10),
inference(superposition,[],[f1,f48]) ).
fof(f69,plain,
e_79 = e_81,
inference(forward_demodulation,[],[f67,f68]) ).
fof(f70,plain,
! [X0] :
( select(a1,X0) = select(a_44,X0)
| i1 = X0 ),
inference(superposition,[],[f2,f3]) ).
fof(f71,plain,
! [X0] :
( select(a2,X0) = select(a_46,X0)
| i1 = X0 ),
inference(superposition,[],[f2,f4]) ).
fof(f72,plain,
! [X0] :
( select(a_44,X0) = select(a_48,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f5]) ).
fof(f73,plain,
! [X0] :
( select(a_46,X0) = select(a_50,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f6]) ).
fof(f74,plain,
! [X0] :
( select(a_48,X0) = select(a_52,X0)
| i3 = X0 ),
inference(superposition,[],[f2,f7]) ).
fof(f75,plain,
! [X0] :
( select(a_50,X0) = select(a_54,X0)
| i3 = X0 ),
inference(superposition,[],[f2,f8]) ).
fof(f76,plain,
! [X0] :
( select(a_52,X0) = select(a_56,X0)
| i4 = X0 ),
inference(superposition,[],[f2,f9]) ).
fof(f77,plain,
! [X0] :
( select(a_54,X0) = select(a_58,X0)
| i4 = X0 ),
inference(superposition,[],[f2,f10]) ).
fof(f78,plain,
! [X0] :
( select(a_56,X0) = select(a_60,X0)
| i5 = X0 ),
inference(superposition,[],[f2,f11]) ).
fof(f79,plain,
! [X0] :
( select(a_58,X0) = select(a_62,X0)
| i5 = X0 ),
inference(superposition,[],[f2,f12]) ).
fof(f80,plain,
! [X0] :
( select(a_60,X0) = select(a_64,X0)
| i6 = X0 ),
inference(superposition,[],[f2,f13]) ).
fof(f81,plain,
! [X0] :
( select(a_62,X0) = select(a_66,X0)
| i6 = X0 ),
inference(superposition,[],[f2,f14]) ).
fof(f82,plain,
! [X0] :
( select(a_64,X0) = select(a_68,X0)
| i7 = X0 ),
inference(superposition,[],[f2,f15]) ).
fof(f83,plain,
! [X0] :
( select(a_66,X0) = select(a_70,X0)
| i7 = X0 ),
inference(superposition,[],[f2,f16]) ).
fof(f84,plain,
! [X0] :
( select(a_68,X0) = select(a_72,X0)
| i8 = X0 ),
inference(superposition,[],[f2,f17]) ).
fof(f85,plain,
! [X0] :
( select(a_70,X0) = select(a_74,X0)
| i8 = X0 ),
inference(superposition,[],[f2,f18]) ).
fof(f86,plain,
! [X0] :
( select(a_72,X0) = select(a_76,X0)
| i9 = X0 ),
inference(superposition,[],[f2,f19]) ).
fof(f87,plain,
! [X0] :
( select(a_74,X0) = select(a_78,X0)
| i9 = X0 ),
inference(superposition,[],[f2,f20]) ).
fof(f88,plain,
! [X0] :
( select(a_78,X0) = select(a_82,X0)
| i10 = X0 ),
inference(superposition,[],[f2,f22]) ).
fof(f89,plain,
! [X0] :
( select(a_76,X0) = select(a_82,X0)
| i10 = X0 ),
inference(superposition,[],[f2,f48]) ).
fof(f94,plain,
( e_84 = select(a_44,i_83)
| i1 = i_83 ),
inference(superposition,[],[f43,f70]) ).
fof(f96,plain,
( e_85 = select(a_46,i_83)
| i1 = i_83 ),
inference(superposition,[],[f44,f71]) ).
fof(f98,plain,
( e_53 = select(a_44,i3)
| i2 = i3 ),
inference(superposition,[],[f28,f72]) ).
fof(f100,plain,
( e_51 = select(a_46,i3)
| i2 = i3 ),
inference(superposition,[],[f27,f73]) ).
fof(f102,plain,
( e_57 = select(a_48,i4)
| i3 = i4 ),
inference(superposition,[],[f30,f74]) ).
fof(f104,plain,
( e_57 = select(a_44,i4)
| i2 = i4
| i3 = i4 ),
inference(superposition,[],[f72,f102]) ).
fof(f106,plain,
( e_55 = select(a_50,i4)
| i3 = i4 ),
inference(superposition,[],[f29,f75]) ).
fof(f108,plain,
( e_55 = select(a_46,i4)
| i2 = i4
| i3 = i4 ),
inference(superposition,[],[f73,f106]) ).
fof(f110,plain,
( e_61 = select(a_52,i5)
| i4 = i5 ),
inference(superposition,[],[f32,f76]) ).
fof(f112,plain,
( e_61 = select(a_48,i5)
| i3 = i5
| i4 = i5 ),
inference(superposition,[],[f74,f110]) ).
fof(f114,plain,
( e_59 = select(a_54,i5)
| i4 = i5 ),
inference(superposition,[],[f31,f77]) ).
fof(f116,plain,
( e_59 = select(a_50,i5)
| i3 = i5
| i4 = i5 ),
inference(superposition,[],[f75,f114]) ).
fof(f118,plain,
( e_65 = select(a_56,i6)
| i5 = i6 ),
inference(superposition,[],[f34,f78]) ).
fof(f120,plain,
( e_65 = select(a_52,i6)
| i4 = i6
| i5 = i6 ),
inference(superposition,[],[f76,f118]) ).
fof(f122,plain,
( e_63 = select(a_58,i6)
| i5 = i6 ),
inference(superposition,[],[f33,f79]) ).
fof(f124,plain,
( e_63 = select(a_54,i6)
| i4 = i6
| i5 = i6 ),
inference(superposition,[],[f77,f122]) ).
fof(f126,plain,
( e_69 = select(a_60,i7)
| i6 = i7 ),
inference(superposition,[],[f36,f80]) ).
fof(f128,plain,
( e_69 = select(a_56,i7)
| i5 = i7
| i6 = i7 ),
inference(superposition,[],[f78,f126]) ).
fof(f130,plain,
( e_67 = select(a_62,i7)
| i6 = i7 ),
inference(superposition,[],[f35,f81]) ).
fof(f132,plain,
( e_67 = select(a_58,i7)
| i5 = i7
| i6 = i7 ),
inference(superposition,[],[f79,f130]) ).
fof(f134,plain,
( e_73 = select(a_64,i8)
| i7 = i8 ),
inference(superposition,[],[f38,f82]) ).
fof(f136,plain,
( e_73 = select(a_60,i8)
| i6 = i8
| i7 = i8 ),
inference(superposition,[],[f80,f134]) ).
fof(f138,plain,
( e_71 = select(a_66,i8)
| i7 = i8 ),
inference(superposition,[],[f37,f83]) ).
fof(f140,plain,
( e_71 = select(a_62,i8)
| i6 = i8
| i7 = i8 ),
inference(superposition,[],[f81,f138]) ).
fof(f142,plain,
( e_77 = select(a_68,i9)
| i8 = i9 ),
inference(superposition,[],[f40,f84]) ).
fof(f144,plain,
( e_77 = select(a_64,i9)
| i7 = i9
| i8 = i9 ),
inference(superposition,[],[f82,f142]) ).
fof(f146,plain,
( e_75 = select(a_70,i9)
| i8 = i9 ),
inference(superposition,[],[f39,f85]) ).
fof(f148,plain,
( e_75 = select(a_66,i9)
| i7 = i9
| i8 = i9 ),
inference(superposition,[],[f83,f146]) ).
fof(f150,plain,
( e_81 = select(a_72,i10)
| i9 = i10 ),
inference(superposition,[],[f42,f86]) ).
fof(f151,plain,
( e_79 = select(a_72,i10)
| i9 = i10 ),
inference(forward_demodulation,[],[f150,f69]) ).
fof(f154,plain,
( e_79 = select(a_68,i10)
| i8 = i10
| i9 = i10 ),
inference(superposition,[],[f84,f151]) ).
fof(f156,plain,
( e_79 = select(a_74,i10)
| i9 = i10 ),
inference(superposition,[],[f41,f87]) ).
fof(f158,plain,
( e_79 = select(a_70,i10)
| i8 = i10
| i9 = i10 ),
inference(superposition,[],[f85,f156]) ).
fof(f160,plain,
! [X0] :
( select(a_76,X0) = select(a_78,X0)
| i10 = X0
| i10 = X0 ),
inference(superposition,[],[f88,f89]) ).
fof(f161,plain,
! [X0] :
( select(a_76,X0) = select(a_78,X0)
| i10 = X0 ),
inference(duplicate_literal_removal,[],[f160]) ).
fof(f165,plain,
! [X0] :
( select(a_74,X0) = select(a_76,X0)
| i9 = X0
| i10 = X0 ),
inference(superposition,[],[f87,f161]) ).
fof(f166,plain,
( e_77 = select(a_76,i9)
| i9 = i10 ),
inference(superposition,[],[f66,f161]) ).
fof(f167,plain,
( i9 = i10
| e_75 = e_77 ),
inference(forward_demodulation,[],[f166,f65]) ).
fof(f170,plain,
( e_79 = select(a_78,i9)
| e_75 = e_77 ),
inference(superposition,[],[f41,f167]) ).
fof(f171,plain,
( e_81 = select(a_76,i9)
| e_75 = e_77 ),
inference(superposition,[],[f42,f167]) ).
fof(f175,plain,
( e_75 = e_81
| e_75 = e_77 ),
inference(forward_demodulation,[],[f171,f65]) ).
fof(f176,plain,
( e_77 = e_79
| e_75 = e_77 ),
inference(forward_demodulation,[],[f170,f66]) ).
fof(f178,plain,
( e_75 = e_79
| e_75 = e_77 ),
inference(forward_demodulation,[],[f175,f69]) ).
fof(f182,plain,
( e_75 = e_77
| e_75 = e_77
| e_75 = e_77 ),
inference(superposition,[],[f176,f178]) ).
fof(f185,plain,
e_75 = e_77,
inference(duplicate_literal_removal,[],[f182]) ).
fof(f188,plain,
( e_61 = select(a_44,i5)
| i2 = i5
| i3 = i5
| i4 = i5 ),
inference(superposition,[],[f72,f112]) ).
fof(f191,plain,
( e_59 = select(a_46,i5)
| i2 = i5
| i3 = i5
| i4 = i5 ),
inference(superposition,[],[f73,f116]) ).
fof(f195,plain,
( e_65 = select(a_48,i6)
| i3 = i6
| i4 = i6
| i5 = i6 ),
inference(superposition,[],[f74,f120]) ).
fof(f201,plain,
( e_63 = select(a_50,i6)
| i3 = i6
| i4 = i6
| i5 = i6 ),
inference(superposition,[],[f75,f124]) ).
fof(f207,plain,
( e_69 = select(a_52,i7)
| i4 = i7
| i5 = i7
| i6 = i7 ),
inference(superposition,[],[f76,f128]) ).
fof(f215,plain,
( e_67 = select(a_54,i7)
| i4 = i7
| i5 = i7
| i6 = i7 ),
inference(superposition,[],[f77,f132]) ).
fof(f223,plain,
( e_73 = select(a_56,i8)
| i5 = i8
| i6 = i8
| i7 = i8 ),
inference(superposition,[],[f78,f136]) ).
fof(f229,plain,
( e_71 = select(a_58,i8)
| i5 = i8
| i6 = i8
| i7 = i8 ),
inference(superposition,[],[f79,f140]) ).
fof(f235,plain,
( e_77 = select(a_60,i9)
| i6 = i9
| i7 = i9
| i8 = i9 ),
inference(superposition,[],[f80,f144]) ).
fof(f236,plain,
( e_75 = select(a_60,i9)
| i6 = i9
| i7 = i9
| i8 = i9 ),
inference(forward_demodulation,[],[f235,f185]) ).
fof(f243,plain,
( e_75 = select(a_62,i9)
| i6 = i9
| i7 = i9
| i8 = i9 ),
inference(superposition,[],[f81,f148]) ).
fof(f249,plain,
( e_79 = select(a_64,i10)
| i7 = i10
| i8 = i10
| i9 = i10 ),
inference(superposition,[],[f82,f154]) ).
fof(f251,plain,
( e_79 = select(a_66,i10)
| i7 = i10
| i8 = i10
| i9 = i10 ),
inference(superposition,[],[f83,f158]) ).
fof(f253,plain,
! [X0] :
( select(a_72,X0) = select(a_74,X0)
| i9 = X0
| i9 = X0
| i10 = X0 ),
inference(superposition,[],[f86,f165]) ).
fof(f254,plain,
! [X0] :
( select(a_72,X0) = select(a_74,X0)
| i9 = X0
| i10 = X0 ),
inference(duplicate_literal_removal,[],[f253]) ).
fof(f258,plain,
! [X0] :
( select(a_70,X0) = select(a_72,X0)
| i8 = X0
| i9 = X0
| i10 = X0 ),
inference(superposition,[],[f85,f254]) ).
fof(f259,plain,
( e_73 = select(a_72,i8)
| i8 = i9
| i8 = i10 ),
inference(superposition,[],[f64,f254]) ).
fof(f260,plain,
( i8 = i10
| i8 = i9
| e_71 = e_73 ),
inference(forward_demodulation,[],[f259,f63]) ).
fof(f269,plain,
( e_79 = select(a_72,i8)
| i8 = i9
| i8 = i9
| e_71 = e_73 ),
inference(superposition,[],[f151,f260]) ).
fof(f270,plain,
( e_79 = select(a_74,i8)
| i8 = i9
| i8 = i9
| e_71 = e_73 ),
inference(superposition,[],[f156,f260]) ).
fof(f277,plain,
( e_79 = select(a_74,i8)
| i8 = i9
| e_71 = e_73 ),
inference(duplicate_literal_removal,[],[f270]) ).
fof(f278,plain,
( e_79 = select(a_72,i8)
| i8 = i9
| e_71 = e_73 ),
inference(duplicate_literal_removal,[],[f269]) ).
fof(f280,plain,
( e_73 = e_79
| i8 = i9
| e_71 = e_73 ),
inference(forward_demodulation,[],[f277,f64]) ).
fof(f281,plain,
( e_71 = e_79
| i8 = i9
| e_71 = e_73 ),
inference(forward_demodulation,[],[f278,f63]) ).
fof(f293,plain,
( e_65 = select(a_44,i6)
| i2 = i6
| i3 = i6
| i4 = i6
| i5 = i6 ),
inference(superposition,[],[f72,f195]) ).
fof(f303,plain,
( e_71 = e_73
| i8 = i9
| e_71 = e_73
| i8 = i9
| e_71 = e_73 ),
inference(superposition,[],[f280,f281]) ).
fof(f304,plain,
( i8 = i9
| e_71 = e_73 ),
inference(duplicate_literal_removal,[],[f303]) ).
fof(f307,plain,
( e_63 = select(a_46,i6)
| i2 = i6
| i3 = i6
| i4 = i6
| i5 = i6 ),
inference(superposition,[],[f73,f201]) ).
fof(f310,plain,
( e_75 = select(a_74,i8)
| e_71 = e_73 ),
inference(superposition,[],[f39,f304]) ).
fof(f311,plain,
( e_77 = select(a_72,i8)
| e_71 = e_73 ),
inference(superposition,[],[f40,f304]) ).
fof(f320,plain,
( e_71 = e_77
| e_71 = e_73 ),
inference(forward_demodulation,[],[f311,f63]) ).
fof(f321,plain,
( e_73 = e_75
| e_71 = e_73 ),
inference(forward_demodulation,[],[f310,f64]) ).
fof(f323,plain,
( e_71 = e_75
| e_71 = e_73 ),
inference(forward_demodulation,[],[f320,f185]) ).
fof(f325,plain,
( e_69 = select(a_48,i7)
| i3 = i7
| i4 = i7
| i5 = i7
| i6 = i7 ),
inference(superposition,[],[f74,f207]) ).
fof(f333,plain,
( e_67 = select(a_50,i7)
| i3 = i7
| i4 = i7
| i5 = i7
| i6 = i7 ),
inference(superposition,[],[f75,f215]) ).
fof(f335,plain,
( e_71 = e_73
| e_71 = e_73
| e_71 = e_73 ),
inference(superposition,[],[f321,f323]) ).
fof(f340,plain,
e_71 = e_73,
inference(duplicate_literal_removal,[],[f335]) ).
fof(f345,plain,
( e_73 = select(a_52,i8)
| i4 = i8
| i5 = i8
| i6 = i8
| i7 = i8 ),
inference(superposition,[],[f76,f223]) ).
fof(f346,plain,
( e_71 = select(a_52,i8)
| i4 = i8
| i5 = i8
| i6 = i8
| i7 = i8 ),
inference(forward_demodulation,[],[f345,f340]) ).
fof(f350,plain,
( e_71 = select(a_54,i8)
| i4 = i8
| i5 = i8
| i6 = i8
| i7 = i8 ),
inference(superposition,[],[f77,f229]) ).
fof(f354,plain,
( e_75 = select(a_56,i9)
| i5 = i9
| i6 = i9
| i7 = i9
| i8 = i9 ),
inference(superposition,[],[f78,f236]) ).
fof(f360,plain,
( e_75 = select(a_58,i9)
| i5 = i9
| i6 = i9
| i7 = i9
| i8 = i9 ),
inference(superposition,[],[f79,f243]) ).
fof(f366,plain,
( e_79 = select(a_60,i10)
| i6 = i10
| i7 = i10
| i8 = i10
| i9 = i10 ),
inference(superposition,[],[f80,f249]) ).
fof(f372,plain,
( e_79 = select(a_62,i10)
| i6 = i10
| i7 = i10
| i8 = i10
| i9 = i10 ),
inference(superposition,[],[f81,f251]) ).
fof(f380,plain,
! [X0] :
( select(a_68,X0) = select(a_70,X0)
| i8 = X0
| i8 = X0
| i9 = X0
| i10 = X0 ),
inference(superposition,[],[f84,f258]) ).
fof(f381,plain,
! [X0] :
( select(a_68,X0) = select(a_70,X0)
| i8 = X0
| i9 = X0
| i10 = X0 ),
inference(duplicate_literal_removal,[],[f380]) ).
fof(f398,plain,
( e_69 = select(a_44,i7)
| i2 = i7
| i3 = i7
| i4 = i7
| i5 = i7
| i6 = i7 ),
inference(superposition,[],[f72,f325]) ).
fof(f404,plain,
( e_67 = select(a_46,i7)
| i2 = i7
| i3 = i7
| i4 = i7
| i5 = i7
| i6 = i7 ),
inference(superposition,[],[f73,f333]) ).
fof(f410,plain,
( e_71 = select(a_48,i8)
| i3 = i8
| i4 = i8
| i5 = i8
| i6 = i8
| i7 = i8 ),
inference(superposition,[],[f74,f346]) ).
fof(f422,plain,
( e_71 = select(a_50,i8)
| i3 = i8
| i4 = i8
| i5 = i8
| i6 = i8
| i7 = i8 ),
inference(superposition,[],[f75,f350]) ).
fof(f428,plain,
( e_75 = select(a_52,i9)
| i4 = i9
| i5 = i9
| i6 = i9
| i7 = i9
| i8 = i9 ),
inference(superposition,[],[f76,f354]) ).
fof(f442,plain,
( e_75 = select(a_54,i9)
| i4 = i9
| i5 = i9
| i6 = i9
| i7 = i9
| i8 = i9 ),
inference(superposition,[],[f77,f360]) ).
fof(f452,plain,
( e_79 = select(a_56,i10)
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| i9 = i10 ),
inference(superposition,[],[f78,f366]) ).
fof(f462,plain,
( e_79 = select(a_58,i10)
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| i9 = i10 ),
inference(superposition,[],[f79,f372]) ).
fof(f470,plain,
! [X0] :
( select(a_66,X0) = select(a_68,X0)
| i7 = X0
| i8 = X0
| i9 = X0
| i10 = X0 ),
inference(superposition,[],[f83,f381]) ).
fof(f471,plain,
( e_69 = select(a_68,i7)
| i7 = i8
| i7 = i9
| i7 = i10 ),
inference(superposition,[],[f62,f381]) ).
fof(f472,plain,
( i7 = i10
| i7 = i8
| i7 = i9
| e_67 = e_69 ),
inference(forward_demodulation,[],[f471,f61]) ).
fof(f488,plain,
( e_79 = select(a_68,i7)
| i7 = i8
| i7 = i9
| i7 = i8
| i7 = i9
| e_67 = e_69 ),
inference(superposition,[],[f154,f472]) ).
fof(f490,plain,
( e_79 = select(a_70,i7)
| i7 = i8
| i7 = i9
| i7 = i8
| i7 = i9
| e_67 = e_69 ),
inference(superposition,[],[f158,f472]) ).
fof(f501,plain,
( e_79 = select(a_70,i7)
| i7 = i8
| i7 = i9
| e_67 = e_69 ),
inference(duplicate_literal_removal,[],[f490]) ).
fof(f503,plain,
( e_79 = select(a_68,i7)
| i7 = i8
| i7 = i9
| e_67 = e_69 ),
inference(duplicate_literal_removal,[],[f488]) ).
fof(f507,plain,
( e_69 = e_79
| i7 = i8
| i7 = i9
| e_67 = e_69 ),
inference(forward_demodulation,[],[f501,f62]) ).
fof(f508,plain,
( e_67 = e_79
| i7 = i8
| i7 = i9
| e_67 = e_69 ),
inference(forward_demodulation,[],[f503,f61]) ).
fof(f526,plain,
( e_71 = select(a_44,i8)
| i2 = i8
| i3 = i8
| i4 = i8
| i5 = i8
| i6 = i8
| i7 = i8 ),
inference(superposition,[],[f72,f410]) ).
fof(f542,plain,
( e_67 = e_69
| i7 = i8
| i7 = i9
| e_67 = e_69
| i7 = i8
| i7 = i9
| e_67 = e_69 ),
inference(superposition,[],[f507,f508]) ).
fof(f543,plain,
( i7 = i9
| i7 = i8
| e_67 = e_69 ),
inference(duplicate_literal_removal,[],[f542]) ).
fof(f546,plain,
( e_71 = select(a_46,i8)
| i2 = i8
| i3 = i8
| i4 = i8
| i5 = i8
| i6 = i8
| i7 = i8 ),
inference(superposition,[],[f73,f422]) ).
fof(f554,plain,
( e_77 = select(a_68,i7)
| i7 = i8
| i7 = i8
| e_67 = e_69 ),
inference(superposition,[],[f142,f543]) ).
fof(f555,plain,
( e_75 = select(a_70,i7)
| i7 = i8
| i7 = i8
| e_67 = e_69 ),
inference(superposition,[],[f146,f543]) ).
fof(f567,plain,
( e_75 = select(a_70,i7)
| i7 = i8
| e_67 = e_69 ),
inference(duplicate_literal_removal,[],[f555]) ).
fof(f568,plain,
( e_77 = select(a_68,i7)
| i7 = i8
| e_67 = e_69 ),
inference(duplicate_literal_removal,[],[f554]) ).
fof(f570,plain,
( e_69 = e_75
| i7 = i8
| e_67 = e_69 ),
inference(forward_demodulation,[],[f567,f62]) ).
fof(f571,plain,
( e_67 = e_77
| i7 = i8
| e_67 = e_69 ),
inference(forward_demodulation,[],[f568,f61]) ).
fof(f575,plain,
( e_67 = e_75
| i7 = i8
| e_67 = e_69 ),
inference(forward_demodulation,[],[f571,f185]) ).
fof(f577,plain,
( e_75 = select(a_48,i9)
| i3 = i9
| i4 = i9
| i5 = i9
| i6 = i9
| i7 = i9
| i8 = i9 ),
inference(superposition,[],[f74,f428]) ).
fof(f591,plain,
( e_75 = select(a_50,i9)
| i3 = i9
| i4 = i9
| i5 = i9
| i6 = i9
| i7 = i9
| i8 = i9 ),
inference(superposition,[],[f75,f442]) ).
fof(f603,plain,
( e_67 = e_69
| i7 = i8
| e_67 = e_69
| i7 = i8
| e_67 = e_69 ),
inference(superposition,[],[f570,f575]) ).
fof(f604,plain,
( i7 = i8
| e_67 = e_69 ),
inference(duplicate_literal_removal,[],[f603]) ).
fof(f607,plain,
( e_79 = select(a_52,i10)
| i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| i9 = i10 ),
inference(superposition,[],[f76,f452]) ).
fof(f610,plain,
( e_71 = select(a_70,i7)
| e_67 = e_69 ),
inference(superposition,[],[f37,f604]) ).
fof(f611,plain,
( e_73 = select(a_68,i7)
| e_67 = e_69 ),
inference(superposition,[],[f38,f604]) ).
fof(f626,plain,
( e_67 = e_73
| e_67 = e_69 ),
inference(forward_demodulation,[],[f611,f61]) ).
fof(f627,plain,
( e_69 = e_71
| e_67 = e_69 ),
inference(forward_demodulation,[],[f610,f62]) ).
fof(f629,plain,
( e_67 = e_71
| e_67 = e_69 ),
inference(forward_demodulation,[],[f626,f340]) ).
fof(f631,plain,
( e_79 = select(a_54,i10)
| i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| i9 = i10 ),
inference(superposition,[],[f77,f462]) ).
fof(f639,plain,
! [X0] :
( select(a_64,X0) = select(a_66,X0)
| i7 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i10 = X0 ),
inference(superposition,[],[f82,f470]) ).
fof(f640,plain,
! [X0] :
( select(a_64,X0) = select(a_66,X0)
| i7 = X0
| i8 = X0
| i9 = X0
| i10 = X0 ),
inference(duplicate_literal_removal,[],[f639]) ).
fof(f643,plain,
( e_67 = e_69
| e_67 = e_69
| e_67 = e_69 ),
inference(superposition,[],[f627,f629]) ).
fof(f648,plain,
e_67 = e_69,
inference(duplicate_literal_removal,[],[f643]) ).
fof(f656,plain,
( e_75 = select(a_44,i9)
| i2 = i9
| i3 = i9
| i4 = i9
| i5 = i9
| i6 = i9
| i7 = i9
| i8 = i9 ),
inference(superposition,[],[f72,f577]) ).
fof(f662,plain,
( e_75 = select(a_46,i9)
| i2 = i9
| i3 = i9
| i4 = i9
| i5 = i9
| i6 = i9
| i7 = i9
| i8 = i9 ),
inference(superposition,[],[f73,f591]) ).
fof(f668,plain,
( e_79 = select(a_48,i10)
| i3 = i10
| i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| i9 = i10 ),
inference(superposition,[],[f74,f607]) ).
fof(f674,plain,
( e_79 = select(a_50,i10)
| i3 = i10
| i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| i9 = i10 ),
inference(superposition,[],[f75,f631]) ).
fof(f789,plain,
! [X0] :
( select(a_62,X0) = select(a_64,X0)
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i10 = X0 ),
inference(superposition,[],[f81,f640]) ).
fof(f790,plain,
( e_65 = select(a_64,i6)
| i6 = i7
| i6 = i8
| i6 = i9
| i6 = i10 ),
inference(superposition,[],[f60,f640]) ).
fof(f791,plain,
( i6 = i10
| i6 = i7
| i6 = i8
| i6 = i9
| e_63 = e_65 ),
inference(forward_demodulation,[],[f790,f59]) ).
fof(f826,plain,
( e_79 = select(a_44,i10)
| i2 = i10
| i3 = i10
| i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| i9 = i10 ),
inference(superposition,[],[f72,f668]) ).
fof(f836,plain,
( e_79 = select(a_46,i10)
| i2 = i10
| i3 = i10
| i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| i9 = i10 ),
inference(superposition,[],[f73,f674]) ).
fof(f877,plain,
( e_79 = select(a_64,i6)
| i6 = i7
| i6 = i8
| i6 = i9
| i6 = i7
| i6 = i8
| i6 = i9
| e_63 = e_65 ),
inference(superposition,[],[f249,f791]) ).
fof(f878,plain,
( e_79 = select(a_66,i6)
| i6 = i7
| i6 = i8
| i6 = i9
| i6 = i7
| i6 = i8
| i6 = i9
| e_63 = e_65 ),
inference(superposition,[],[f251,f791]) ).
fof(f887,plain,
( e_79 = select(a_66,i6)
| i6 = i7
| i6 = i8
| i6 = i9
| e_63 = e_65 ),
inference(duplicate_literal_removal,[],[f878]) ).
fof(f888,plain,
( e_79 = select(a_64,i6)
| i6 = i7
| i6 = i8
| i6 = i9
| e_63 = e_65 ),
inference(duplicate_literal_removal,[],[f877]) ).
fof(f897,plain,
( e_65 = e_79
| i6 = i7
| i6 = i8
| i6 = i9
| e_63 = e_65 ),
inference(forward_demodulation,[],[f887,f60]) ).
fof(f898,plain,
( e_63 = e_79
| i6 = i7
| i6 = i8
| i6 = i9
| e_63 = e_65 ),
inference(forward_demodulation,[],[f888,f59]) ).
fof(f902,plain,
! [X0] :
( select(a_60,X0) = select(a_62,X0)
| i6 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i10 = X0 ),
inference(superposition,[],[f80,f789]) ).
fof(f903,plain,
! [X0] :
( select(a_60,X0) = select(a_62,X0)
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i10 = X0 ),
inference(duplicate_literal_removal,[],[f902]) ).
fof(f946,plain,
( e_63 = e_65
| i6 = i7
| i6 = i8
| i6 = i9
| e_63 = e_65
| i6 = i7
| i6 = i8
| i6 = i9
| e_63 = e_65 ),
inference(superposition,[],[f897,f898]) ).
fof(f947,plain,
( i6 = i9
| i6 = i7
| i6 = i8
| e_63 = e_65 ),
inference(duplicate_literal_removal,[],[f946]) ).
fof(f958,plain,
( e_77 = select(a_64,i6)
| i6 = i7
| i6 = i8
| i6 = i7
| i6 = i8
| e_63 = e_65 ),
inference(superposition,[],[f144,f947]) ).
fof(f960,plain,
( e_75 = select(a_66,i6)
| i6 = i7
| i6 = i8
| i6 = i7
| i6 = i8
| e_63 = e_65 ),
inference(superposition,[],[f148,f947]) ).
fof(f976,plain,
( e_75 = select(a_66,i6)
| i6 = i7
| i6 = i8
| e_63 = e_65 ),
inference(duplicate_literal_removal,[],[f960]) ).
fof(f978,plain,
( e_77 = select(a_64,i6)
| i6 = i7
| i6 = i8
| e_63 = e_65 ),
inference(duplicate_literal_removal,[],[f958]) ).
fof(f982,plain,
( e_65 = e_75
| i6 = i7
| i6 = i8
| e_63 = e_65 ),
inference(forward_demodulation,[],[f976,f60]) ).
fof(f983,plain,
( e_63 = e_77
| i6 = i7
| i6 = i8
| e_63 = e_65 ),
inference(forward_demodulation,[],[f978,f59]) ).
fof(f988,plain,
( e_63 = e_75
| i6 = i7
| i6 = i8
| e_63 = e_65 ),
inference(forward_demodulation,[],[f983,f185]) ).
fof(f1034,plain,
( e_63 = e_65
| i6 = i7
| i6 = i8
| e_63 = e_65
| i6 = i7
| i6 = i8
| e_63 = e_65 ),
inference(superposition,[],[f982,f988]) ).
fof(f1035,plain,
( i6 = i8
| i6 = i7
| e_63 = e_65 ),
inference(duplicate_literal_removal,[],[f1034]) ).
fof(f1052,plain,
( e_73 = select(a_64,i6)
| i6 = i7
| i6 = i7
| e_63 = e_65 ),
inference(superposition,[],[f134,f1035]) ).
fof(f1053,plain,
( e_71 = select(a_66,i6)
| i6 = i7
| i6 = i7
| e_63 = e_65 ),
inference(superposition,[],[f138,f1035]) ).
fof(f1071,plain,
( e_71 = select(a_66,i6)
| i6 = i7
| e_63 = e_65 ),
inference(duplicate_literal_removal,[],[f1053]) ).
fof(f1072,plain,
( e_73 = select(a_64,i6)
| i6 = i7
| e_63 = e_65 ),
inference(duplicate_literal_removal,[],[f1052]) ).
fof(f1074,plain,
( e_65 = e_71
| i6 = i7
| e_63 = e_65 ),
inference(forward_demodulation,[],[f1071,f60]) ).
fof(f1075,plain,
( e_63 = e_73
| i6 = i7
| e_63 = e_65 ),
inference(forward_demodulation,[],[f1072,f59]) ).
fof(f1079,plain,
( e_63 = e_71
| i6 = i7
| e_63 = e_65 ),
inference(forward_demodulation,[],[f1075,f340]) ).
fof(f1119,plain,
( e_63 = e_65
| i6 = i7
| e_63 = e_65
| i6 = i7
| e_63 = e_65 ),
inference(superposition,[],[f1074,f1079]) ).
fof(f1120,plain,
( i6 = i7
| e_63 = e_65 ),
inference(duplicate_literal_removal,[],[f1119]) ).
fof(f1132,plain,
( e_67 = select(a_66,i6)
| e_63 = e_65 ),
inference(superposition,[],[f35,f1120]) ).
fof(f1133,plain,
( e_69 = select(a_64,i6)
| e_63 = e_65 ),
inference(superposition,[],[f36,f1120]) ).
fof(f1156,plain,
( e_63 = e_69
| e_63 = e_65 ),
inference(forward_demodulation,[],[f1133,f59]) ).
fof(f1157,plain,
( e_65 = e_67
| e_63 = e_65 ),
inference(forward_demodulation,[],[f1132,f60]) ).
fof(f1159,plain,
( e_63 = e_67
| e_63 = e_65 ),
inference(forward_demodulation,[],[f1156,f648]) ).
fof(f1187,plain,
( e_63 = e_65
| e_63 = e_65
| e_63 = e_65 ),
inference(superposition,[],[f1157,f1159]) ).
fof(f1192,plain,
e_63 = e_65,
inference(duplicate_literal_removal,[],[f1187]) ).
fof(f1211,plain,
! [X0] :
( select(a_58,X0) = select(a_60,X0)
| i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i10 = X0 ),
inference(superposition,[],[f79,f903]) ).
fof(f1212,plain,
( e_61 = select(a_60,i5)
| i5 = i6
| i5 = i7
| i5 = i8
| i5 = i9
| i5 = i10 ),
inference(superposition,[],[f58,f903]) ).
fof(f1213,plain,
( i5 = i10
| i5 = i6
| i5 = i7
| i5 = i8
| i5 = i9
| e_59 = e_61 ),
inference(forward_demodulation,[],[f1212,f57]) ).
fof(f1267,plain,
( e_79 = select(a_60,i5)
| i5 = i6
| i5 = i7
| i5 = i8
| i5 = i9
| i5 = i6
| i5 = i7
| i5 = i8
| i5 = i9
| e_59 = e_61 ),
inference(superposition,[],[f366,f1213]) ).
fof(f1268,plain,
( e_79 = select(a_62,i5)
| i5 = i6
| i5 = i7
| i5 = i8
| i5 = i9
| i5 = i6
| i5 = i7
| i5 = i8
| i5 = i9
| e_59 = e_61 ),
inference(superposition,[],[f372,f1213]) ).
fof(f1277,plain,
( e_79 = select(a_62,i5)
| i5 = i6
| i5 = i7
| i5 = i8
| i5 = i9
| e_59 = e_61 ),
inference(duplicate_literal_removal,[],[f1268]) ).
fof(f1278,plain,
( e_79 = select(a_60,i5)
| i5 = i6
| i5 = i7
| i5 = i8
| i5 = i9
| e_59 = e_61 ),
inference(duplicate_literal_removal,[],[f1267]) ).
fof(f1291,plain,
( e_61 = e_79
| i5 = i6
| i5 = i7
| i5 = i8
| i5 = i9
| e_59 = e_61 ),
inference(forward_demodulation,[],[f1277,f58]) ).
fof(f1292,plain,
( e_59 = e_79
| i5 = i6
| i5 = i7
| i5 = i8
| i5 = i9
| e_59 = e_61 ),
inference(forward_demodulation,[],[f1278,f57]) ).
fof(f1304,plain,
! [X0] :
( select(a_56,X0) = select(a_58,X0)
| i5 = X0
| i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i10 = X0 ),
inference(superposition,[],[f78,f1211]) ).
fof(f1305,plain,
! [X0] :
( select(a_56,X0) = select(a_58,X0)
| i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i10 = X0 ),
inference(duplicate_literal_removal,[],[f1304]) ).
fof(f1540,plain,
( e_59 = e_61
| i5 = i6
| i5 = i7
| i5 = i8
| i5 = i9
| e_59 = e_61
| i5 = i6
| i5 = i7
| i5 = i8
| i5 = i9
| e_59 = e_61 ),
inference(superposition,[],[f1291,f1292]) ).
fof(f1541,plain,
( i5 = i9
| i5 = i6
| i5 = i7
| i5 = i8
| e_59 = e_61 ),
inference(duplicate_literal_removal,[],[f1540]) ).
fof(f1641,plain,
( e_75 = select(a_60,i5)
| i5 = i6
| i5 = i7
| i5 = i8
| i5 = i6
| i5 = i7
| i5 = i8
| e_59 = e_61 ),
inference(superposition,[],[f236,f1541]) ).
fof(f1642,plain,
( e_75 = select(a_62,i5)
| i5 = i6
| i5 = i7
| i5 = i8
| i5 = i6
| i5 = i7
| i5 = i8
| e_59 = e_61 ),
inference(superposition,[],[f243,f1541]) ).
fof(f1657,plain,
( e_75 = select(a_62,i5)
| i5 = i6
| i5 = i7
| i5 = i8
| e_59 = e_61 ),
inference(duplicate_literal_removal,[],[f1642]) ).
fof(f1658,plain,
( e_75 = select(a_60,i5)
| i5 = i6
| i5 = i7
| i5 = i8
| e_59 = e_61 ),
inference(duplicate_literal_removal,[],[f1641]) ).
fof(f1666,plain,
( e_61 = e_75
| i5 = i6
| i5 = i7
| i5 = i8
| e_59 = e_61 ),
inference(forward_demodulation,[],[f1657,f58]) ).
fof(f1667,plain,
( e_59 = e_75
| i5 = i6
| i5 = i7
| i5 = i8
| e_59 = e_61 ),
inference(forward_demodulation,[],[f1658,f57]) ).
fof(f1736,plain,
( e_59 = e_61
| i5 = i6
| i5 = i7
| i5 = i8
| e_59 = e_61
| i5 = i6
| i5 = i7
| i5 = i8
| e_59 = e_61 ),
inference(superposition,[],[f1666,f1667]) ).
fof(f1737,plain,
( i5 = i8
| i5 = i6
| i5 = i7
| e_59 = e_61 ),
inference(duplicate_literal_removal,[],[f1736]) ).
fof(f1756,plain,
( e_73 = select(a_60,i5)
| i5 = i6
| i5 = i7
| i5 = i6
| i5 = i7
| e_59 = e_61 ),
inference(superposition,[],[f136,f1737]) ).
fof(f1758,plain,
( e_71 = select(a_62,i5)
| i5 = i6
| i5 = i7
| i5 = i6
| i5 = i7
| e_59 = e_61 ),
inference(superposition,[],[f140,f1737]) ).
fof(f1780,plain,
( e_71 = select(a_62,i5)
| i5 = i6
| i5 = i7
| e_59 = e_61 ),
inference(duplicate_literal_removal,[],[f1758]) ).
fof(f1782,plain,
( e_73 = select(a_60,i5)
| i5 = i6
| i5 = i7
| e_59 = e_61 ),
inference(duplicate_literal_removal,[],[f1756]) ).
fof(f1786,plain,
( e_61 = e_71
| i5 = i6
| i5 = i7
| e_59 = e_61 ),
inference(forward_demodulation,[],[f1780,f58]) ).
fof(f1787,plain,
( e_59 = e_73
| i5 = i6
| i5 = i7
| e_59 = e_61 ),
inference(forward_demodulation,[],[f1782,f57]) ).
fof(f1792,plain,
( e_59 = e_71
| i5 = i6
| i5 = i7
| e_59 = e_61 ),
inference(forward_demodulation,[],[f1787,f340]) ).
fof(f1856,plain,
( e_59 = e_61
| i5 = i6
| i5 = i7
| e_59 = e_61
| i5 = i6
| i5 = i7
| e_59 = e_61 ),
inference(superposition,[],[f1786,f1792]) ).
fof(f1857,plain,
( i5 = i7
| i5 = i6
| e_59 = e_61 ),
inference(duplicate_literal_removal,[],[f1856]) ).
fof(f1861,plain,
! [X0] :
( select(a_54,X0) = select(a_56,X0)
| i4 = X0
| i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i10 = X0 ),
inference(superposition,[],[f77,f1305]) ).
fof(f1862,plain,
( e_57 = select(a_56,i4)
| i4 = i5
| i4 = i6
| i4 = i7
| i4 = i8
| i4 = i9
| i4 = i10 ),
inference(superposition,[],[f56,f1305]) ).
fof(f1863,plain,
( i4 = i10
| i4 = i5
| i4 = i6
| i4 = i7
| i4 = i8
| i4 = i9
| e_55 = e_57 ),
inference(forward_demodulation,[],[f1862,f55]) ).
fof(f1872,plain,
( e_69 = select(a_60,i5)
| i5 = i6
| i5 = i6
| e_59 = e_61 ),
inference(superposition,[],[f126,f1857]) ).
fof(f1873,plain,
( e_67 = select(a_62,i5)
| i5 = i6
| i5 = i6
| e_59 = e_61 ),
inference(superposition,[],[f130,f1857]) ).
fof(f1899,plain,
( e_67 = select(a_62,i5)
| i5 = i6
| e_59 = e_61 ),
inference(duplicate_literal_removal,[],[f1873]) ).
fof(f1900,plain,
( e_69 = select(a_60,i5)
| i5 = i6
| e_59 = e_61 ),
inference(duplicate_literal_removal,[],[f1872]) ).
fof(f1902,plain,
( e_61 = e_67
| i5 = i6
| e_59 = e_61 ),
inference(forward_demodulation,[],[f1899,f58]) ).
fof(f1903,plain,
( e_59 = e_69
| i5 = i6
| e_59 = e_61 ),
inference(forward_demodulation,[],[f1900,f57]) ).
fof(f1907,plain,
( e_59 = e_67
| i5 = i6
| e_59 = e_61 ),
inference(forward_demodulation,[],[f1903,f648]) ).
fof(f1947,plain,
( e_59 = e_61
| i5 = i6
| e_59 = e_61
| i5 = i6
| e_59 = e_61 ),
inference(superposition,[],[f1902,f1907]) ).
fof(f1948,plain,
( i5 = i6
| e_59 = e_61 ),
inference(duplicate_literal_removal,[],[f1947]) ).
fof(f1977,plain,
( e_79 = select(a_56,i4)
| i4 = i5
| i4 = i6
| i4 = i7
| i4 = i8
| i4 = i9
| i4 = i5
| i4 = i6
| i4 = i7
| i4 = i8
| i4 = i9
| e_55 = e_57 ),
inference(superposition,[],[f452,f1863]) ).
fof(f1978,plain,
( e_79 = select(a_58,i4)
| i4 = i5
| i4 = i6
| i4 = i7
| i4 = i8
| i4 = i9
| i4 = i5
| i4 = i6
| i4 = i7
| i4 = i8
| i4 = i9
| e_55 = e_57 ),
inference(superposition,[],[f462,f1863]) ).
fof(f1991,plain,
( e_79 = select(a_58,i4)
| i4 = i5
| i4 = i6
| i4 = i7
| i4 = i8
| i4 = i9
| e_55 = e_57 ),
inference(duplicate_literal_removal,[],[f1978]) ).
fof(f1992,plain,
( e_79 = select(a_56,i4)
| i4 = i5
| i4 = i6
| i4 = i7
| i4 = i8
| i4 = i9
| e_55 = e_57 ),
inference(duplicate_literal_removal,[],[f1977]) ).
fof(f2008,plain,
( e_57 = e_79
| i4 = i5
| i4 = i6
| i4 = i7
| i4 = i8
| i4 = i9
| e_55 = e_57 ),
inference(forward_demodulation,[],[f1991,f56]) ).
fof(f2009,plain,
( e_55 = e_79
| i4 = i5
| i4 = i6
| i4 = i7
| i4 = i8
| i4 = i9
| e_55 = e_57 ),
inference(forward_demodulation,[],[f1992,f55]) ).
fof(f2014,plain,
( e_63 = select(a_62,i5)
| e_59 = e_61 ),
inference(superposition,[],[f33,f1948]) ).
fof(f2015,plain,
( e_65 = select(a_60,i5)
| e_59 = e_61 ),
inference(superposition,[],[f34,f1948]) ).
fof(f2048,plain,
( e_59 = e_65
| e_59 = e_61 ),
inference(forward_demodulation,[],[f2015,f57]) ).
fof(f2049,plain,
( e_61 = e_63
| e_59 = e_61 ),
inference(forward_demodulation,[],[f2014,f58]) ).
fof(f2051,plain,
( e_59 = e_63
| e_59 = e_61 ),
inference(forward_demodulation,[],[f2048,f1192]) ).
fof(f2053,plain,
! [X0] :
( select(a_52,X0) = select(a_54,X0)
| i4 = X0
| i4 = X0
| i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i10 = X0 ),
inference(superposition,[],[f76,f1861]) ).
fof(f2054,plain,
! [X0] :
( select(a_52,X0) = select(a_54,X0)
| i4 = X0
| i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i10 = X0 ),
inference(duplicate_literal_removal,[],[f2053]) ).
fof(f2073,plain,
( e_59 = e_61
| e_59 = e_61
| e_59 = e_61 ),
inference(superposition,[],[f2049,f2051]) ).
fof(f2078,plain,
e_59 = e_61,
inference(duplicate_literal_removal,[],[f2073]) ).
fof(f2302,plain,
( e_55 = e_57
| i4 = i5
| i4 = i6
| i4 = i7
| i4 = i8
| i4 = i9
| e_55 = e_57
| i4 = i5
| i4 = i6
| i4 = i7
| i4 = i8
| i4 = i9
| e_55 = e_57 ),
inference(superposition,[],[f2008,f2009]) ).
fof(f2303,plain,
( i4 = i9
| i4 = i5
| i4 = i6
| i4 = i7
| i4 = i8
| e_55 = e_57 ),
inference(duplicate_literal_removal,[],[f2302]) ).
fof(f2603,plain,
! [X0] :
( select(a_50,X0) = select(a_52,X0)
| i3 = X0
| i4 = X0
| i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i10 = X0 ),
inference(superposition,[],[f75,f2054]) ).
fof(f2604,plain,
( e_53 = select(a_52,i3)
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| i3 = i8
| i3 = i9
| i3 = i10 ),
inference(superposition,[],[f54,f2054]) ).
fof(f2605,plain,
( i3 = i10
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| i3 = i8
| i3 = i9
| e_51 = e_53 ),
inference(forward_demodulation,[],[f2604,f53]) ).
fof(f2687,plain,
( e_75 = select(a_56,i4)
| i4 = i5
| i4 = i6
| i4 = i7
| i4 = i8
| i4 = i5
| i4 = i6
| i4 = i7
| i4 = i8
| e_55 = e_57 ),
inference(superposition,[],[f354,f2303]) ).
fof(f2688,plain,
( e_75 = select(a_58,i4)
| i4 = i5
| i4 = i6
| i4 = i7
| i4 = i8
| i4 = i5
| i4 = i6
| i4 = i7
| i4 = i8
| e_55 = e_57 ),
inference(superposition,[],[f360,f2303]) ).
fof(f2701,plain,
( e_75 = select(a_58,i4)
| i4 = i5
| i4 = i6
| i4 = i7
| i4 = i8
| e_55 = e_57 ),
inference(duplicate_literal_removal,[],[f2688]) ).
fof(f2702,plain,
( e_75 = select(a_56,i4)
| i4 = i5
| i4 = i6
| i4 = i7
| i4 = i8
| e_55 = e_57 ),
inference(duplicate_literal_removal,[],[f2687]) ).
fof(f2714,plain,
( e_57 = e_75
| i4 = i5
| i4 = i6
| i4 = i7
| i4 = i8
| e_55 = e_57 ),
inference(forward_demodulation,[],[f2701,f56]) ).
fof(f2715,plain,
( e_55 = e_75
| i4 = i5
| i4 = i6
| i4 = i7
| i4 = i8
| e_55 = e_57 ),
inference(forward_demodulation,[],[f2702,f55]) ).
fof(f2814,plain,
( e_79 = select(a_52,i3)
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| i3 = i8
| i3 = i9
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| i3 = i8
| i3 = i9
| e_51 = e_53 ),
inference(superposition,[],[f607,f2605]) ).
fof(f2815,plain,
( e_79 = select(a_54,i3)
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| i3 = i8
| i3 = i9
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| i3 = i8
| i3 = i9
| e_51 = e_53 ),
inference(superposition,[],[f631,f2605]) ).
fof(f2828,plain,
( e_79 = select(a_54,i3)
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| i3 = i8
| i3 = i9
| e_51 = e_53 ),
inference(duplicate_literal_removal,[],[f2815]) ).
fof(f2829,plain,
( e_79 = select(a_52,i3)
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| i3 = i8
| i3 = i9
| e_51 = e_53 ),
inference(duplicate_literal_removal,[],[f2814]) ).
fof(f2849,plain,
( e_53 = e_79
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| i3 = i8
| i3 = i9
| e_51 = e_53 ),
inference(forward_demodulation,[],[f2828,f54]) ).
fof(f2850,plain,
( e_51 = e_79
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| i3 = i8
| i3 = i9
| e_51 = e_53 ),
inference(forward_demodulation,[],[f2829,f53]) ).
fof(f2882,plain,
( e_55 = e_57
| i4 = i5
| i4 = i6
| i4 = i7
| i4 = i8
| e_55 = e_57
| i4 = i5
| i4 = i6
| i4 = i7
| i4 = i8
| e_55 = e_57 ),
inference(superposition,[],[f2714,f2715]) ).
fof(f2883,plain,
( i4 = i8
| i4 = i5
| i4 = i6
| i4 = i7
| e_55 = e_57 ),
inference(duplicate_literal_removal,[],[f2882]) ).
fof(f2886,plain,
! [X0] :
( select(a_48,X0) = select(a_50,X0)
| i3 = X0
| i3 = X0
| i4 = X0
| i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i10 = X0 ),
inference(superposition,[],[f74,f2603]) ).
fof(f2887,plain,
! [X0] :
( select(a_48,X0) = select(a_50,X0)
| i3 = X0
| i4 = X0
| i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i10 = X0 ),
inference(duplicate_literal_removal,[],[f2886]) ).
fof(f2902,plain,
( e_73 = select(a_56,i4)
| i4 = i5
| i4 = i6
| i4 = i7
| i4 = i5
| i4 = i6
| i4 = i7
| e_55 = e_57 ),
inference(superposition,[],[f223,f2883]) ).
fof(f2903,plain,
( e_71 = select(a_58,i4)
| i4 = i5
| i4 = i6
| i4 = i7
| i4 = i5
| i4 = i6
| i4 = i7
| e_55 = e_57 ),
inference(superposition,[],[f229,f2883]) ).
fof(f2929,plain,
( e_71 = select(a_58,i4)
| i4 = i5
| i4 = i6
| i4 = i7
| e_55 = e_57 ),
inference(duplicate_literal_removal,[],[f2903]) ).
fof(f2930,plain,
( e_73 = select(a_56,i4)
| i4 = i5
| i4 = i6
| i4 = i7
| e_55 = e_57 ),
inference(duplicate_literal_removal,[],[f2902]) ).
fof(f2938,plain,
( e_57 = e_71
| i4 = i5
| i4 = i6
| i4 = i7
| e_55 = e_57 ),
inference(forward_demodulation,[],[f2929,f56]) ).
fof(f2939,plain,
( e_55 = e_73
| i4 = i5
| i4 = i6
| i4 = i7
| e_55 = e_57 ),
inference(forward_demodulation,[],[f2930,f55]) ).
fof(f2945,plain,
( e_55 = e_71
| i4 = i5
| i4 = i6
| i4 = i7
| e_55 = e_57 ),
inference(forward_demodulation,[],[f2939,f340]) ).
fof(f3011,plain,
( e_55 = e_57
| i4 = i5
| i4 = i6
| i4 = i7
| e_55 = e_57
| i4 = i5
| i4 = i6
| i4 = i7
| e_55 = e_57 ),
inference(superposition,[],[f2938,f2945]) ).
fof(f3012,plain,
( i4 = i7
| i4 = i5
| i4 = i6
| e_55 = e_57 ),
inference(duplicate_literal_removal,[],[f3011]) ).
fof(f3031,plain,
( e_69 = select(a_56,i4)
| i4 = i5
| i4 = i6
| i4 = i5
| i4 = i6
| e_55 = e_57 ),
inference(superposition,[],[f128,f3012]) ).
fof(f3033,plain,
( e_67 = select(a_58,i4)
| i4 = i5
| i4 = i6
| i4 = i5
| i4 = i6
| e_55 = e_57 ),
inference(superposition,[],[f132,f3012]) ).
fof(f3063,plain,
( e_67 = select(a_58,i4)
| i4 = i5
| i4 = i6
| e_55 = e_57 ),
inference(duplicate_literal_removal,[],[f3033]) ).
fof(f3065,plain,
( e_69 = select(a_56,i4)
| i4 = i5
| i4 = i6
| e_55 = e_57 ),
inference(duplicate_literal_removal,[],[f3031]) ).
fof(f3069,plain,
( e_57 = e_67
| i4 = i5
| i4 = i6
| e_55 = e_57 ),
inference(forward_demodulation,[],[f3063,f56]) ).
fof(f3070,plain,
( e_55 = e_69
| i4 = i5
| i4 = i6
| e_55 = e_57 ),
inference(forward_demodulation,[],[f3065,f55]) ).
fof(f3075,plain,
( e_55 = e_67
| i4 = i5
| i4 = i6
| e_55 = e_57 ),
inference(forward_demodulation,[],[f3070,f648]) ).
fof(f3135,plain,
( e_55 = e_57
| i4 = i5
| i4 = i6
| e_55 = e_57
| i4 = i5
| i4 = i6
| e_55 = e_57 ),
inference(superposition,[],[f3069,f3075]) ).
fof(f3136,plain,
( i4 = i6
| i4 = i5
| e_55 = e_57 ),
inference(duplicate_literal_removal,[],[f3135]) ).
fof(f3157,plain,
( e_65 = select(a_56,i4)
| i4 = i5
| i4 = i5
| e_55 = e_57 ),
inference(superposition,[],[f118,f3136]) ).
fof(f3158,plain,
( e_63 = select(a_58,i4)
| i4 = i5
| i4 = i5
| e_55 = e_57 ),
inference(superposition,[],[f122,f3136]) ).
fof(f3194,plain,
( e_63 = select(a_58,i4)
| i4 = i5
| e_55 = e_57 ),
inference(duplicate_literal_removal,[],[f3158]) ).
fof(f3195,plain,
( e_65 = select(a_56,i4)
| i4 = i5
| e_55 = e_57 ),
inference(duplicate_literal_removal,[],[f3157]) ).
fof(f3197,plain,
( e_57 = e_63
| i4 = i5
| e_55 = e_57 ),
inference(forward_demodulation,[],[f3194,f56]) ).
fof(f3198,plain,
( e_55 = e_65
| i4 = i5
| e_55 = e_57 ),
inference(forward_demodulation,[],[f3195,f55]) ).
fof(f3202,plain,
( e_55 = e_63
| i4 = i5
| e_55 = e_57 ),
inference(forward_demodulation,[],[f3198,f1192]) ).
fof(f3250,plain,
( e_55 = e_57
| i4 = i5
| e_55 = e_57
| i4 = i5
| e_55 = e_57 ),
inference(superposition,[],[f3197,f3202]) ).
fof(f3251,plain,
( i4 = i5
| e_55 = e_57 ),
inference(duplicate_literal_removal,[],[f3250]) ).
fof(f3267,plain,
( e_59 = select(a_58,i4)
| e_55 = e_57 ),
inference(superposition,[],[f31,f3251]) ).
fof(f3268,plain,
( e_61 = select(a_56,i4)
| e_55 = e_57 ),
inference(superposition,[],[f32,f3251]) ).
fof(f3313,plain,
( e_55 = e_61
| e_55 = e_57 ),
inference(forward_demodulation,[],[f3268,f55]) ).
fof(f3314,plain,
( e_57 = e_59
| e_55 = e_57 ),
inference(forward_demodulation,[],[f3267,f56]) ).
fof(f3316,plain,
( e_55 = e_59
| e_55 = e_57 ),
inference(forward_demodulation,[],[f3313,f2078]) ).
fof(f3350,plain,
( e_55 = e_57
| e_55 = e_57
| e_55 = e_57 ),
inference(superposition,[],[f3314,f3316]) ).
fof(f3355,plain,
e_55 = e_57,
inference(duplicate_literal_removal,[],[f3350]) ).
fof(f3453,plain,
( e_51 = e_53
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| i3 = i8
| i3 = i9
| e_51 = e_53
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| i3 = i8
| i3 = i9
| e_51 = e_53 ),
inference(superposition,[],[f2849,f2850]) ).
fof(f3454,plain,
( i3 = i9
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| i3 = i8
| e_51 = e_53 ),
inference(duplicate_literal_removal,[],[f3453]) ).
fof(f3731,plain,
! [X0] :
( select(a_46,X0) = select(a_48,X0)
| i2 = X0
| i3 = X0
| i4 = X0
| i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i10 = X0 ),
inference(superposition,[],[f73,f2887]) ).
fof(f3732,plain,
( e_49 = select(a_48,i2)
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| i2 = i8
| i2 = i9
| i2 = i10 ),
inference(superposition,[],[f52,f2887]) ).
fof(f3733,plain,
( i2 = i10
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| i2 = i8
| i2 = i9
| e_47 = e_49 ),
inference(forward_demodulation,[],[f3732,f51]) ).
fof(f3815,plain,
( e_75 = select(a_52,i3)
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| i3 = i8
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| i3 = i8
| e_51 = e_53 ),
inference(superposition,[],[f428,f3454]) ).
fof(f3816,plain,
( e_75 = select(a_54,i3)
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| i3 = i8
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| i3 = i8
| e_51 = e_53 ),
inference(superposition,[],[f442,f3454]) ).
fof(f3833,plain,
( e_75 = select(a_54,i3)
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| i3 = i8
| e_51 = e_53 ),
inference(duplicate_literal_removal,[],[f3816]) ).
fof(f3834,plain,
( e_75 = select(a_52,i3)
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| i3 = i8
| e_51 = e_53 ),
inference(duplicate_literal_removal,[],[f3815]) ).
fof(f3849,plain,
( e_53 = e_75
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| i3 = i8
| e_51 = e_53 ),
inference(forward_demodulation,[],[f3833,f54]) ).
fof(f3850,plain,
( e_51 = e_75
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| i3 = i8
| e_51 = e_53 ),
inference(forward_demodulation,[],[f3834,f53]) ).
fof(f3972,plain,
( e_79 = select(a_48,i2)
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| i2 = i8
| i2 = i9
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| i2 = i8
| i2 = i9
| e_47 = e_49 ),
inference(superposition,[],[f668,f3733]) ).
fof(f3973,plain,
( e_79 = select(a_50,i2)
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| i2 = i8
| i2 = i9
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| i2 = i8
| i2 = i9
| e_47 = e_49 ),
inference(superposition,[],[f674,f3733]) ).
fof(f3990,plain,
( e_79 = select(a_50,i2)
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| i2 = i8
| i2 = i9
| e_47 = e_49 ),
inference(duplicate_literal_removal,[],[f3973]) ).
fof(f3991,plain,
( e_79 = select(a_48,i2)
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| i2 = i8
| i2 = i9
| e_47 = e_49 ),
inference(duplicate_literal_removal,[],[f3972]) ).
fof(f4014,plain,
( e_49 = e_79
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| i2 = i8
| i2 = i9
| e_47 = e_49 ),
inference(forward_demodulation,[],[f3990,f52]) ).
fof(f4015,plain,
( e_47 = e_79
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| i2 = i8
| i2 = i9
| e_47 = e_49 ),
inference(forward_demodulation,[],[f3991,f51]) ).
fof(f4039,plain,
! [X0] :
( select(a_44,X0) = select(a_46,X0)
| i2 = X0
| i2 = X0
| i3 = X0
| i4 = X0
| i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i10 = X0 ),
inference(superposition,[],[f72,f3731]) ).
fof(f4040,plain,
! [X0] :
( select(a_44,X0) = select(a_46,X0)
| i2 = X0
| i3 = X0
| i4 = X0
| i5 = X0
| i6 = X0
| i7 = X0
| i8 = X0
| i9 = X0
| i10 = X0 ),
inference(duplicate_literal_removal,[],[f4039]) ).
fof(f4349,plain,
( e_51 = e_53
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| i3 = i8
| e_51 = e_53
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| i3 = i8
| e_51 = e_53 ),
inference(superposition,[],[f3849,f3850]) ).
fof(f4350,plain,
( i3 = i8
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| e_51 = e_53 ),
inference(duplicate_literal_removal,[],[f4349]) ).
fof(f4377,plain,
( e_71 = select(a_52,i3)
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| e_51 = e_53 ),
inference(superposition,[],[f346,f4350]) ).
fof(f4379,plain,
( e_71 = select(a_54,i3)
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| e_51 = e_53 ),
inference(superposition,[],[f350,f4350]) ).
fof(f4399,plain,
( e_71 = select(a_54,i3)
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| e_51 = e_53 ),
inference(duplicate_literal_removal,[],[f4379]) ).
fof(f4400,plain,
( e_71 = select(a_52,i3)
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| e_51 = e_53 ),
inference(duplicate_literal_removal,[],[f4377]) ).
fof(f4411,plain,
( e_53 = e_71
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| e_51 = e_53 ),
inference(forward_demodulation,[],[f4399,f54]) ).
fof(f4412,plain,
( e_51 = e_71
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| e_51 = e_53 ),
inference(forward_demodulation,[],[f4400,f53]) ).
fof(f4496,plain,
( e_51 = e_53
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| e_51 = e_53
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i7
| e_51 = e_53 ),
inference(superposition,[],[f4411,f4412]) ).
fof(f4497,plain,
( i3 = i7
| i3 = i4
| i3 = i5
| i3 = i6
| e_51 = e_53 ),
inference(duplicate_literal_removal,[],[f4496]) ).
fof(f4520,plain,
( e_69 = select(a_52,i3)
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i4
| i3 = i5
| i3 = i6
| e_51 = e_53 ),
inference(superposition,[],[f207,f4497]) ).
fof(f4521,plain,
( e_67 = select(a_54,i3)
| i3 = i4
| i3 = i5
| i3 = i6
| i3 = i4
| i3 = i5
| i3 = i6
| e_51 = e_53 ),
inference(superposition,[],[f215,f4497]) ).
fof(f4555,plain,
( e_67 = select(a_54,i3)
| i3 = i4
| i3 = i5
| i3 = i6
| e_51 = e_53 ),
inference(duplicate_literal_removal,[],[f4521]) ).
fof(f4556,plain,
( e_69 = select(a_52,i3)
| i3 = i4
| i3 = i5
| i3 = i6
| e_51 = e_53 ),
inference(duplicate_literal_removal,[],[f4520]) ).
fof(f4564,plain,
( e_53 = e_67
| i3 = i4
| i3 = i5
| i3 = i6
| e_51 = e_53 ),
inference(forward_demodulation,[],[f4555,f54]) ).
fof(f4565,plain,
( e_51 = e_69
| i3 = i4
| i3 = i5
| i3 = i6
| e_51 = e_53 ),
inference(forward_demodulation,[],[f4556,f53]) ).
fof(f4571,plain,
( e_51 = e_67
| i3 = i4
| i3 = i5
| i3 = i6
| e_51 = e_53 ),
inference(forward_demodulation,[],[f4565,f648]) ).
fof(f4643,plain,
( e_51 = e_53
| i3 = i4
| i3 = i5
| i3 = i6
| e_51 = e_53
| i3 = i4
| i3 = i5
| i3 = i6
| e_51 = e_53 ),
inference(superposition,[],[f4564,f4571]) ).
fof(f4644,plain,
( i3 = i6
| i3 = i4
| i3 = i5
| e_51 = e_53 ),
inference(duplicate_literal_removal,[],[f4643]) ).
fof(f4667,plain,
( e_65 = select(a_52,i3)
| i3 = i4
| i3 = i5
| i3 = i4
| i3 = i5
| e_51 = e_53 ),
inference(superposition,[],[f120,f4644]) ).
fof(f4669,plain,
( e_63 = select(a_54,i3)
| i3 = i4
| i3 = i5
| i3 = i4
| i3 = i5
| e_51 = e_53 ),
inference(superposition,[],[f124,f4644]) ).
fof(f4709,plain,
( e_63 = select(a_54,i3)
| i3 = i4
| i3 = i5
| e_51 = e_53 ),
inference(duplicate_literal_removal,[],[f4669]) ).
fof(f4711,plain,
( e_65 = select(a_52,i3)
| i3 = i4
| i3 = i5
| e_51 = e_53 ),
inference(duplicate_literal_removal,[],[f4667]) ).
fof(f4715,plain,
( e_53 = e_63
| i3 = i4
| i3 = i5
| e_51 = e_53 ),
inference(forward_demodulation,[],[f4709,f54]) ).
fof(f4716,plain,
( e_51 = e_65
| i3 = i4
| i3 = i5
| e_51 = e_53 ),
inference(forward_demodulation,[],[f4711,f53]) ).
fof(f4721,plain,
( e_51 = e_63
| i3 = i4
| i3 = i5
| e_51 = e_53 ),
inference(forward_demodulation,[],[f4716,f1192]) ).
fof(f4781,plain,
( e_51 = e_53
| i3 = i4
| i3 = i5
| e_51 = e_53
| i3 = i4
| i3 = i5
| e_51 = e_53 ),
inference(superposition,[],[f4715,f4721]) ).
fof(f4782,plain,
( i3 = i5
| i3 = i4
| e_51 = e_53 ),
inference(duplicate_literal_removal,[],[f4781]) ).
fof(f4803,plain,
( e_61 = select(a_52,i3)
| i3 = i4
| i3 = i4
| e_51 = e_53 ),
inference(superposition,[],[f110,f4782]) ).
fof(f4804,plain,
( e_59 = select(a_54,i3)
| i3 = i4
| i3 = i4
| e_51 = e_53 ),
inference(superposition,[],[f114,f4782]) ).
fof(f4852,plain,
( e_59 = select(a_54,i3)
| i3 = i4
| e_51 = e_53 ),
inference(duplicate_literal_removal,[],[f4804]) ).
fof(f4853,plain,
( e_61 = select(a_52,i3)
| i3 = i4
| e_51 = e_53 ),
inference(duplicate_literal_removal,[],[f4803]) ).
fof(f4855,plain,
( e_53 = e_59
| i3 = i4
| e_51 = e_53 ),
inference(forward_demodulation,[],[f4852,f54]) ).
fof(f4856,plain,
( e_51 = e_61
| i3 = i4
| e_51 = e_53 ),
inference(forward_demodulation,[],[f4853,f53]) ).
fof(f4860,plain,
( e_51 = e_59
| i3 = i4
| e_51 = e_53 ),
inference(forward_demodulation,[],[f4856,f2078]) ).
fof(f4908,plain,
( e_51 = e_53
| i3 = i4
| e_51 = e_53
| i3 = i4
| e_51 = e_53 ),
inference(superposition,[],[f4855,f4860]) ).
fof(f4909,plain,
( i3 = i4
| e_51 = e_53 ),
inference(duplicate_literal_removal,[],[f4908]) ).
fof(f4925,plain,
( e_55 = select(a_54,i3)
| e_51 = e_53 ),
inference(superposition,[],[f29,f4909]) ).
fof(f4926,plain,
( e_57 = select(a_52,i3)
| e_51 = e_53 ),
inference(superposition,[],[f30,f4909]) ).
fof(f4985,plain,
( e_51 = e_57
| e_51 = e_53 ),
inference(forward_demodulation,[],[f4926,f53]) ).
fof(f4986,plain,
( e_53 = e_55
| e_51 = e_53 ),
inference(forward_demodulation,[],[f4925,f54]) ).
fof(f4988,plain,
( e_51 = e_55
| e_51 = e_53 ),
inference(forward_demodulation,[],[f4985,f3355]) ).
fof(f5028,plain,
( e_51 = e_53
| e_51 = e_53
| e_51 = e_53 ),
inference(superposition,[],[f4986,f4988]) ).
fof(f5033,plain,
e_51 = e_53,
inference(duplicate_literal_removal,[],[f5028]) ).
fof(f5127,plain,
( e_47 = e_49
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| i2 = i8
| i2 = i9
| e_47 = e_49
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| i2 = i8
| i2 = i9
| e_47 = e_49 ),
inference(superposition,[],[f4014,f4015]) ).
fof(f5128,plain,
( i2 = i9
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| i2 = i8
| e_47 = e_49 ),
inference(duplicate_literal_removal,[],[f5127]) ).
fof(f5432,plain,
( e_45 = select(a_44,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| i1 = i8
| i1 = i9
| i1 = i10 ),
inference(superposition,[],[f50,f4040]) ).
fof(f5433,plain,
( e_85 = select(a_44,i_83)
| i1 = i_83
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i10 = i_83 ),
inference(superposition,[],[f96,f4040]) ).
fof(f5434,plain,
( i1 = i10
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| i1 = i8
| i1 = i9
| e_43 = e_45 ),
inference(forward_demodulation,[],[f5432,f49]) ).
fof(f5529,plain,
( e_75 = select(a_48,i2)
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| i2 = i8
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| i2 = i8
| e_47 = e_49 ),
inference(superposition,[],[f577,f5128]) ).
fof(f5532,plain,
( e_75 = select(a_50,i2)
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| i2 = i8
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| i2 = i8
| e_47 = e_49 ),
inference(superposition,[],[f591,f5128]) ).
fof(f5549,plain,
( e_75 = select(a_50,i2)
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| i2 = i8
| e_47 = e_49 ),
inference(duplicate_literal_removal,[],[f5532]) ).
fof(f5550,plain,
( e_75 = select(a_48,i2)
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| i2 = i8
| e_47 = e_49 ),
inference(duplicate_literal_removal,[],[f5529]) ).
fof(f5569,plain,
( e_49 = e_75
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| i2 = i8
| e_47 = e_49 ),
inference(forward_demodulation,[],[f5549,f52]) ).
fof(f5570,plain,
( e_47 = e_75
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| i2 = i8
| e_47 = e_49 ),
inference(forward_demodulation,[],[f5550,f51]) ).
fof(f5706,plain,
( e_79 = select(a_44,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| i1 = i8
| i1 = i9
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| i1 = i8
| i1 = i9
| e_43 = e_45 ),
inference(superposition,[],[f826,f5434]) ).
fof(f5707,plain,
( e_79 = select(a_46,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| i1 = i8
| i1 = i9
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| i1 = i8
| i1 = i9
| e_43 = e_45 ),
inference(superposition,[],[f836,f5434]) ).
fof(f5726,plain,
( e_79 = select(a_46,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| i1 = i8
| i1 = i9
| e_43 = e_45 ),
inference(duplicate_literal_removal,[],[f5707]) ).
fof(f5727,plain,
( e_79 = select(a_44,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| i1 = i8
| i1 = i9
| e_43 = e_45 ),
inference(duplicate_literal_removal,[],[f5706]) ).
fof(f5754,plain,
( e_45 = e_79
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| i1 = i8
| i1 = i9
| e_43 = e_45 ),
inference(forward_demodulation,[],[f5726,f50]) ).
fof(f5755,plain,
( e_43 = e_79
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| i1 = i8
| i1 = i9
| e_43 = e_45 ),
inference(forward_demodulation,[],[f5727,f49]) ).
fof(f5769,plain,
( e_84 = e_85
| i1 = i_83
| i1 = i_83
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i10 = i_83 ),
inference(superposition,[],[f94,f5433]) ).
fof(f5770,plain,
( e_84 = e_85
| i1 = i_83
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i10 = i_83 ),
inference(duplicate_literal_removal,[],[f5769]) ).
fof(f5772,plain,
( i10 = i_83
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f5770,f47]) ).
fof(f5774,plain,
( e_85 = select(a_46,i10)
| i1 = i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(superposition,[],[f96,f5772]) ).
fof(f5775,plain,
( e_84 = select(a_44,i10)
| i1 = i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(superposition,[],[f94,f5772]) ).
fof(f5778,plain,
( i2 != i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f5772]) ).
fof(f5779,plain,
( i3 != i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f5772]) ).
fof(f5780,plain,
( i4 != i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f5772]) ).
fof(f5781,plain,
( i5 != i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f5772]) ).
fof(f5782,plain,
( i6 != i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f5772]) ).
fof(f5783,plain,
( i7 != i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f5772]) ).
fof(f5784,plain,
( i8 != i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f5772]) ).
fof(f5785,plain,
( i9 != i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f5772]) ).
fof(f5786,plain,
( i1 != i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f5772]) ).
fof(f5787,plain,
( e_84 = select(a_44,i10)
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f5775,f5786]) ).
fof(f5788,plain,
( e_85 = select(a_46,i10)
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f5774,f5786]) ).
fof(f6137,plain,
( e_79 = e_84
| i2 = i10
| i3 = i10
| i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| i9 = i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(superposition,[],[f826,f5787]) ).
fof(f6138,plain,
( e_79 = e_84
| i3 = i10
| i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| i9 = i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6137,f5778]) ).
fof(f6140,plain,
( e_79 = e_84
| i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| i9 = i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6138,f5779]) ).
fof(f6142,plain,
( e_79 = e_84
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| i9 = i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6140,f5780]) ).
fof(f6144,plain,
( e_79 = e_84
| i6 = i10
| i7 = i10
| i8 = i10
| i9 = i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6142,f5781]) ).
fof(f6146,plain,
( e_79 = e_84
| i7 = i10
| i8 = i10
| i9 = i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6144,f5782]) ).
fof(f6148,plain,
( e_79 = e_84
| i8 = i10
| i9 = i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6146,f5783]) ).
fof(f6150,plain,
( e_79 = e_84
| i9 = i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6148,f5784]) ).
fof(f6152,plain,
( i9 = i_83
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| e_79 = e_84
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6150,f5785]) ).
fof(f6252,plain,
( e_47 = e_49
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| i2 = i8
| e_47 = e_49
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| i2 = i8
| e_47 = e_49 ),
inference(superposition,[],[f5569,f5570]) ).
fof(f6253,plain,
( i2 = i8
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| e_47 = e_49 ),
inference(duplicate_literal_removal,[],[f6252]) ).
fof(f6414,plain,
( e_79 = e_85
| i2 = i10
| i3 = i10
| i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| i9 = i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(superposition,[],[f836,f5788]) ).
fof(f6415,plain,
( e_79 = e_85
| i3 = i10
| i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| i9 = i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6414,f5778]) ).
fof(f6417,plain,
( e_79 = e_85
| i4 = i10
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| i9 = i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6415,f5779]) ).
fof(f6419,plain,
( e_79 = e_85
| i5 = i10
| i6 = i10
| i7 = i10
| i8 = i10
| i9 = i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6417,f5780]) ).
fof(f6421,plain,
( e_79 = e_85
| i6 = i10
| i7 = i10
| i8 = i10
| i9 = i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6419,f5781]) ).
fof(f6423,plain,
( e_79 = e_85
| i7 = i10
| i8 = i10
| i9 = i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6421,f5782]) ).
fof(f6425,plain,
( e_79 = e_85
| i8 = i10
| i9 = i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6423,f5783]) ).
fof(f6427,plain,
( e_79 = e_85
| i9 = i10
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6425,f5784]) ).
fof(f6429,plain,
( e_79 = e_85
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6427,f5785]) ).
fof(f6443,plain,
( e_79 != e_84
| i2 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i9 = i_83
| i1 = i_83 ),
inference(superposition,[],[f47,f6429]) ).
fof(f6444,plain,
( i9 = i_83
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6443,f6152]) ).
fof(f6460,plain,
( e_84 = select(a_44,i9)
| i1 = i9
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f94,f6444]) ).
fof(f6461,plain,
( e_85 = select(a_46,i9)
| i1 = i9
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f96,f6444]) ).
fof(f6462,plain,
( i3 != i9
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f6444]) ).
fof(f6463,plain,
( i4 != i9
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f6444]) ).
fof(f6464,plain,
( i5 != i9
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f6444]) ).
fof(f6465,plain,
( i6 != i9
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f6444]) ).
fof(f6466,plain,
( i7 != i9
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f6444]) ).
fof(f6467,plain,
( i8 != i9
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f6444]) ).
fof(f6468,plain,
( i2 != i9
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f6444]) ).
fof(f6469,plain,
( i1 != i9
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f6444]) ).
fof(f6470,plain,
( e_85 = select(a_46,i9)
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6461,f6469]) ).
fof(f6471,plain,
( e_84 = select(a_44,i9)
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6460,f6469]) ).
fof(f6713,plain,
( e_43 = e_45
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| i1 = i8
| i1 = i9
| e_43 = e_45
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| i1 = i8
| i1 = i9
| e_43 = e_45 ),
inference(superposition,[],[f5754,f5755]) ).
fof(f6714,plain,
( i1 = i9
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| i1 = i8
| e_43 = e_45 ),
inference(duplicate_literal_removal,[],[f6713]) ).
fof(f6767,plain,
( e_75 = e_85
| i2 = i9
| i3 = i9
| i4 = i9
| i5 = i9
| i6 = i9
| i7 = i9
| i8 = i9
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f662,f6470]) ).
fof(f6768,plain,
( e_75 = e_85
| i3 = i9
| i4 = i9
| i5 = i9
| i6 = i9
| i7 = i9
| i8 = i9
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6767,f6468]) ).
fof(f6770,plain,
( e_75 = e_85
| i4 = i9
| i5 = i9
| i6 = i9
| i7 = i9
| i8 = i9
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6768,f6462]) ).
fof(f6772,plain,
( e_75 = e_85
| i5 = i9
| i6 = i9
| i7 = i9
| i8 = i9
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6770,f6463]) ).
fof(f6774,plain,
( e_75 = e_85
| i6 = i9
| i7 = i9
| i8 = i9
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6772,f6464]) ).
fof(f6776,plain,
( e_75 = e_85
| i7 = i9
| i8 = i9
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6774,f6465]) ).
fof(f6778,plain,
( e_75 = e_85
| i8 = i9
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6776,f6466]) ).
fof(f6780,plain,
( e_75 = e_85
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6778,f6467]) ).
fof(f6792,plain,
( e_75 != e_84
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f47,f6780]) ).
fof(f6819,plain,
( e_75 = e_84
| i2 = i9
| i3 = i9
| i4 = i9
| i5 = i9
| i6 = i9
| i7 = i9
| i8 = i9
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f656,f6471]) ).
fof(f6820,plain,
( i2 = i9
| i3 = i9
| i4 = i9
| i5 = i9
| i6 = i9
| i7 = i9
| i8 = i9
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6819,f6792]) ).
fof(f6822,plain,
( i3 = i9
| i4 = i9
| i5 = i9
| i6 = i9
| i7 = i9
| i8 = i9
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6820,f6468]) ).
fof(f6824,plain,
( i4 = i9
| i5 = i9
| i6 = i9
| i7 = i9
| i8 = i9
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6822,f6462]) ).
fof(f6826,plain,
( i5 = i9
| i6 = i9
| i7 = i9
| i8 = i9
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6824,f6463]) ).
fof(f6828,plain,
( i6 = i9
| i7 = i9
| i8 = i9
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6826,f6464]) ).
fof(f6830,plain,
( i7 = i9
| i8 = i9
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6828,f6465]) ).
fof(f6832,plain,
( i8 = i9
| i3 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i8 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6830,f6466]) ).
fof(f6834,plain,
( i8 = i_83
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6832,f6467]) ).
fof(f6849,plain,
( e_84 = select(a_44,i8)
| i1 = i8
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f94,f6834]) ).
fof(f6850,plain,
( e_85 = select(a_46,i8)
| i1 = i8
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f96,f6834]) ).
fof(f6851,plain,
( i4 != i8
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f6834]) ).
fof(f6852,plain,
( i5 != i8
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f6834]) ).
fof(f6853,plain,
( i6 != i8
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f6834]) ).
fof(f6854,plain,
( i7 != i8
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f6834]) ).
fof(f6855,plain,
( i3 != i8
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f6834]) ).
fof(f6856,plain,
( i2 != i8
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f6834]) ).
fof(f6857,plain,
( i1 != i8
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f6834]) ).
fof(f6858,plain,
( e_85 = select(a_46,i8)
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6850,f6857]) ).
fof(f6859,plain,
( e_84 = select(a_44,i8)
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f6849,f6857]) ).
fof(f7000,plain,
( e_71 = e_85
| i2 = i8
| i3 = i8
| i4 = i8
| i5 = i8
| i6 = i8
| i7 = i8
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f546,f6858]) ).
fof(f7001,plain,
( e_71 = e_85
| i3 = i8
| i4 = i8
| i5 = i8
| i6 = i8
| i7 = i8
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7000,f6856]) ).
fof(f7003,plain,
( e_71 = e_85
| i4 = i8
| i5 = i8
| i6 = i8
| i7 = i8
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7001,f6855]) ).
fof(f7005,plain,
( e_71 = e_85
| i5 = i8
| i6 = i8
| i7 = i8
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7003,f6851]) ).
fof(f7007,plain,
( e_71 = e_85
| i6 = i8
| i7 = i8
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7005,f6852]) ).
fof(f7009,plain,
( e_71 = e_85
| i7 = i8
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7007,f6853]) ).
fof(f7011,plain,
( e_71 = e_85
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7009,f6854]) ).
fof(f7039,plain,
( e_71 != e_84
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f47,f7011]) ).
fof(f7080,plain,
( e_71 = e_84
| i2 = i8
| i3 = i8
| i4 = i8
| i5 = i8
| i6 = i8
| i7 = i8
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f526,f6859]) ).
fof(f7081,plain,
( i2 = i8
| i3 = i8
| i4 = i8
| i5 = i8
| i6 = i8
| i7 = i8
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7080,f7039]) ).
fof(f7083,plain,
( i3 = i8
| i4 = i8
| i5 = i8
| i6 = i8
| i7 = i8
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7081,f6856]) ).
fof(f7085,plain,
( i4 = i8
| i5 = i8
| i6 = i8
| i7 = i8
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7083,f6855]) ).
fof(f7087,plain,
( i5 = i8
| i6 = i8
| i7 = i8
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7085,f6851]) ).
fof(f7089,plain,
( i6 = i8
| i7 = i8
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7087,f6852]) ).
fof(f7091,plain,
( i7 = i8
| i4 = i_83
| i5 = i_83
| i6 = i_83
| i7 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7089,f6853]) ).
fof(f7093,plain,
( i7 = i_83
| i5 = i_83
| i6 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7091,f6854]) ).
fof(f7109,plain,
( e_84 = select(a_44,i7)
| i1 = i7
| i5 = i_83
| i6 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f94,f7093]) ).
fof(f7110,plain,
( e_85 = select(a_46,i7)
| i1 = i7
| i5 = i_83
| i6 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f96,f7093]) ).
fof(f7111,plain,
( i5 != i7
| i5 = i_83
| i6 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f7093]) ).
fof(f7112,plain,
( i6 != i7
| i5 = i_83
| i6 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f7093]) ).
fof(f7113,plain,
( i4 != i7
| i5 = i_83
| i6 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f7093]) ).
fof(f7114,plain,
( i3 != i7
| i5 = i_83
| i6 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f7093]) ).
fof(f7115,plain,
( i2 != i7
| i5 = i_83
| i6 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f7093]) ).
fof(f7116,plain,
( i1 != i7
| i5 = i_83
| i6 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f7093]) ).
fof(f7117,plain,
( e_85 = select(a_46,i7)
| i5 = i_83
| i6 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7110,f7116]) ).
fof(f7118,plain,
( e_84 = select(a_44,i7)
| i5 = i_83
| i6 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7109,f7116]) ).
fof(f7149,plain,
( e_71 = select(a_48,i2)
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| e_47 = e_49 ),
inference(superposition,[],[f410,f6253]) ).
fof(f7150,plain,
( e_71 = select(a_50,i2)
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| e_47 = e_49 ),
inference(superposition,[],[f422,f6253]) ).
fof(f7185,plain,
( e_71 = select(a_50,i2)
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| e_47 = e_49 ),
inference(duplicate_literal_removal,[],[f7150]) ).
fof(f7186,plain,
( e_71 = select(a_48,i2)
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| e_47 = e_49 ),
inference(duplicate_literal_removal,[],[f7149]) ).
fof(f7200,plain,
( e_49 = e_71
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| e_47 = e_49 ),
inference(forward_demodulation,[],[f7185,f52]) ).
fof(f7201,plain,
( e_47 = e_71
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| e_47 = e_49 ),
inference(forward_demodulation,[],[f7186,f51]) ).
fof(f7281,plain,
( e_75 = select(a_44,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| i1 = i8
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| i1 = i8
| e_43 = e_45 ),
inference(superposition,[],[f656,f6714]) ).
fof(f7282,plain,
( e_75 = select(a_46,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| i1 = i8
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| i1 = i8
| e_43 = e_45 ),
inference(superposition,[],[f662,f6714]) ).
fof(f7325,plain,
( e_75 = select(a_46,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| i1 = i8
| e_43 = e_45 ),
inference(duplicate_literal_removal,[],[f7282]) ).
fof(f7326,plain,
( e_75 = select(a_44,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| i1 = i8
| e_43 = e_45 ),
inference(duplicate_literal_removal,[],[f7281]) ).
fof(f7348,plain,
( e_45 = e_75
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| i1 = i8
| e_43 = e_45 ),
inference(forward_demodulation,[],[f7325,f50]) ).
fof(f7349,plain,
( e_43 = e_75
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| i1 = i8
| e_43 = e_45 ),
inference(forward_demodulation,[],[f7326,f49]) ).
fof(f7466,plain,
( e_67 = e_85
| i2 = i7
| i3 = i7
| i4 = i7
| i5 = i7
| i6 = i7
| i5 = i_83
| i6 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f404,f7117]) ).
fof(f7467,plain,
( e_67 = e_85
| i3 = i7
| i4 = i7
| i5 = i7
| i6 = i7
| i5 = i_83
| i6 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7466,f7115]) ).
fof(f7469,plain,
( e_67 = e_85
| i4 = i7
| i5 = i7
| i6 = i7
| i5 = i_83
| i6 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7467,f7114]) ).
fof(f7471,plain,
( e_67 = e_85
| i5 = i7
| i6 = i7
| i5 = i_83
| i6 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7469,f7113]) ).
fof(f7473,plain,
( e_67 = e_85
| i6 = i7
| i5 = i_83
| i6 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7471,f7111]) ).
fof(f7475,plain,
( e_67 = e_85
| i5 = i_83
| i6 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7473,f7112]) ).
fof(f7499,plain,
( e_67 != e_84
| i5 = i_83
| i6 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f47,f7475]) ).
fof(f7571,plain,
( e_69 = e_84
| i2 = i7
| i3 = i7
| i4 = i7
| i5 = i7
| i6 = i7
| i5 = i_83
| i6 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f398,f7118]) ).
fof(f7572,plain,
( e_69 = e_84
| i3 = i7
| i4 = i7
| i5 = i7
| i6 = i7
| i5 = i_83
| i6 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7571,f7115]) ).
fof(f7574,plain,
( e_69 = e_84
| i4 = i7
| i5 = i7
| i6 = i7
| i5 = i_83
| i6 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7572,f7114]) ).
fof(f7576,plain,
( e_69 = e_84
| i5 = i7
| i6 = i7
| i5 = i_83
| i6 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7574,f7113]) ).
fof(f7578,plain,
( e_69 = e_84
| i6 = i7
| i5 = i_83
| i6 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7576,f7111]) ).
fof(f7580,plain,
( e_69 = e_84
| i5 = i_83
| i6 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7578,f7112]) ).
fof(f7582,plain,
( e_67 = e_84
| i5 = i_83
| i6 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_demodulation,[],[f7580,f648]) ).
fof(f7584,plain,
( i6 = i_83
| i5 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7582,f7499]) ).
fof(f7626,plain,
( e_84 = select(a_44,i6)
| i1 = i6
| i5 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f94,f7584]) ).
fof(f7627,plain,
( e_85 = select(a_46,i6)
| i1 = i6
| i5 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f96,f7584]) ).
fof(f7628,plain,
( i5 != i6
| i5 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f7584]) ).
fof(f7629,plain,
( i4 != i6
| i5 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f7584]) ).
fof(f7630,plain,
( i3 != i6
| i5 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f7584]) ).
fof(f7631,plain,
( i2 != i6
| i5 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f7584]) ).
fof(f7632,plain,
( i1 != i6
| i5 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f7584]) ).
fof(f7634,plain,
( e_85 = select(a_46,i6)
| i5 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7627,f7632]) ).
fof(f7635,plain,
( e_84 = select(a_44,i6)
| i5 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7626,f7632]) ).
fof(f7801,plain,
( e_47 = e_49
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| e_47 = e_49
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i7
| e_47 = e_49 ),
inference(superposition,[],[f7200,f7201]) ).
fof(f7802,plain,
( i2 = i7
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| e_47 = e_49 ),
inference(duplicate_literal_removal,[],[f7801]) ).
fof(f7844,plain,
( e_63 = e_85
| i2 = i6
| i3 = i6
| i4 = i6
| i5 = i6
| i5 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f307,f7634]) ).
fof(f7845,plain,
( e_63 = e_85
| i3 = i6
| i4 = i6
| i5 = i6
| i5 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7844,f7631]) ).
fof(f7847,plain,
( e_63 = e_85
| i4 = i6
| i5 = i6
| i5 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7845,f7630]) ).
fof(f7849,plain,
( e_63 = e_85
| i5 = i6
| i5 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7847,f7629]) ).
fof(f7851,plain,
( e_63 = e_85
| i5 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7849,f7628]) ).
fof(f7873,plain,
( e_63 != e_84
| i5 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f47,f7851]) ).
fof(f7918,plain,
( e_65 = e_84
| i2 = i6
| i3 = i6
| i4 = i6
| i5 = i6
| i5 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f293,f7635]) ).
fof(f7919,plain,
( e_65 = e_84
| i3 = i6
| i4 = i6
| i5 = i6
| i5 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7918,f7631]) ).
fof(f7921,plain,
( e_65 = e_84
| i4 = i6
| i5 = i6
| i5 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7919,f7630]) ).
fof(f7923,plain,
( e_65 = e_84
| i5 = i6
| i5 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7921,f7629]) ).
fof(f7925,plain,
( e_65 = e_84
| i5 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7923,f7628]) ).
fof(f7927,plain,
( e_63 = e_84
| i5 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_demodulation,[],[f7925,f1192]) ).
fof(f7929,plain,
( i5 = i_83
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7927,f7873]) ).
fof(f7956,plain,
( e_84 = select(a_44,i5)
| i1 = i5
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f94,f7929]) ).
fof(f7957,plain,
( e_85 = select(a_46,i5)
| i1 = i5
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f96,f7929]) ).
fof(f7958,plain,
( i4 != i5
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f7929]) ).
fof(f7959,plain,
( i3 != i5
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f7929]) ).
fof(f7960,plain,
( i2 != i5
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f7929]) ).
fof(f7961,plain,
( i1 != i5
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f7929]) ).
fof(f7963,plain,
( e_85 = select(a_46,i5)
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7957,f7961]) ).
fof(f7964,plain,
( e_84 = select(a_44,i5)
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f7956,f7961]) ).
fof(f8098,plain,
( e_59 = e_85
| i2 = i5
| i3 = i5
| i4 = i5
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f191,f7963]) ).
fof(f8099,plain,
( e_59 = e_85
| i3 = i5
| i4 = i5
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f8098,f7960]) ).
fof(f8101,plain,
( e_59 = e_85
| i4 = i5
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f8099,f7959]) ).
fof(f8103,plain,
( e_59 = e_85
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f8101,f7958]) ).
fof(f8126,plain,
( e_59 != e_84
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f47,f8103]) ).
fof(f8237,plain,
( e_43 = e_45
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| i1 = i8
| e_43 = e_45
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| i1 = i8
| e_43 = e_45 ),
inference(superposition,[],[f7348,f7349]) ).
fof(f8238,plain,
( i1 = i8
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| e_43 = e_45 ),
inference(duplicate_literal_removal,[],[f8237]) ).
fof(f8243,plain,
( e_61 = e_84
| i2 = i5
| i3 = i5
| i4 = i5
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f188,f7964]) ).
fof(f8244,plain,
( e_61 = e_84
| i3 = i5
| i4 = i5
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f8243,f7960]) ).
fof(f8246,plain,
( e_61 = e_84
| i4 = i5
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f8244,f7959]) ).
fof(f8248,plain,
( e_61 = e_84
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f8246,f7958]) ).
fof(f8250,plain,
( e_59 = e_84
| i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_demodulation,[],[f8248,f2078]) ).
fof(f8252,plain,
( i4 = i_83
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f8250,f8126]) ).
fof(f8274,plain,
( e_84 = select(a_44,i4)
| i1 = i4
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f94,f8252]) ).
fof(f8275,plain,
( e_85 = select(a_46,i4)
| i1 = i4
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f96,f8252]) ).
fof(f8276,plain,
( i3 != i4
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f8252]) ).
fof(f8277,plain,
( i2 != i4
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f8252]) ).
fof(f8278,plain,
( i1 != i4
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f8252]) ).
fof(f8280,plain,
( e_85 = select(a_46,i4)
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f8275,f8278]) ).
fof(f8281,plain,
( e_84 = select(a_44,i4)
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f8274,f8278]) ).
fof(f8358,plain,
( e_55 = e_85
| i2 = i4
| i3 = i4
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f108,f8280]) ).
fof(f8359,plain,
( e_55 = e_85
| i3 = i4
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f8358,f8277]) ).
fof(f8361,plain,
( e_55 = e_85
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f8359,f8276]) ).
fof(f8381,plain,
( e_55 != e_84
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f47,f8361]) ).
fof(f8426,plain,
( e_57 = e_84
| i2 = i4
| i3 = i4
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f104,f8281]) ).
fof(f8427,plain,
( e_57 = e_84
| i3 = i4
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f8426,f8277]) ).
fof(f8429,plain,
( e_57 = e_84
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f8427,f8276]) ).
fof(f8431,plain,
( e_55 = e_84
| i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_demodulation,[],[f8429,f3355]) ).
fof(f8433,plain,
( i3 = i_83
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f8431,f8381]) ).
fof(f8458,plain,
( e_84 = select(a_44,i3)
| i1 = i3
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f94,f8433]) ).
fof(f8459,plain,
( e_85 = select(a_46,i3)
| i1 = i3
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f96,f8433]) ).
fof(f8460,plain,
( i2 != i3
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f8433]) ).
fof(f8461,plain,
( i1 != i3
| i2 = i_83
| i1 = i_83 ),
inference(equality_factoring,[],[f8433]) ).
fof(f8463,plain,
( e_85 = select(a_46,i3)
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f8459,f8461]) ).
fof(f8464,plain,
( e_84 = select(a_44,i3)
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f8458,f8461]) ).
fof(f8530,plain,
( e_51 = e_85
| i2 = i3
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f100,f8463]) ).
fof(f8531,plain,
( e_51 = e_85
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f8530,f8460]) ).
fof(f8560,plain,
( e_51 != e_84
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f47,f8531]) ).
fof(f8613,plain,
( e_53 = e_84
| i2 = i3
| i2 = i_83
| i1 = i_83 ),
inference(superposition,[],[f98,f8464]) ).
fof(f8614,plain,
( e_53 = e_84
| i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f8613,f8460]) ).
fof(f8616,plain,
( e_51 = e_84
| i2 = i_83
| i1 = i_83 ),
inference(forward_demodulation,[],[f8614,f5033]) ).
fof(f8618,plain,
( i2 = i_83
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f8616,f8560]) ).
fof(f8642,plain,
( select(a_44,i2) = e_84
| i1 = i2
| i1 = i_83 ),
inference(superposition,[],[f94,f8618]) ).
fof(f8643,plain,
( select(a_46,i2) = e_85
| i1 = i2
| i1 = i_83 ),
inference(superposition,[],[f96,f8618]) ).
fof(f8644,plain,
( i1 != i2
| i1 = i_83 ),
inference(equality_factoring,[],[f8618]) ).
fof(f8646,plain,
( select(a_46,i2) = e_85
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f8643,f8644]) ).
fof(f8647,plain,
( select(a_44,i2) = e_84
| i1 = i_83 ),
inference(forward_subsumption_resolution,[],[f8642,f8644]) ).
fof(f8648,plain,
( e_47 = e_85
| i1 = i_83 ),
inference(forward_demodulation,[],[f8646,f25]) ).
fof(f8649,plain,
( i1 = i_83
| e_49 = e_84 ),
inference(forward_demodulation,[],[f8647,f26]) ).
fof(f8678,plain,
( e_47 != e_84
| i1 = i_83 ),
inference(superposition,[],[f47,f8648]) ).
fof(f8721,plain,
( select(a1,i1) = e_84
| e_49 = e_84 ),
inference(superposition,[],[f43,f8649]) ).
fof(f8722,plain,
( select(a2,i1) = e_85
| e_49 = e_84 ),
inference(superposition,[],[f44,f8649]) ).
fof(f8724,plain,
( e_43 = e_85
| e_49 = e_84 ),
inference(forward_demodulation,[],[f8722,f23]) ).
fof(f8725,plain,
( e_49 = e_84
| e_45 = e_84 ),
inference(forward_demodulation,[],[f8721,f24]) ).
fof(f8749,plain,
( e_69 = select(a_48,i2)
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| e_47 = e_49 ),
inference(superposition,[],[f325,f7802]) ).
fof(f8750,plain,
( e_67 = select(a_50,i2)
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| e_47 = e_49 ),
inference(superposition,[],[f333,f7802]) ).
fof(f8799,plain,
( e_67 = select(a_50,i2)
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| e_47 = e_49 ),
inference(duplicate_literal_removal,[],[f8750]) ).
fof(f8800,plain,
( e_69 = select(a_48,i2)
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| e_47 = e_49 ),
inference(duplicate_literal_removal,[],[f8749]) ).
fof(f8811,plain,
( e_49 = e_67
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| e_47 = e_49 ),
inference(forward_demodulation,[],[f8799,f52]) ).
fof(f8812,plain,
( e_47 = e_69
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| e_47 = e_49 ),
inference(forward_demodulation,[],[f8800,f51]) ).
fof(f8819,plain,
( e_47 = e_67
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| e_47 = e_49 ),
inference(forward_demodulation,[],[f8812,f648]) ).
fof(f8829,plain,
( e_43 != e_84
| e_49 = e_84 ),
inference(superposition,[],[f47,f8724]) ).
fof(f8855,plain,
( e_47 != e_49
| i1 = i_83
| e_45 = e_84 ),
inference(superposition,[],[f8678,f8725]) ).
fof(f8899,plain,
( e_71 = select(a_44,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| e_43 = e_45 ),
inference(superposition,[],[f526,f8238]) ).
fof(f8900,plain,
( e_71 = select(a_46,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| e_43 = e_45 ),
inference(superposition,[],[f546,f8238]) ).
fof(f8939,plain,
( e_71 = select(a_46,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| e_43 = e_45 ),
inference(duplicate_literal_removal,[],[f8900]) ).
fof(f8940,plain,
( e_71 = select(a_44,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| e_43 = e_45 ),
inference(duplicate_literal_removal,[],[f8899]) ).
fof(f8957,plain,
( e_45 = e_71
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| e_43 = e_45 ),
inference(forward_demodulation,[],[f8939,f50]) ).
fof(f8958,plain,
( e_43 = e_71
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| e_43 = e_45 ),
inference(forward_demodulation,[],[f8940,f49]) ).
fof(f9074,plain,
( e_47 = e_49
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| e_47 = e_49
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i6
| e_47 = e_49 ),
inference(superposition,[],[f8811,f8819]) ).
fof(f9075,plain,
( i2 = i6
| i2 = i3
| i2 = i4
| i2 = i5
| e_47 = e_49 ),
inference(duplicate_literal_removal,[],[f9074]) ).
fof(f9114,plain,
( e_65 = select(a_48,i2)
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i3
| i2 = i4
| i2 = i5
| e_47 = e_49 ),
inference(superposition,[],[f195,f9075]) ).
fof(f9115,plain,
( e_63 = select(a_50,i2)
| i2 = i3
| i2 = i4
| i2 = i5
| i2 = i3
| i2 = i4
| i2 = i5
| e_47 = e_49 ),
inference(superposition,[],[f201,f9075]) ).
fof(f9169,plain,
( e_63 = select(a_50,i2)
| i2 = i3
| i2 = i4
| i2 = i5
| e_47 = e_49 ),
inference(duplicate_literal_removal,[],[f9115]) ).
fof(f9170,plain,
( e_65 = select(a_48,i2)
| i2 = i3
| i2 = i4
| i2 = i5
| e_47 = e_49 ),
inference(duplicate_literal_removal,[],[f9114]) ).
fof(f9178,plain,
( e_49 = e_63
| i2 = i3
| i2 = i4
| i2 = i5
| e_47 = e_49 ),
inference(forward_demodulation,[],[f9169,f52]) ).
fof(f9179,plain,
( e_47 = e_65
| i2 = i3
| i2 = i4
| i2 = i5
| e_47 = e_49 ),
inference(forward_demodulation,[],[f9170,f51]) ).
fof(f9185,plain,
( e_47 = e_63
| i2 = i3
| i2 = i4
| i2 = i5
| e_47 = e_49 ),
inference(forward_demodulation,[],[f9179,f1192]) ).
fof(f9265,plain,
( e_47 = e_49
| i2 = i3
| i2 = i4
| i2 = i5
| e_47 = e_49
| i2 = i3
| i2 = i4
| i2 = i5
| e_47 = e_49 ),
inference(superposition,[],[f9178,f9185]) ).
fof(f9266,plain,
( i2 = i5
| i2 = i3
| i2 = i4
| e_47 = e_49 ),
inference(duplicate_literal_removal,[],[f9265]) ).
fof(f9297,plain,
( e_61 = select(a_48,i2)
| i2 = i3
| i2 = i4
| i2 = i3
| i2 = i4
| e_47 = e_49 ),
inference(superposition,[],[f112,f9266]) ).
fof(f9299,plain,
( e_59 = select(a_50,i2)
| i2 = i3
| i2 = i4
| i2 = i3
| i2 = i4
| e_47 = e_49 ),
inference(superposition,[],[f116,f9266]) ).
fof(f9360,plain,
( e_59 = select(a_50,i2)
| i2 = i3
| i2 = i4
| e_47 = e_49 ),
inference(duplicate_literal_removal,[],[f9299]) ).
fof(f9362,plain,
( e_61 = select(a_48,i2)
| i2 = i3
| i2 = i4
| e_47 = e_49 ),
inference(duplicate_literal_removal,[],[f9297]) ).
fof(f9366,plain,
( e_49 = e_59
| i2 = i3
| i2 = i4
| e_47 = e_49 ),
inference(forward_demodulation,[],[f9360,f52]) ).
fof(f9367,plain,
( e_47 = e_61
| i2 = i3
| i2 = i4
| e_47 = e_49 ),
inference(forward_demodulation,[],[f9362,f51]) ).
fof(f9372,plain,
( e_47 = e_59
| i2 = i3
| i2 = i4
| e_47 = e_49 ),
inference(forward_demodulation,[],[f9367,f2078]) ).
fof(f9448,plain,
( e_47 = e_49
| i2 = i3
| i2 = i4
| e_47 = e_49
| i2 = i3
| i2 = i4
| e_47 = e_49 ),
inference(superposition,[],[f9366,f9372]) ).
fof(f9449,plain,
( i2 = i4
| i2 = i3
| e_47 = e_49 ),
inference(duplicate_literal_removal,[],[f9448]) ).
fof(f9478,plain,
( e_57 = select(a_48,i2)
| i2 = i3
| i2 = i3
| e_47 = e_49 ),
inference(superposition,[],[f102,f9449]) ).
fof(f9479,plain,
( e_55 = select(a_50,i2)
| i2 = i3
| i2 = i3
| e_47 = e_49 ),
inference(superposition,[],[f106,f9449]) ).
fof(f9549,plain,
( e_55 = select(a_50,i2)
| i2 = i3
| e_47 = e_49 ),
inference(duplicate_literal_removal,[],[f9479]) ).
fof(f9550,plain,
( e_57 = select(a_48,i2)
| i2 = i3
| e_47 = e_49 ),
inference(duplicate_literal_removal,[],[f9478]) ).
fof(f9552,plain,
( e_49 = e_55
| i2 = i3
| e_47 = e_49 ),
inference(forward_demodulation,[],[f9549,f52]) ).
fof(f9553,plain,
( e_47 = e_57
| i2 = i3
| e_47 = e_49 ),
inference(forward_demodulation,[],[f9550,f51]) ).
fof(f9557,plain,
( e_47 = e_55
| i2 = i3
| e_47 = e_49 ),
inference(forward_demodulation,[],[f9553,f3355]) ).
fof(f9621,plain,
( e_47 = e_49
| i2 = i3
| e_47 = e_49
| i2 = i3
| e_47 = e_49 ),
inference(superposition,[],[f9552,f9557]) ).
fof(f9622,plain,
( i2 = i3
| e_47 = e_49 ),
inference(duplicate_literal_removal,[],[f9621]) ).
fof(f9646,plain,
( e_51 = select(a_50,i2)
| e_47 = e_49 ),
inference(superposition,[],[f27,f9622]) ).
fof(f9647,plain,
( e_53 = select(a_48,i2)
| e_47 = e_49 ),
inference(superposition,[],[f28,f9622]) ).
fof(f9729,plain,
( e_47 = e_53
| e_47 = e_49 ),
inference(forward_demodulation,[],[f9647,f51]) ).
fof(f9730,plain,
( e_49 = e_51
| e_47 = e_49 ),
inference(forward_demodulation,[],[f9646,f52]) ).
fof(f9732,plain,
( e_47 = e_51
| e_47 = e_49 ),
inference(forward_demodulation,[],[f9729,f5033]) ).
fof(f9768,plain,
( e_47 = e_49
| e_47 = e_49
| e_47 = e_49 ),
inference(superposition,[],[f9730,f9732]) ).
fof(f9773,plain,
e_47 = e_49,
inference(duplicate_literal_removal,[],[f9768]) ).
fof(f9820,plain,
( e_47 != e_47
| i1 = i_83
| e_45 = e_84 ),
inference(superposition,[],[f8855,f9773]) ).
fof(f9822,plain,
( i1 = i_83
| e_45 = e_84 ),
inference(trivial_inequality_removal,[],[f9820]) ).
fof(f9864,plain,
( e_43 = e_45
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| e_43 = e_45
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i7
| e_43 = e_45 ),
inference(superposition,[],[f8957,f8958]) ).
fof(f9865,plain,
( i1 = i7
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| e_43 = e_45 ),
inference(duplicate_literal_removal,[],[f9864]) ).
fof(f9892,plain,
( select(a1,i1) = e_84
| e_45 = e_84 ),
inference(superposition,[],[f43,f9822]) ).
fof(f9896,plain,
( e_45 = e_84
| e_45 = e_84 ),
inference(forward_demodulation,[],[f9892,f24]) ).
fof(f9897,plain,
e_45 = e_84,
inference(duplicate_literal_removal,[],[f9896]) ).
fof(f9918,plain,
( e_45 != e_47
| i1 = i_83 ),
inference(superposition,[],[f8678,f9897]) ).
fof(f9919,plain,
( e_43 != e_45
| e_45 = e_49 ),
inference(superposition,[],[f8829,f9897]) ).
fof(f9920,plain,
( e_43 != e_45
| e_45 = e_47 ),
inference(forward_demodulation,[],[f9919,f9773]) ).
fof(f10339,plain,
( e_69 = select(a_44,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| e_43 = e_45 ),
inference(superposition,[],[f398,f9865]) ).
fof(f10340,plain,
( e_67 = select(a_46,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| e_43 = e_45 ),
inference(superposition,[],[f404,f9865]) ).
fof(f10393,plain,
( e_67 = select(a_46,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| e_43 = e_45 ),
inference(duplicate_literal_removal,[],[f10340]) ).
fof(f10394,plain,
( e_69 = select(a_44,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| e_43 = e_45 ),
inference(duplicate_literal_removal,[],[f10339]) ).
fof(f10408,plain,
( e_45 = e_67
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| e_43 = e_45 ),
inference(forward_demodulation,[],[f10393,f50]) ).
fof(f10409,plain,
( e_43 = e_69
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| e_43 = e_45 ),
inference(forward_demodulation,[],[f10394,f49]) ).
fof(f10417,plain,
( e_43 = e_67
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| e_43 = e_45 ),
inference(forward_demodulation,[],[f10409,f648]) ).
fof(f11003,plain,
( e_43 = e_45
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| e_43 = e_45
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i6
| e_43 = e_45 ),
inference(superposition,[],[f10408,f10417]) ).
fof(f11004,plain,
( i1 = i6
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| e_43 = e_45 ),
inference(duplicate_literal_removal,[],[f11003]) ).
fof(f11092,plain,
( e_65 = select(a_44,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| e_43 = e_45 ),
inference(superposition,[],[f293,f11004]) ).
fof(f11093,plain,
( e_63 = select(a_46,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| e_43 = e_45 ),
inference(superposition,[],[f307,f11004]) ).
fof(f11151,plain,
( e_63 = select(a_46,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| e_43 = e_45 ),
inference(duplicate_literal_removal,[],[f11093]) ).
fof(f11152,plain,
( e_65 = select(a_44,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| e_43 = e_45 ),
inference(duplicate_literal_removal,[],[f11092]) ).
fof(f11163,plain,
( e_45 = e_63
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| e_43 = e_45 ),
inference(forward_demodulation,[],[f11151,f50]) ).
fof(f11164,plain,
( e_43 = e_65
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| e_43 = e_45 ),
inference(forward_demodulation,[],[f11152,f49]) ).
fof(f11171,plain,
( e_43 = e_63
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| e_43 = e_45 ),
inference(forward_demodulation,[],[f11164,f1192]) ).
fof(f11273,plain,
( e_43 = e_45
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| e_43 = e_45
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i5
| e_43 = e_45 ),
inference(superposition,[],[f11163,f11171]) ).
fof(f11274,plain,
( i1 = i5
| i1 = i2
| i1 = i3
| i1 = i4
| e_43 = e_45 ),
inference(duplicate_literal_removal,[],[f11273]) ).
fof(f11309,plain,
( e_61 = select(a_44,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i2
| i1 = i3
| i1 = i4
| e_43 = e_45 ),
inference(superposition,[],[f188,f11274]) ).
fof(f11310,plain,
( e_59 = select(a_46,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| i1 = i2
| i1 = i3
| i1 = i4
| e_43 = e_45 ),
inference(superposition,[],[f191,f11274]) ).
fof(f11375,plain,
( e_59 = select(a_46,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| e_43 = e_45 ),
inference(duplicate_literal_removal,[],[f11310]) ).
fof(f11376,plain,
( e_61 = select(a_44,i1)
| i1 = i2
| i1 = i3
| i1 = i4
| e_43 = e_45 ),
inference(duplicate_literal_removal,[],[f11309]) ).
fof(f11384,plain,
( e_45 = e_59
| i1 = i2
| i1 = i3
| i1 = i4
| e_43 = e_45 ),
inference(forward_demodulation,[],[f11375,f50]) ).
fof(f11385,plain,
( e_43 = e_61
| i1 = i2
| i1 = i3
| i1 = i4
| e_43 = e_45 ),
inference(forward_demodulation,[],[f11376,f49]) ).
fof(f11391,plain,
( e_43 = e_59
| i1 = i2
| i1 = i3
| i1 = i4
| e_43 = e_45 ),
inference(forward_demodulation,[],[f11385,f2078]) ).
fof(f11481,plain,
( e_43 = e_45
| i1 = i2
| i1 = i3
| i1 = i4
| e_43 = e_45
| i1 = i2
| i1 = i3
| i1 = i4
| e_43 = e_45 ),
inference(superposition,[],[f11384,f11391]) ).
fof(f11482,plain,
( i1 = i4
| i1 = i2
| i1 = i3
| e_43 = e_45 ),
inference(duplicate_literal_removal,[],[f11481]) ).
fof(f11513,plain,
( e_57 = select(a_44,i1)
| i1 = i2
| i1 = i3
| i1 = i2
| i1 = i3
| e_43 = e_45 ),
inference(superposition,[],[f104,f11482]) ).
fof(f11515,plain,
( e_55 = select(a_46,i1)
| i1 = i2
| i1 = i3
| i1 = i2
| i1 = i3
| e_43 = e_45 ),
inference(superposition,[],[f108,f11482]) ).
fof(f11589,plain,
( e_55 = select(a_46,i1)
| i1 = i2
| i1 = i3
| e_43 = e_45 ),
inference(duplicate_literal_removal,[],[f11515]) ).
fof(f11591,plain,
( e_57 = select(a_44,i1)
| i1 = i2
| i1 = i3
| e_43 = e_45 ),
inference(duplicate_literal_removal,[],[f11513]) ).
fof(f11595,plain,
( e_45 = e_55
| i1 = i2
| i1 = i3
| e_43 = e_45 ),
inference(forward_demodulation,[],[f11589,f50]) ).
fof(f11596,plain,
( e_43 = e_57
| i1 = i2
| i1 = i3
| e_43 = e_45 ),
inference(forward_demodulation,[],[f11591,f49]) ).
fof(f11601,plain,
( e_43 = e_55
| i1 = i2
| i1 = i3
| e_43 = e_45 ),
inference(forward_demodulation,[],[f11596,f3355]) ).
fof(f11679,plain,
( e_43 = e_45
| i1 = i2
| i1 = i3
| e_43 = e_45
| i1 = i2
| i1 = i3
| e_43 = e_45 ),
inference(superposition,[],[f11595,f11601]) ).
fof(f11680,plain,
( i1 = i3
| i1 = i2
| e_43 = e_45 ),
inference(duplicate_literal_removal,[],[f11679]) ).
fof(f11709,plain,
( e_53 = select(a_44,i1)
| i1 = i2
| i1 = i2
| e_43 = e_45 ),
inference(superposition,[],[f98,f11680]) ).
fof(f11710,plain,
( e_51 = select(a_46,i1)
| i1 = i2
| i1 = i2
| e_43 = e_45 ),
inference(superposition,[],[f100,f11680]) ).
fof(f11795,plain,
( e_51 = select(a_46,i1)
| i1 = i2
| e_43 = e_45 ),
inference(duplicate_literal_removal,[],[f11710]) ).
fof(f11796,plain,
( e_53 = select(a_44,i1)
| i1 = i2
| e_43 = e_45 ),
inference(duplicate_literal_removal,[],[f11709]) ).
fof(f11798,plain,
( e_45 = e_51
| i1 = i2
| e_43 = e_45 ),
inference(forward_demodulation,[],[f11795,f50]) ).
fof(f11799,plain,
( e_43 = e_53
| i1 = i2
| e_43 = e_45 ),
inference(forward_demodulation,[],[f11796,f49]) ).
fof(f11803,plain,
( e_43 = e_51
| i1 = i2
| e_43 = e_45 ),
inference(forward_demodulation,[],[f11799,f5033]) ).
fof(f11861,plain,
( e_43 = e_45
| i1 = i2
| e_43 = e_45
| i1 = i2
| e_43 = e_45 ),
inference(superposition,[],[f11798,f11803]) ).
fof(f11862,plain,
( i1 = i2
| e_43 = e_45 ),
inference(duplicate_literal_removal,[],[f11861]) ).
fof(f11875,plain,
( e_47 = select(a_46,i1)
| e_43 = e_45 ),
inference(superposition,[],[f25,f11862]) ).
fof(f11876,plain,
( e_49 = select(a_44,i1)
| e_43 = e_45 ),
inference(superposition,[],[f26,f11862]) ).
fof(f11973,plain,
( e_43 = e_49
| e_43 = e_45 ),
inference(forward_demodulation,[],[f11876,f49]) ).
fof(f11974,plain,
( e_45 = e_47
| e_43 = e_45 ),
inference(forward_demodulation,[],[f11875,f50]) ).
fof(f11976,plain,
( e_43 = e_47
| e_43 = e_45 ),
inference(forward_demodulation,[],[f11973,f9773]) ).
fof(f11977,plain,
e_45 = e_47,
inference(forward_subsumption_resolution,[],[f11974,f9920]) ).
fof(f11992,plain,
( e_45 != e_45
| i1 = i_83 ),
inference(superposition,[],[f9918,f11977]) ).
fof(f11993,plain,
i1 = i_83,
inference(trivial_inequality_removal,[],[f11992]) ).
fof(f12031,plain,
select(a2,i1) = e_85,
inference(superposition,[],[f44,f11993]) ).
fof(f12033,plain,
e_43 = e_85,
inference(forward_demodulation,[],[f12031,f23]) ).
fof(f12064,plain,
e_43 != e_84,
inference(superposition,[],[f47,f12033]) ).
fof(f12074,plain,
e_43 != e_45,
inference(forward_demodulation,[],[f12064,f9897]) ).
fof(f13038,plain,
( e_43 = e_45
| e_43 = e_45 ),
inference(superposition,[],[f11977,f11976]) ).
fof(f13039,plain,
e_43 = e_45,
inference(duplicate_literal_removal,[],[f13038]) ).
fof(f13041,plain,
$false,
inference(forward_subsumption_resolution,[],[f13039,f12074]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV555-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n018.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 11:47:55 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.59/2.39 % (3322970)Will run a generic schedule for satisfiability detection.
% 14.59/2.39 % (3322978)dis+10_1_sil=32000:sp=arity:random_seed=335283928:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.59/2.39 % (3322976)% WARNING: option uhcvi not known.
% 14.59/2.39 % (3322976)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=705984768:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.59/2.39 % (3322975)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1830104572_2999 on theBenchmark for (2999ds/0Mi)
% 14.59/2.39 % (3322979)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3911471943:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.59/2.39 % (3322980)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3437716309:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.59/2.39 % (3322977)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1630304767:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.59/2.39 % (3322981)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1154696614:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.59/2.39 % TRYING [1]
% 14.59/2.39 % TRYING [2]
% 14.59/2.39 % TRYING [3]
% 14.59/2.39 % TRYING [4]
% 14.59/2.39 % (3322978)Instruction limit reached!
% 14.59/2.39 % (3322978)------------------------------
% 14.59/2.39 % (3322978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.59/2.39 % (3322978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.59/2.39 % (3322978)CaDiCaL version: 2.1.3
% 14.59/2.39 % (3322978)Termination reason: Instruction limit
% 14.59/2.39 % (3322978)Termination phase: Saturation
% 14.59/2.39 % (3322978)Time elapsed: 0.030 s
% 14.59/2.39 % (3322978)Peak memory usage: 12 MB
% 14.59/2.39 % (3322978)Instructions burned: 105 (million)
% 14.59/2.39 % TRYING [5]
% 14.59/2.39 % (3322989)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=866471866:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 14.59/2.39 % TRYING [1]
% 14.59/2.39 % TRYING [2]
% 14.59/2.39 % TRYING [3]
% 14.59/2.39 % TRYING [4]
% 14.59/2.39 % TRYING [5]
% 14.59/2.39 % TRYING [6]
% 14.59/2.39 % (3322980)Instruction limit reached!
% 14.59/2.39 % (3322980)------------------------------
% 14.59/2.39 % (3322980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.59/2.39 % (3322980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.59/2.39 % (3322980)CaDiCaL version: 2.1.3
% 14.59/2.39 % (3322980)Termination reason: Instruction limit
% 14.59/2.39 % (3322980)Termination phase: Saturation
% 14.59/2.39 % (3322980)Time elapsed: 0.060 s
% 14.59/2.39 % (3322980)Peak memory usage: 12 MB
% 14.59/2.39 % (3322980)Instructions burned: 131 (million)
% 14.59/2.39 % (3322979)Instruction limit reached!
% 14.59/2.39 % (3322979)------------------------------
% 14.59/2.39 % (3322979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.59/2.39 % (3322979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.59/2.39 % (3322979)CaDiCaL version: 2.1.3
% 14.59/2.39 % (3322979)Termination reason: Instruction limit
% 14.59/2.39 % (3322979)Termination phase: Saturation
% 14.59/2.39 % (3322979)Time elapsed: 0.065 s
% 14.59/2.39 % (3322979)Peak memory usage: 12 MB
% 14.59/2.39 % (3322979)Instructions burned: 117 (million)
% 14.59/2.39 % (3322991)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2543958496:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 14.59/2.39 % (3322992)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=4009758610:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.59/2.39 % (3322981)Instruction limit reached!
% 14.59/2.39 % (3322981)------------------------------
% 14.59/2.39 % (3322981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.59/2.39 % (3322981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.59/2.39 % (3322981)CaDiCaL version: 2.1.3
% 14.59/2.39 % (3322981)Termination reason: Instruction limit
% 14.59/2.39 % (3322981)Termination phase: Saturation
% 14.59/2.39 % (3322981)Time elapsed: 0.092 s
% 14.59/2.39 % (3322981)Peak memory usage: 13 MB
% 14.59/2.39 % (3322981)Instructions burned: 161 (million)
% 14.59/2.39 % TRYING [6]
% 14.59/2.39 % (3322995)ott-21_1_sil=16000:fs=off:random_seed=337272237:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.59/2.39 % TRYING [7]
% 14.59/2.39 % (3322991)Instruction limit reached!
% 14.59/2.39 % (3322991)------------------------------
% 14.59/2.39 % (3322991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.97/6.34 % (3322991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.97/6.34 % (3322991)CaDiCaL version: 2.1.3
% 42.97/6.34 % (3322991)Termination reason: Instruction limit
% 42.97/6.34 % (3322991)Termination phase: Saturation
% 42.97/6.34 % (3322991)Time elapsed: 0.075 s
% 42.97/6.34 % (3322991)Peak memory usage: 12 MB
% 42.97/6.34 % (3322991)Instructions burned: 133 (million)
% 42.97/6.34 % (3322997)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4195393275:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 42.97/6.34 % (3322995)Instruction limit reached!
% 42.97/6.34 % (3322995)------------------------------
% 42.97/6.34 % (3322995)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.97/6.34 % (3322995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.97/6.34 % (3322995)CaDiCaL version: 2.1.3
% 42.97/6.34 % (3322995)Termination reason: Instruction limit
% 42.97/6.34 % (3322995)Termination phase: Saturation
% 42.97/6.34 % (3322995)Time elapsed: 0.076 s
% 42.97/6.34 % (3322995)Peak memory usage: 11 MB
% 42.97/6.34 % (3322995)Instructions burned: 182 (million)
% 42.97/6.34 % (3322999)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3109099515:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 42.97/6.34 % TRYING [1]
% 42.97/6.34 % (3322989)Instruction limit reached!
% 42.97/6.34 % (3322989)------------------------------
% 42.97/6.34 % (3322989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.97/6.34 % (3322989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.97/6.34 % (3322989)CaDiCaL version: 2.1.3
% 42.97/6.34 % (3322989)Termination reason: Instruction limit
% 42.97/6.34 % (3322989)Termination phase: Finite model building SAT solving
% 42.97/6.34 % (3322989)Time elapsed: 0.178 s
% 42.97/6.34 % (3322989)Peak memory usage: 24 MB
% 42.97/6.34 % (3322989)Instructions burned: 714 (million)
% 42.97/6.34 % TRYING [2]
% 42.97/6.34 % TRYING [3]
% 42.97/6.34 % (3323001)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3524368650:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 42.97/6.34 % TRYING [4]
% 42.97/6.34 % TRYING [5]
% 42.97/6.34 % TRYING [6]
% 42.97/6.34 % TRYING [8]
% 42.97/6.34 % (3322997)Instruction limit reached!
% 42.97/6.34 % (3322997)------------------------------
% 42.97/6.34 % (3322997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.97/6.34 % (3322997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.97/6.34 % (3322997)CaDiCaL version: 2.1.3
% 42.97/6.34 % (3322997)Termination reason: Instruction limit
% 42.97/6.34 % (3322997)Termination phase: Saturation
% 42.97/6.34 % (3322997)Time elapsed: 0.268 s
% 42.97/6.34 % (3322997)Peak memory usage: 13 MB
% 42.97/6.34 % (3322997)Instructions burned: 478 (million)
% 42.97/6.34 % (3322992)Instruction limit reached!
% 42.97/6.34 % (3322992)------------------------------
% 42.97/6.34 % (3322992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.97/6.34 % (3322992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.97/6.34 % (3322992)CaDiCaL version: 2.1.3
% 42.97/6.34 % (3322992)Termination reason: Instruction limit
% 42.97/6.34 % (3322992)Termination phase: Saturation
% 42.97/6.34 % (3322992)Time elapsed: 0.378 s
% 42.97/6.34 % (3322992)Peak memory usage: 16 MB
% 42.97/6.34 % (3322992)Instructions burned: 686 (million)
% 42.97/6.34 % (3323003)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1983107118:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 42.97/6.34 % (3323005)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3246252000:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 42.97/6.34 % TRYING [14]
% 42.97/6.34 % (3322999)Instruction limit reached!
% 42.97/6.34 % (3322999)------------------------------
% 42.97/6.34 % (3322999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 42.97/6.34 % (3322999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.97/6.34 % (3322999)CaDiCaL version: 2.1.3
% 42.97/6.34 % (3322999)Termination reason: Instruction limit
% 42.97/6.34 % (3322999)Termination phase: Finite model building SAT solving
% 42.97/6.34 % (3322999)Time elapsed: 0.292 s
% 42.97/6.34 % (3322999)Peak memory usage: 18 MB
% 42.97/6.34 % (3322999)Instructions burned: 865 (million)
% 42.97/6.34 % (3323007)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3869631605:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 68.53/9.98 % (3323001)Instruction limit reached!
% 68.53/9.98 % (3323001)------------------------------
% 68.53/9.98 % (3323001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.53/9.98 % (3323001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.53/9.98 % (3323001)CaDiCaL version: 2.1.3
% 68.53/9.98 % (3323001)Termination reason: Instruction limit
% 68.53/9.98 % (3323001)Termination phase: Saturation
% 68.53/9.98 % (3323001)Time elapsed: 0.317 s
% 68.53/9.98 % (3323001)Peak memory usage: 23 MB
% 68.53/9.98 % (3323001)Instructions burned: 1179 (million)
% 68.53/9.98 % (3323009)fmb+10_1_sil=64000:random_seed=2230892467:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 68.53/9.98 % TRYING [1]
% 68.53/9.98 % TRYING [2]
% 68.53/9.98 % TRYING [3]
% 68.53/9.98 % TRYING [4]
% 68.53/9.98 % TRYING [5]
% 68.53/9.98 % TRYING [6]
% 68.53/9.98 % (3323003)Instruction limit reached!
% 68.53/9.98 % (3323003)------------------------------
% 68.53/9.98 % (3323003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.53/9.98 % (3323003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.53/9.98 % (3323003)CaDiCaL version: 2.1.3
% 68.53/9.98 % (3323003)Termination reason: Instruction limit
% 68.53/9.98 % (3323003)Termination phase: Finite model building constraint generation
% 68.53/9.98 % (3323003)Time elapsed: 0.299 s
% 68.53/9.98 % (3323003)Peak memory usage: 66 MB
% 68.53/9.98 % (3323003)Instructions burned: 892 (million)
% 68.53/9.98 % TRYING [7]
% 68.53/9.98 % (3323011)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=383046004:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 68.53/9.98 % TRYING [20]
% 68.53/9.98 % (3323005)Instruction limit reached!
% 68.53/9.98 % (3323005)------------------------------
% 68.53/9.98 % (3323005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.53/9.98 % (3323005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.53/9.98 % (3323005)CaDiCaL version: 2.1.3
% 68.53/9.98 % (3323005)Termination reason: Instruction limit
% 68.53/9.98 % (3323005)Termination phase: Saturation
% 68.53/9.98 % (3323005)Time elapsed: 0.372 s
% 68.53/9.98 % (3323005)Peak memory usage: 17 MB
% 68.53/9.98 % (3323005)Instructions burned: 692 (million)
% 68.53/9.98 % (3323013)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=807095456:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 68.53/9.98 % TRYING [8]
% 68.53/9.98 % TRYING [8]
% 68.53/9.98 % (3323007)Instruction limit reached!
% 68.53/9.98 % (3323007)------------------------------
% 68.53/9.98 % (3323007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.53/9.98 % (3323007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.53/9.98 % (3323007)CaDiCaL version: 2.1.3
% 68.53/9.98 % (3323007)Termination reason: Instruction limit
% 68.53/9.98 % (3323007)Termination phase: Saturation
% 68.53/9.98 % (3323007)Time elapsed: 0.466 s
% 68.53/9.98 % (3323007)Peak memory usage: 17 MB
% 68.53/9.98 % (3323007)Instructions burned: 879 (million)
% 68.53/9.98 % (3323015)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2736279152:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 68.53/9.98 % (3323013)Instruction limit reached!
% 68.53/9.98 % (3323013)------------------------------
% 68.53/9.98 % (3323013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.53/9.98 % (3323013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.53/9.98 % (3323013)CaDiCaL version: 2.1.3
% 68.53/9.98 % (3323013)Termination reason: Instruction limit
% 68.53/9.98 % (3323013)Termination phase: Finite model building SAT solving
% 68.53/9.98 % (3323013)Time elapsed: 0.374 s
% 68.53/9.98 % (3323013)Peak memory usage: 36 MB
% 68.53/9.98 % (3323013)Instructions burned: 920 (million)
% 68.53/9.98 % (3323017)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3494609653:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 68.53/9.98 % TRYING [9]
% 68.53/9.98 % TRYING [9]
% 68.53/9.98 % (3323017)Instruction limit reached!
% 68.53/9.98 % (3323017)------------------------------
% 68.53/9.98 % (3323017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 68.53/9.98 % (3323017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.53/9.98 % (3323017)CaDiCaL version: 2.1.3
% 68.53/9.98 % (3323017)Termination reason: Instruction limit
% 68.53/9.98 % (3323017)Termination phase: Saturation
% 68.53/9.98 % (3323017)Time elapsed: 0.820 s
% 68.53/9.98 % (3323017)Peak memory usage: 28 MB
% 68.53/9.98 % (3323017)Instructions burned: 1473 (million)
% 68.53/9.98 % (3323019)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1681301039:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 192.40/27.48 % TRYING [77]
% 192.40/27.48 % TRYING [10]
% 192.40/27.48 % TRYING [10]
% 192.40/27.48 % (3323015)Instruction limit reached!
% 192.40/27.48 % (3323015)------------------------------
% 192.40/27.48 % (3323015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 192.40/27.48 % (3323015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.40/27.48 % (3323015)CaDiCaL version: 2.1.3
% 192.40/27.48 % (3323015)Termination reason: Instruction limit
% 192.40/27.48 % (3323015)Termination phase: Saturation
% 192.40/27.48 % (3323015)Time elapsed: 2.529 s
% 192.40/27.48 % (3323015)Peak memory usage: 40 MB
% 192.40/27.48 % (3323015)Instructions burned: 5131 (million)
% 192.40/27.48 % (3323021)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1748066064:fmbsr=2.30978:i=2174_2964 on theBenchmark for (2964ds/2174Mi)
% 192.40/27.48 % TRYING [16]
% 192.40/27.48 % (3323021)Instruction limit reached!
% 192.40/27.48 % (3323021)------------------------------
% 192.40/27.48 % (3323021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 192.40/27.48 % (3323021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.40/27.48 % (3323021)CaDiCaL version: 2.1.3
% 192.40/27.48 % (3323021)Termination reason: Instruction limit
% 192.40/27.48 % (3323021)Termination phase: Finite model building constraint generation
% 192.40/27.48 % (3323021)Time elapsed: 0.807 s
% 192.40/27.48 % (3323021)Peak memory usage: 173 MB
% 192.40/27.48 % (3323021)Instructions burned: 2175 (million)
% 192.40/27.48 % (3323019)Instruction limit reached!
% 192.40/27.48 % (3323019)------------------------------
% 192.40/27.48 % (3323019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 192.40/27.48 % (3323019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.40/27.48 % (3323019)CaDiCaL version: 2.1.3
% 192.40/27.48 % (3323019)Termination reason: Instruction limit
% 192.40/27.48 % (3323019)Termination phase: Finite model building constraint generation
% 192.40/27.48 % (3323019)Time elapsed: 2.266 s
% 192.40/27.48 % (3323019)Peak memory usage: 456 MB
% 192.40/27.48 % (3323019)Instructions burned: 6326 (million)
% 192.40/27.48 % (3323023)ott-2_1_sil=16000:newcnf=on:random_seed=742539092:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2955 on theBenchmark for (2955ds/869Mi)
% 192.40/27.48 % (3323025)ott+10_1_sil=32000:tgt=ground:random_seed=3815002319:i=5114:av=off_2955 on theBenchmark for (2955ds/5114Mi)
% 192.40/27.48 % (3323023)Instruction limit reached!
% 192.40/27.48 % (3323023)------------------------------
% 192.40/27.48 % (3323023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 192.40/27.48 % (3323023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.40/27.48 % (3323023)CaDiCaL version: 2.1.3
% 192.40/27.48 % (3323023)Termination reason: Instruction limit
% 192.40/27.48 % (3323023)Termination phase: Saturation
% 192.40/27.48 % (3323023)Time elapsed: 0.438 s
% 192.40/27.48 % (3323023)Peak memory usage: 21 MB
% 192.40/27.48 % (3323023)Instructions burned: 870 (million)
% 192.40/27.48 % (3323027)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3411370626:i=54282_2951 on theBenchmark for (2951ds/54282Mi)
% 192.40/27.48 % TRYING [1]
% 192.40/27.48 % TRYING [2]
% 192.40/27.48 % TRYING [3]
% 192.40/27.48 % TRYING [4]
% 192.40/27.48 % TRYING [5]
% 192.40/27.48 % TRYING [6]
% 192.40/27.48 % TRYING [7]
% 192.40/27.48 % (3323011)Instruction limit reached!
% 192.40/27.48 % (3323011)------------------------------
% 192.40/27.48 % (3323011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 192.40/27.48 % (3323011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.40/27.48 % (3323011)CaDiCaL version: 2.1.3
% 192.40/27.48 % (3323011)Termination reason: Instruction limit
% 192.40/27.48 % (3323011)Termination phase: Finite model building constraint generation
% 192.40/27.48 % (3323011)Time elapsed: 4.287 s
% 192.40/27.48 % (3323011)Peak memory usage: 596 MB
% 192.40/27.48 % (3323011)Instructions burned: 9515 (million)
% 192.40/27.48 % (3323029)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=931672107:i=3512:aac=none_2948 on theBenchmark for (2948ds/3512Mi)
% 192.40/27.48 % TRYING [8]
% 192.40/27.48 % (3323009)Instruction limit reached!
% 192.40/27.48 % (3323009)------------------------------
% 192.40/27.48 % (3323009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 192.40/27.48 % (3323009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.40/27.48 % (3323009)CaDiCaL version: 2.1.3
% 192.40/27.48 % (3323009)Termination reason: Instruction limit
% 192.40/27.48 % (3323009)Termination phase: Finite model building SAT solving
% 192.40/27.48 % (3323009)Time elapsed: 5.506 s
% 192.40/27.48 % (3323009)Peak memory usage: 64 MB
% 192.40/27.48 % (3323009)Instructions burned: 22061 (million)
% 192.40/27.48 % (3323031)dis+21_1_sil=32000:sas=cadical:random_seed=2702602140:i=3773:amm=off_2938 on theBenchmark for (2938ds/3773Mi)
% 192.40/27.48 % (3323025)Instruction limit reached!
% 192.40/27.48 % (3323025)------------------------------
% 192.40/27.48 % (3323025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 192.40/27.48 % (3323025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.40/27.48 % (3323025)CaDiCaL version: 2.1.3
% 192.40/27.48 % (3323025)Termination reason: Instruction limit
% 192.40/27.48 % (3323025)Termination phase: Saturation
% 192.40/27.48 % (3323025)Time elapsed: 1.750 s
% 192.40/27.48 % (3323025)Peak memory usage: 13 MB
% 192.40/27.48 % (3323025)Instructions burned: 5115 (million)
% 192.40/27.48 % (3323033)ott+11_1_sil=16000:gs=on:random_seed=295291295:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2937 on theBenchmark for (2937ds/2251Mi)
% 192.40/27.48 % TRYING [9]
% 192.40/27.48 % (3323029)Instruction limit reached!
% 192.40/27.48 % (3323029)------------------------------
% 192.40/27.48 % (3323029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 192.40/27.48 % (3323029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.40/27.48 % (3323029)CaDiCaL version: 2.1.3
% 192.40/27.48 % (3323029)Termination reason: Instruction limit
% 192.40/27.48 % (3323029)Termination phase: Saturation
% 192.40/27.48 % (3323029)Time elapsed: 1.800 s
% 192.40/27.48 % (3323029)Peak memory usage: 33 MB
% 192.40/27.48 % (3323029)Instructions burned: 3513 (million)
% 192.40/27.48 % (3323035)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2040741857:fmbsr=1.6:i=67534_2929 on theBenchmark for (2929ds/67534Mi)
% 192.40/27.48 % TRYING [7]
% 192.40/27.48 % (3323031)Instruction limit reached!
% 192.40/27.48 % (3323031)------------------------------
% 192.40/27.48 % (3323031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 192.40/27.48 % (3323031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.40/27.48 % (3323031)CaDiCaL version: 2.1.3
% 192.40/27.48 % (3323031)Termination reason: Instruction limit
% 192.40/27.48 % (3323031)Termination phase: Saturation
% 192.40/27.48 % (3323031)Time elapsed: 1.132 s
% 192.40/27.48 % (3323031)Peak memory usage: 33 MB
% 192.40/27.48 % (3323031)Instructions burned: 3775 (million)
% 192.40/27.48 % (3323037)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1992595211:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2927 on theBenchmark for (2927ds/4591Mi)
% 192.40/27.48 % (3323033)Instruction limit reached!
% 192.40/27.48 % (3323033)------------------------------
% 192.40/27.48 % (3323033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 192.40/27.48 % (3323033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.40/27.48 % (3323033)CaDiCaL version: 2.1.3
% 192.40/27.48 % (3323033)Termination reason: Instruction limit
% 192.40/27.48 % (3323033)Termination phase: Saturation
% 192.40/27.48 % (3323033)Time elapsed: 1.114 s
% 192.40/27.48 % (3323033)Peak memory usage: 34 MB
% 192.40/27.48 % (3323033)Instructions burned: 2252 (million)
% 192.40/27.48 % (3323039)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3505841151:i=29340_2926 on theBenchmark for (2926ds/29340Mi)
% 192.40/27.48 % TRYING [10]
% 192.40/27.48 % TRYING [8]
% 192.40/27.48 % (3323037)Instruction limit reached!
% 192.40/27.48 % (3323037)------------------------------
% 192.40/27.48 % (3323037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 192.40/27.48 % (3323037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.40/27.48 % (3323037)CaDiCaL version: 2.1.3
% 192.40/27.48 % (3323037)Termination reason: Instruction limit
% 192.40/27.48 % (3323037)Termination phase: Saturation
% 192.40/27.48 % (3323037)Time elapsed: 1.305 s
% 192.40/27.48 % (3323037)Peak memory usage: 58 MB
% 192.40/27.48 % (3323037)Instructions burned: 4594 (million)
% 192.40/27.48 % (3323041)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=403218426:i=5211_2914 on theBenchmark for (2914ds/5211Mi)
% 192.40/27.48 % (3323041)Instruction limit reached!
% 192.40/27.48 % (3323041)------------------------------
% 192.40/27.48 % (3323041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 192.40/27.48 % (3323041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.40/27.48 % (3323041)CaDiCaL version: 2.1.3
% 192.40/27.48 % (3323041)Termination reason: Instruction limit
% 192.40/27.48 % (3323041)Termination phase: Saturation
% 192.40/27.48 % (3323041)Time elapsed: 1.159 s
% 192.40/27.48 % (3323041)Peak memory usage: 53 MB
% 192.40/27.48 % (3323041)Instructions burned: 5216 (million)
% 192.40/27.48 % (3323043)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=499040366:i=5497:nm=2_2902 on theBenchmark for (2902ds/5497Mi)
% 192.40/27.48 % TRYING [17]
% 192.40/27.48 % (3323043)Instruction limit reached!
% 192.40/27.48 % (3323043)------------------------------
% 192.40/27.48 % (3323043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 192.40/27.48 % (3323043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.40/27.48 % (3323043)CaDiCaL version: 2.1.3
% 192.40/27.48 % (3323043)Termination reason: Instruction limit
% 192.40/27.48 % (3323043)Termination phase: Finite model building constraint generation
% 192.40/27.48 % (3323043)Time elapsed: 1.315 s
% 192.40/27.48 % (3323043)Peak memory usage: 307 MB
% 192.40/27.48 % (3323043)Instructions burned: 5499 (million)
% 192.40/27.48 % (3323045)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1566581323:fmbsr=2:i=46332_2889 on theBenchmark for (2889ds/46332Mi)
% 192.40/27.48 % TRYING [15]
% 192.40/27.48 % TRYING [9]
% 192.40/27.48 % (3323039)Instruction limit reached!
% 192.40/27.48 % (3323039)------------------------------
% 192.40/27.48 % (3323039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 192.40/27.48 % (3323039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.40/27.48 % (3323039)CaDiCaL version: 2.1.3
% 192.40/27.48 % (3323039)Termination reason: Instruction limit
% 192.40/27.48 % (3323039)Termination phase: Saturation
% 192.40/27.48 % (3323039)Time elapsed: 12.870 s
% 192.40/27.48 % (3323039)Peak memory usage: 116 MB
% 192.40/27.48 % (3323039)Instructions burned: 29340 (million)
% 192.40/27.48 % (3323047)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3300925184:i=14071_2797 on theBenchmark for (2797ds/14071Mi)
% 192.40/27.48 % TRYING [12]
% 192.40/27.48 % (3323045)Instruction limit reached!
% 192.40/27.48 % (3323045)------------------------------
% 192.40/27.48 % (3323045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 192.40/27.48 % (3323045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.40/27.48 % (3323045)CaDiCaL version: 2.1.3
% 192.40/27.48 % (3323045)Termination reason: Instruction limit
% 192.40/27.48 % (3323045)Termination phase: Finite model building SAT solving
% 192.40/27.48 % (3323045)Time elapsed: 15.596 s
% 192.40/27.48 % (3323045)Peak memory usage: 423 MB
% 192.40/27.48 % (3323045)Instructions burned: 46337 (million)
% 192.40/27.48 % (3323049)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4189735786:i=22565:add=on:rawr=on_2732 on theBenchmark for (2732ds/22565Mi)
% 192.40/27.48 % (3323047)Instruction limit reached!
% 192.40/27.48 % (3323047)------------------------------
% 192.40/27.48 % (3323047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 192.40/27.48 % (3323047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.40/27.48 % (3323047)CaDiCaL version: 2.1.3
% 192.40/27.48 % (3323047)Termination reason: Instruction limit
% 192.40/27.48 % (3323047)Termination phase: Finite model building SAT solving
% 192.40/27.48 % (3323047)Time elapsed: 6.519 s
% 192.40/27.48 % (3323047)Peak memory usage: 182 MB
% 192.40/27.48 % (3323047)Instructions burned: 14073 (million)
% 192.40/27.48 % (3323051)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3613173005:i=8173:av=off_2731 on theBenchmark for (2731ds/8173Mi)
% 192.40/27.48 % (3323051) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3322970-3323051"...
% 192.40/27.48 % (3323051)...printing done.
% 192.40/27.48 % (3323051)Refutation found. Thanks to Tanya!
% 192.40/27.48 % SZS status Unsatisfiable for theBenchmark
% 192.40/27.48 % SZS output start Proof for theBenchmark
% See solution above
% 192.40/27.49 % (3323051)------------------------------
% 192.40/27.49 % (3323051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 192.40/27.49 % (3323051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 192.40/27.49 % (3323051)CaDiCaL version: 2.1.3
% 192.40/27.49 % (3323051)Termination reason: Refutation
% 192.40/27.49 % (3323051)Time elapsed: 0.308 s
% 192.40/27.49 % (3323051)Peak memory usage: 13 MB
% 192.40/27.49 % (3323051)Instructions burned: 706 (million)
% 192.40/27.49 % (3322970)Success in time 27.247 s
% 192.40/27.49 % Vampire exiting
%------------------------------------------------------------------------------