%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWV567-1.014 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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 : Sun Sep 27 09:04:20 AM UTC 2026
% Result : Unsatisfiable 138.21s 20.33s
% Output : CNFRefutation 138.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 62
% Number of leaves : 70
% Syntax : Number of clauses : 294 ( 246 unt; 47 nHn; 275 RR)
% Number of literals : 377 ( 376 equ; 109 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 64 ( 64 usr; 61 con; 0-3 aty)
% Number of variables : 53 ( 4 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(as12,axiom,
s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))) != X0 ).
cnf(as11,axiom,
s(s(s(s(s(s(s(s(s(s(s(X0))))))))))) != X0 ).
cnf(as10,axiom,
s(s(s(s(s(s(s(s(s(s(X0)))))))))) != X0 ).
cnf(as9,axiom,
s(s(s(s(s(s(s(s(s(X0))))))))) != X0 ).
cnf(as8,axiom,
s(s(s(s(s(s(s(s(X0)))))))) != X0 ).
cnf(as7,axiom,
s(s(s(s(s(s(s(X0))))))) != X0 ).
cnf(as6,axiom,
s(s(s(s(s(s(X0)))))) != X0 ).
cnf(as5,axiom,
s(s(s(s(s(X0))))) != X0 ).
cnf(as4,axiom,
s(s(s(s(X0)))) != X0 ).
cnf(as3,axiom,
s(s(s(X0))) != X0 ).
cnf(as2,axiom,
s(s(X0)) != X0 ).
cnf(as1,axiom,
s(X0) != X0 ).
cnf(hyp0,hypothesis,
'earray$u12' = store('earray$u9','elem$u10','elem$u11') ).
cnf(hyp1,hypothesis,
'earray$u15' = store('earray$u12','elem$u13','elem$u14') ).
cnf(hyp2,hypothesis,
'earray$u18' = store('earray$u15','elem$u16','elem$u17') ).
cnf(hyp3,hypothesis,
'earray$u21' = store('earray$u18','elem$u19','elem$u20') ).
cnf(hyp4,hypothesis,
'earray$u24' = store('earray$u21','elem$u22','elem$u23') ).
cnf(hyp5,hypothesis,
'earray$u27' = store('earray$u24','elem$u25','elem$u26') ).
cnf(hyp7,hypothesis,
'earray$u30' = store('earray$u27','elem$u28','elem$u29') ).
cnf(hyp8,hypothesis,
'earray$u33' = store('earray$u30','elem$u31','elem$u32') ).
cnf(hyp9,hypothesis,
'earray$u36' = store('earray$u33','elem$u34','elem$u35') ).
cnf(hyp10,hypothesis,
'earray$u39' = store('earray$u36','elem$u37','elem$u38') ).
cnf(hyp11,hypothesis,
'earray$u42' = store('earray$u39','elem$u40','elem$u41') ).
cnf(hyp20,hypothesis,
'earray$u6' = store('earray$u3','elem$u4','elem$u5') ).
cnf(hyp24,hypothesis,
'earray$u67' = store('earray$u65','elem$u4','elem$u66') ).
cnf(hyp25,hypothesis,
'earray$u69' = store('earray$u67','elem$u0','elem$u68') ).
cnf(hyp26,hypothesis,
'earray$u71' = store('earray$u69',i,'elem$u70') ).
cnf(hyp27,hypothesis,
'earray$u9' = store('earray$u6','elem$u7','elem$u8') ).
cnf(hyp28,hypothesis,
'elem$u0' = s(i) ).
cnf(hyp30,hypothesis,
'elem$u10' = s('elem$u7') ).
cnf(hyp31,hypothesis,
'elem$u11' = s('elem$u8') ).
cnf(hyp32,hypothesis,
'elem$u13' = s('elem$u10') ).
cnf(hyp33,hypothesis,
'elem$u14' = s('elem$u11') ).
cnf(hyp34,hypothesis,
'elem$u16' = s('elem$u13') ).
cnf(hyp35,hypothesis,
'elem$u17' = s('elem$u14') ).
cnf(hyp36,hypothesis,
'elem$u19' = s('elem$u16') ).
cnf(hyp38,hypothesis,
'elem$u20' = s('elem$u17') ).
cnf(hyp39,hypothesis,
'elem$u22' = s('elem$u19') ).
cnf(hyp40,hypothesis,
'elem$u23' = s('elem$u20') ).
cnf(hyp41,hypothesis,
'elem$u25' = s('elem$u22') ).
cnf(hyp42,hypothesis,
'elem$u26' = s('elem$u23') ).
cnf(hyp43,hypothesis,
'elem$u28' = s('elem$u25') ).
cnf(hyp44,hypothesis,
'elem$u29' = s('elem$u26') ).
cnf(hyp45,hypothesis,
'elem$u31' = s('elem$u28') ).
cnf(hyp46,hypothesis,
'elem$u32' = s('elem$u29') ).
cnf(hyp47,hypothesis,
'elem$u34' = s('elem$u31') ).
cnf(hyp48,hypothesis,
'elem$u35' = s('elem$u32') ).
cnf(hyp49,hypothesis,
'elem$u37' = s('elem$u34') ).
cnf(hyp50,hypothesis,
'elem$u38' = s('elem$u35') ).
cnf(hyp51,hypothesis,
'elem$u4' = s('elem$u0') ).
cnf(hyp52,hypothesis,
'elem$u40' = s('elem$u37') ).
cnf(hyp53,hypothesis,
'elem$u41' = s('elem$u38') ).
cnf(hyp55,hypothesis,
s('elem$u44') = 'elem$u43' ).
cnf(hyp56,hypothesis,
s('elem$u46') = 'elem$u44' ).
cnf(hyp57,hypothesis,
s('elem$u48') = 'elem$u46' ).
cnf(hyp59,hypothesis,
s('elem$u50') = 'elem$u48' ).
cnf(hyp60,hypothesis,
s('elem$u52') = 'elem$u50' ).
cnf(hyp61,hypothesis,
s('elem$u54') = 'elem$u52' ).
cnf(hyp62,hypothesis,
s('elem$u56') = 'elem$u54' ).
cnf(hyp63,hypothesis,
s('elem$u58') = 'elem$u56' ).
cnf(hyp64,hypothesis,
s('elem$u60') = 'elem$u58' ).
cnf(hyp65,hypothesis,
s('elem$u62') = 'elem$u60' ).
cnf(hyp66,hypothesis,
s('elem$u64') = 'elem$u62' ).
cnf(hyp67,hypothesis,
s('elem$u66') = 'elem$u64' ).
cnf(hyp69,hypothesis,
'elem$u7' = s('elem$u4') ).
cnf(hyp71,hypothesis,
'elem$u8' = s('elem$u5') ).
cnf(hyp72,hypothesis,
'earray$u42' = 'earray$u71' ).
cnf(goal,negated_conjecture,
'elem$u41' != 'elem$u43' ).
cnf(c0,plain,
select(store(X0,X1,X2),X1) = X2,
inference(clausification,[status(esa)],[a1]) ).
cnf(c1,plain,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
inference(clausification,[status(esa)],[a2]) ).
cnf(c620,plain,
s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))) != X0,
inference(clausification,[status(esa)],[as12]) ).
cnf(c621,plain,
s(s(s(s(s(s(s(s(s(s(s(X0))))))))))) != X0,
inference(clausification,[status(esa)],[as11]) ).
cnf(c622,plain,
s(s(s(s(s(s(s(s(s(s(X0)))))))))) != X0,
inference(clausification,[status(esa)],[as10]) ).
cnf(c623,plain,
s(s(s(s(s(s(s(s(s(X0))))))))) != X0,
inference(clausification,[status(esa)],[as9]) ).
cnf(c624,plain,
s(s(s(s(s(s(s(s(X0)))))))) != X0,
inference(clausification,[status(esa)],[as8]) ).
cnf(c625,plain,
s(s(s(s(s(s(s(X0))))))) != X0,
inference(clausification,[status(esa)],[as7]) ).
cnf(c626,plain,
s(s(s(s(s(s(X0)))))) != X0,
inference(clausification,[status(esa)],[as6]) ).
cnf(c627,plain,
s(s(s(s(s(X0))))) != X0,
inference(clausification,[status(esa)],[as5]) ).
cnf(c628,plain,
s(s(s(s(X0)))) != X0,
inference(clausification,[status(esa)],[as4]) ).
cnf(c629,plain,
s(s(s(X0))) != X0,
inference(clausification,[status(esa)],[as3]) ).
cnf(c630,plain,
s(s(X0)) != X0,
inference(clausification,[status(esa)],[as2]) ).
cnf(c631,plain,
s(X0) != X0,
inference(clausification,[status(esa)],[as1]) ).
cnf(c632,plain,
'earray$u12' = store('earray$u9','elem$u10','elem$u11'),
inference(clausification,[status(esa)],[hyp0]) ).
cnf(c633,plain,
'earray$u15' = store('earray$u12','elem$u13','elem$u14'),
inference(clausification,[status(esa)],[hyp1]) ).
cnf(c634,plain,
'earray$u18' = store('earray$u15','elem$u16','elem$u17'),
inference(clausification,[status(esa)],[hyp2]) ).
cnf(c635,plain,
'earray$u21' = store('earray$u18','elem$u19','elem$u20'),
inference(clausification,[status(esa)],[hyp3]) ).
cnf(c636,plain,
'earray$u24' = store('earray$u21','elem$u22','elem$u23'),
inference(clausification,[status(esa)],[hyp4]) ).
cnf(c637,plain,
'earray$u27' = store('earray$u24','elem$u25','elem$u26'),
inference(clausification,[status(esa)],[hyp5]) ).
cnf(c639,plain,
'earray$u30' = store('earray$u27','elem$u28','elem$u29'),
inference(clausification,[status(esa)],[hyp7]) ).
cnf(c640,plain,
'earray$u33' = store('earray$u30','elem$u31','elem$u32'),
inference(clausification,[status(esa)],[hyp8]) ).
cnf(c641,plain,
'earray$u36' = store('earray$u33','elem$u34','elem$u35'),
inference(clausification,[status(esa)],[hyp9]) ).
cnf(c642,plain,
'earray$u39' = store('earray$u36','elem$u37','elem$u38'),
inference(clausification,[status(esa)],[hyp10]) ).
cnf(c643,plain,
'earray$u42' = store('earray$u39','elem$u40','elem$u41'),
inference(clausification,[status(esa)],[hyp11]) ).
cnf(c652,plain,
'earray$u6' = store('earray$u3','elem$u4','elem$u5'),
inference(clausification,[status(esa)],[hyp20]) ).
cnf(c656,plain,
'earray$u67' = store('earray$u65','elem$u4','elem$u66'),
inference(clausification,[status(esa)],[hyp24]) ).
cnf(c657,plain,
'earray$u69' = store('earray$u67','elem$u0','elem$u68'),
inference(clausification,[status(esa)],[hyp25]) ).
cnf(c658,plain,
'earray$u71' = store('earray$u69',i,'elem$u70'),
inference(clausification,[status(esa)],[hyp26]) ).
cnf(c659,plain,
'earray$u9' = store('earray$u6','elem$u7','elem$u8'),
inference(clausification,[status(esa)],[hyp27]) ).
cnf(c660,plain,
'elem$u0' = s(i),
inference(clausification,[status(esa)],[hyp28]) ).
cnf(c662,plain,
'elem$u10' = s('elem$u7'),
inference(clausification,[status(esa)],[hyp30]) ).
cnf(c663,plain,
'elem$u11' = s('elem$u8'),
inference(clausification,[status(esa)],[hyp31]) ).
cnf(c664,plain,
'elem$u13' = s('elem$u10'),
inference(clausification,[status(esa)],[hyp32]) ).
cnf(c665,plain,
'elem$u14' = s('elem$u11'),
inference(clausification,[status(esa)],[hyp33]) ).
cnf(c666,plain,
'elem$u16' = s('elem$u13'),
inference(clausification,[status(esa)],[hyp34]) ).
cnf(c667,plain,
'elem$u17' = s('elem$u14'),
inference(clausification,[status(esa)],[hyp35]) ).
cnf(c668,plain,
'elem$u19' = s('elem$u16'),
inference(clausification,[status(esa)],[hyp36]) ).
cnf(c670,plain,
'elem$u20' = s('elem$u17'),
inference(clausification,[status(esa)],[hyp38]) ).
cnf(c671,plain,
'elem$u22' = s('elem$u19'),
inference(clausification,[status(esa)],[hyp39]) ).
cnf(c672,plain,
'elem$u23' = s('elem$u20'),
inference(clausification,[status(esa)],[hyp40]) ).
cnf(c673,plain,
'elem$u25' = s('elem$u22'),
inference(clausification,[status(esa)],[hyp41]) ).
cnf(c674,plain,
'elem$u26' = s('elem$u23'),
inference(clausification,[status(esa)],[hyp42]) ).
cnf(c675,plain,
'elem$u28' = s('elem$u25'),
inference(clausification,[status(esa)],[hyp43]) ).
cnf(c676,plain,
'elem$u29' = s('elem$u26'),
inference(clausification,[status(esa)],[hyp44]) ).
cnf(c677,plain,
'elem$u31' = s('elem$u28'),
inference(clausification,[status(esa)],[hyp45]) ).
cnf(c678,plain,
'elem$u32' = s('elem$u29'),
inference(clausification,[status(esa)],[hyp46]) ).
cnf(c679,plain,
'elem$u34' = s('elem$u31'),
inference(clausification,[status(esa)],[hyp47]) ).
cnf(c680,plain,
'elem$u35' = s('elem$u32'),
inference(clausification,[status(esa)],[hyp48]) ).
cnf(c681,plain,
'elem$u37' = s('elem$u34'),
inference(clausification,[status(esa)],[hyp49]) ).
cnf(c682,plain,
'elem$u38' = s('elem$u35'),
inference(clausification,[status(esa)],[hyp50]) ).
cnf(c683,plain,
'elem$u4' = s('elem$u0'),
inference(clausification,[status(esa)],[hyp51]) ).
cnf(c684,plain,
'elem$u40' = s('elem$u37'),
inference(clausification,[status(esa)],[hyp52]) ).
cnf(c685,plain,
'elem$u41' = s('elem$u38'),
inference(clausification,[status(esa)],[hyp53]) ).
cnf(c687,plain,
s('elem$u44') = 'elem$u43',
inference(clausification,[status(esa)],[hyp55]) ).
cnf(c688,plain,
s('elem$u46') = 'elem$u44',
inference(clausification,[status(esa)],[hyp56]) ).
cnf(c689,plain,
s('elem$u48') = 'elem$u46',
inference(clausification,[status(esa)],[hyp57]) ).
cnf(c691,plain,
s('elem$u50') = 'elem$u48',
inference(clausification,[status(esa)],[hyp59]) ).
cnf(c692,plain,
s('elem$u52') = 'elem$u50',
inference(clausification,[status(esa)],[hyp60]) ).
cnf(c693,plain,
s('elem$u54') = 'elem$u52',
inference(clausification,[status(esa)],[hyp61]) ).
cnf(c694,plain,
s('elem$u56') = 'elem$u54',
inference(clausification,[status(esa)],[hyp62]) ).
cnf(c695,plain,
s('elem$u58') = 'elem$u56',
inference(clausification,[status(esa)],[hyp63]) ).
cnf(c696,plain,
s('elem$u60') = 'elem$u58',
inference(clausification,[status(esa)],[hyp64]) ).
cnf(c697,plain,
s('elem$u62') = 'elem$u60',
inference(clausification,[status(esa)],[hyp65]) ).
cnf(c698,plain,
s('elem$u64') = 'elem$u62',
inference(clausification,[status(esa)],[hyp66]) ).
cnf(c699,plain,
s('elem$u66') = 'elem$u64',
inference(clausification,[status(esa)],[hyp67]) ).
cnf(c701,plain,
'elem$u7' = s('elem$u4'),
inference(clausification,[status(esa)],[hyp69]) ).
cnf(c703,plain,
'elem$u8' = s('elem$u5'),
inference(clausification,[status(esa)],[hyp71]) ).
cnf(c704,plain,
'earray$u42' = 'earray$u71',
inference(clausification,[status(esa)],[hyp72]) ).
cnf(c705,plain,
'elem$u41' != 'elem$u43',
inference(clausification,[status(esa)],[goal]) ).
cnf(d0,plain,
'elem$u4' != 'elem$u0',
inference(superposition,[status(thm)],[c683,c631]) ).
cnf(d1,plain,
s('elem$u0') != i,
inference(superposition,[status(thm)],[c660,c630]) ).
cnf(d2,plain,
'elem$u4' != i,
inference(demodulation,[status(thm)],[d1,c683]) ).
cnf(d3,plain,
( 'elem$u10' = X0
| select('earray$u12',X0) = select('earray$u9',X0) ),
inference(superposition,[status(thm)],[c632,c1]) ).
cnf(d4,plain,
select('earray$u6','elem$u4') = 'elem$u5',
inference(superposition,[status(thm)],[c652,c0]) ).
cnf(d5,plain,
( 'elem$u7' = X0
| select('earray$u9',X0) = select('earray$u6',X0) ),
inference(superposition,[status(thm)],[c659,c1]) ).
cnf(d6,plain,
( 'elem$u7' = 'elem$u4'
| select('earray$u9','elem$u4') = 'elem$u5' ),
inference(superposition,[status(thm)],[d5,d4]) ).
cnf(d7,plain,
'elem$u7' != 'elem$u4',
inference(superposition,[status(thm)],[c701,c631]) ).
cnf(d8,plain,
select('earray$u9','elem$u4') = 'elem$u5',
inference(resolution,[status(thm)],[d7,d6]) ).
cnf(d9,plain,
( 'elem$u10' = 'elem$u4'
| select('earray$u12','elem$u4') = 'elem$u5' ),
inference(superposition,[status(thm)],[d8,d3]) ).
cnf(d10,plain,
s('elem$u7') != 'elem$u4',
inference(superposition,[status(thm)],[c701,c630]) ).
cnf(d11,plain,
'elem$u10' != 'elem$u4',
inference(demodulation,[status(thm)],[d10,c662]) ).
cnf(d12,plain,
select('earray$u12','elem$u4') = 'elem$u5',
inference(resolution,[status(thm)],[d11,d9]) ).
cnf(d13,plain,
( 'elem$u13' = X0
| select('earray$u15',X0) = select('earray$u12',X0) ),
inference(superposition,[status(thm)],[c633,c1]) ).
cnf(d14,plain,
( 'elem$u16' = X0
| select('earray$u18',X0) = select('earray$u15',X0) ),
inference(superposition,[status(thm)],[c634,c1]) ).
cnf(d15,plain,
( 'elem$u19' = X0
| select('earray$u21',X0) = select('earray$u18',X0) ),
inference(superposition,[status(thm)],[c635,c1]) ).
cnf(d16,plain,
( 'elem$u22' = X0
| select('earray$u24',X0) = select('earray$u21',X0) ),
inference(superposition,[status(thm)],[c636,c1]) ).
cnf(d17,plain,
( 'elem$u25' = X0
| select('earray$u27',X0) = select('earray$u24',X0) ),
inference(superposition,[status(thm)],[c637,c1]) ).
cnf(d18,plain,
( 'elem$u28' = X0
| select('earray$u30',X0) = select('earray$u27',X0) ),
inference(superposition,[status(thm)],[c639,c1]) ).
cnf(d19,plain,
( 'elem$u31' = X0
| select('earray$u33',X0) = select('earray$u30',X0) ),
inference(superposition,[status(thm)],[c640,c1]) ).
cnf(d20,plain,
( 'elem$u34' = X0
| select('earray$u36',X0) = select('earray$u33',X0) ),
inference(superposition,[status(thm)],[c641,c1]) ).
cnf(d21,plain,
( 'elem$u37' = X0
| select('earray$u39',X0) = select('earray$u36',X0) ),
inference(superposition,[status(thm)],[c642,c1]) ).
cnf(d22,plain,
( 'elem$u40' = X0
| select('earray$u42',X0) = select('earray$u39',X0) ),
inference(superposition,[status(thm)],[c643,c1]) ).
cnf(d23,plain,
select('earray$u67','elem$u4') = 'elem$u66',
inference(superposition,[status(thm)],[c656,c0]) ).
cnf(d24,plain,
( 'elem$u0' = X0
| select('earray$u69',X0) = select('earray$u67',X0) ),
inference(superposition,[status(thm)],[c657,c1]) ).
cnf(d25,plain,
'earray$u42' = store('earray$u69',i,'elem$u70'),
inference(demodulation,[status(thm)],[c658,c704]) ).
cnf(d26,plain,
( i = X0
| select('earray$u42',X0) = select('earray$u69',X0) ),
inference(superposition,[status(thm)],[d25,c1]) ).
cnf(d27,plain,
( i = X0
| 'elem$u0' = X0
| select('earray$u42',X0) = select('earray$u67',X0) ),
inference(superposition,[status(thm)],[d26,d24]) ).
cnf(d28,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| select('earray$u42','elem$u4') = 'elem$u66' ),
inference(superposition,[status(thm)],[d27,d23]) ).
cnf(d29,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u40' = 'elem$u4'
| 'elem$u66' = select('earray$u39','elem$u4') ),
inference(superposition,[status(thm)],[d28,d22]) ).
cnf(d30,plain,
s(s(s(s(s(s(s(s(s(s(s('elem$u7'))))))))))) != 'elem$u4',
inference(superposition,[status(thm)],[c701,c620]) ).
cnf(d31,plain,
s(s(s(s(s(s(s(s(s(s('elem$u10')))))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d30,c662]) ).
cnf(d32,plain,
s(s(s(s(s(s(s(s(s('elem$u13'))))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d31,c664]) ).
cnf(d33,plain,
s(s(s(s(s(s(s(s('elem$u16')))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d32,c666]) ).
cnf(d34,plain,
s(s(s(s(s(s(s('elem$u19'))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d33,c668]) ).
cnf(d35,plain,
s(s(s(s(s(s('elem$u22')))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d34,c671]) ).
cnf(d36,plain,
s(s(s(s(s('elem$u25'))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d35,c673]) ).
cnf(d37,plain,
s(s(s(s('elem$u28')))) != 'elem$u4',
inference(demodulation,[status(thm)],[d36,c675]) ).
cnf(d38,plain,
s(s(s('elem$u31'))) != 'elem$u4',
inference(demodulation,[status(thm)],[d37,c677]) ).
cnf(d39,plain,
s(s('elem$u34')) != 'elem$u4',
inference(demodulation,[status(thm)],[d38,c679]) ).
cnf(d40,plain,
s('elem$u37') != 'elem$u4',
inference(demodulation,[status(thm)],[d39,c681]) ).
cnf(d41,plain,
'elem$u40' != 'elem$u4',
inference(demodulation,[status(thm)],[d40,c684]) ).
cnf(d42,plain,
( i = 'elem$u4'
| 'elem$u66' = select('earray$u39','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d41,d29]) ).
cnf(d43,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u37' = 'elem$u4'
| 'elem$u66' = select('earray$u36','elem$u4') ),
inference(superposition,[status(thm)],[d42,d21]) ).
cnf(d44,plain,
s(s(s(s(s(s(s(s(s(s('elem$u7')))))))))) != 'elem$u4',
inference(superposition,[status(thm)],[c701,c621]) ).
cnf(d45,plain,
s(s(s(s(s(s(s(s(s('elem$u10'))))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d44,c662]) ).
cnf(d46,plain,
s(s(s(s(s(s(s(s('elem$u13')))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d45,c664]) ).
cnf(d47,plain,
s(s(s(s(s(s(s('elem$u16'))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d46,c666]) ).
cnf(d48,plain,
s(s(s(s(s(s('elem$u19')))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d47,c668]) ).
cnf(d49,plain,
s(s(s(s(s('elem$u22'))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d48,c671]) ).
cnf(d50,plain,
s(s(s(s('elem$u25')))) != 'elem$u4',
inference(demodulation,[status(thm)],[d49,c673]) ).
cnf(d51,plain,
s(s(s('elem$u28'))) != 'elem$u4',
inference(demodulation,[status(thm)],[d50,c675]) ).
cnf(d52,plain,
s(s('elem$u31')) != 'elem$u4',
inference(demodulation,[status(thm)],[d51,c677]) ).
cnf(d53,plain,
s('elem$u34') != 'elem$u4',
inference(demodulation,[status(thm)],[d52,c679]) ).
cnf(d54,plain,
'elem$u37' != 'elem$u4',
inference(demodulation,[status(thm)],[d53,c681]) ).
cnf(d55,plain,
( i = 'elem$u4'
| 'elem$u66' = select('earray$u36','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d54,d43]) ).
cnf(d56,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u34' = 'elem$u4'
| 'elem$u66' = select('earray$u33','elem$u4') ),
inference(superposition,[status(thm)],[d55,d20]) ).
cnf(d57,plain,
s(s(s(s(s(s(s(s(s('elem$u7'))))))))) != 'elem$u4',
inference(superposition,[status(thm)],[c701,c622]) ).
cnf(d58,plain,
s(s(s(s(s(s(s(s('elem$u10')))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d57,c662]) ).
cnf(d59,plain,
s(s(s(s(s(s(s('elem$u13'))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d58,c664]) ).
cnf(d60,plain,
s(s(s(s(s(s('elem$u16')))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d59,c666]) ).
cnf(d61,plain,
s(s(s(s(s('elem$u19'))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d60,c668]) ).
cnf(d62,plain,
s(s(s(s('elem$u22')))) != 'elem$u4',
inference(demodulation,[status(thm)],[d61,c671]) ).
cnf(d63,plain,
s(s(s('elem$u25'))) != 'elem$u4',
inference(demodulation,[status(thm)],[d62,c673]) ).
cnf(d64,plain,
s(s('elem$u28')) != 'elem$u4',
inference(demodulation,[status(thm)],[d63,c675]) ).
cnf(d65,plain,
s('elem$u31') != 'elem$u4',
inference(demodulation,[status(thm)],[d64,c677]) ).
cnf(d66,plain,
'elem$u34' != 'elem$u4',
inference(demodulation,[status(thm)],[d65,c679]) ).
cnf(d67,plain,
( i = 'elem$u4'
| 'elem$u66' = select('earray$u33','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d66,d56]) ).
cnf(d68,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u31' = 'elem$u4'
| 'elem$u66' = select('earray$u30','elem$u4') ),
inference(superposition,[status(thm)],[d67,d19]) ).
cnf(d69,plain,
s(s(s(s(s(s(s(s('elem$u7')))))))) != 'elem$u4',
inference(superposition,[status(thm)],[c701,c623]) ).
cnf(d70,plain,
s(s(s(s(s(s(s('elem$u10'))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d69,c662]) ).
cnf(d71,plain,
s(s(s(s(s(s('elem$u13')))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d70,c664]) ).
cnf(d72,plain,
s(s(s(s(s('elem$u16'))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d71,c666]) ).
cnf(d73,plain,
s(s(s(s('elem$u19')))) != 'elem$u4',
inference(demodulation,[status(thm)],[d72,c668]) ).
cnf(d74,plain,
s(s(s('elem$u22'))) != 'elem$u4',
inference(demodulation,[status(thm)],[d73,c671]) ).
cnf(d75,plain,
s(s('elem$u25')) != 'elem$u4',
inference(demodulation,[status(thm)],[d74,c673]) ).
cnf(d76,plain,
s('elem$u28') != 'elem$u4',
inference(demodulation,[status(thm)],[d75,c675]) ).
cnf(d77,plain,
'elem$u31' != 'elem$u4',
inference(demodulation,[status(thm)],[d76,c677]) ).
cnf(d78,plain,
( i = 'elem$u4'
| 'elem$u66' = select('earray$u30','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d77,d68]) ).
cnf(d79,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u28' = 'elem$u4'
| 'elem$u66' = select('earray$u27','elem$u4') ),
inference(superposition,[status(thm)],[d78,d18]) ).
cnf(d80,plain,
s(s(s(s(s(s(s('elem$u7'))))))) != 'elem$u4',
inference(superposition,[status(thm)],[c701,c624]) ).
cnf(d81,plain,
s(s(s(s(s(s('elem$u10')))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d80,c662]) ).
cnf(d82,plain,
s(s(s(s(s('elem$u13'))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d81,c664]) ).
cnf(d83,plain,
s(s(s(s('elem$u16')))) != 'elem$u4',
inference(demodulation,[status(thm)],[d82,c666]) ).
cnf(d84,plain,
s(s(s('elem$u19'))) != 'elem$u4',
inference(demodulation,[status(thm)],[d83,c668]) ).
cnf(d85,plain,
s(s('elem$u22')) != 'elem$u4',
inference(demodulation,[status(thm)],[d84,c671]) ).
cnf(d86,plain,
s('elem$u25') != 'elem$u4',
inference(demodulation,[status(thm)],[d85,c673]) ).
cnf(d87,plain,
'elem$u28' != 'elem$u4',
inference(demodulation,[status(thm)],[d86,c675]) ).
cnf(d88,plain,
( i = 'elem$u4'
| 'elem$u66' = select('earray$u27','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d87,d79]) ).
cnf(d89,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u25' = 'elem$u4'
| 'elem$u66' = select('earray$u24','elem$u4') ),
inference(superposition,[status(thm)],[d88,d17]) ).
cnf(d90,plain,
s(s(s(s(s(s('elem$u7')))))) != 'elem$u4',
inference(superposition,[status(thm)],[c701,c625]) ).
cnf(d91,plain,
s(s(s(s(s('elem$u10'))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d90,c662]) ).
cnf(d92,plain,
s(s(s(s('elem$u13')))) != 'elem$u4',
inference(demodulation,[status(thm)],[d91,c664]) ).
cnf(d93,plain,
s(s(s('elem$u16'))) != 'elem$u4',
inference(demodulation,[status(thm)],[d92,c666]) ).
cnf(d94,plain,
s(s('elem$u19')) != 'elem$u4',
inference(demodulation,[status(thm)],[d93,c668]) ).
cnf(d95,plain,
s('elem$u22') != 'elem$u4',
inference(demodulation,[status(thm)],[d94,c671]) ).
cnf(d96,plain,
'elem$u25' != 'elem$u4',
inference(demodulation,[status(thm)],[d95,c673]) ).
cnf(d97,plain,
( i = 'elem$u4'
| 'elem$u66' = select('earray$u24','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d96,d89]) ).
cnf(d98,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u22' = 'elem$u4'
| 'elem$u66' = select('earray$u21','elem$u4') ),
inference(superposition,[status(thm)],[d97,d16]) ).
cnf(d99,plain,
s(s(s(s(s('elem$u7'))))) != 'elem$u4',
inference(superposition,[status(thm)],[c701,c626]) ).
cnf(d100,plain,
s(s(s(s('elem$u10')))) != 'elem$u4',
inference(demodulation,[status(thm)],[d99,c662]) ).
cnf(d101,plain,
s(s(s('elem$u13'))) != 'elem$u4',
inference(demodulation,[status(thm)],[d100,c664]) ).
cnf(d102,plain,
s(s('elem$u16')) != 'elem$u4',
inference(demodulation,[status(thm)],[d101,c666]) ).
cnf(d103,plain,
s('elem$u19') != 'elem$u4',
inference(demodulation,[status(thm)],[d102,c668]) ).
cnf(d104,plain,
'elem$u22' != 'elem$u4',
inference(demodulation,[status(thm)],[d103,c671]) ).
cnf(d105,plain,
( i = 'elem$u4'
| 'elem$u66' = select('earray$u21','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d104,d98]) ).
cnf(d106,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u19' = 'elem$u4'
| 'elem$u66' = select('earray$u18','elem$u4') ),
inference(superposition,[status(thm)],[d105,d15]) ).
cnf(d107,plain,
s(s(s(s('elem$u7')))) != 'elem$u4',
inference(superposition,[status(thm)],[c701,c627]) ).
cnf(d108,plain,
s(s(s('elem$u10'))) != 'elem$u4',
inference(demodulation,[status(thm)],[d107,c662]) ).
cnf(d109,plain,
s(s('elem$u13')) != 'elem$u4',
inference(demodulation,[status(thm)],[d108,c664]) ).
cnf(d110,plain,
s('elem$u16') != 'elem$u4',
inference(demodulation,[status(thm)],[d109,c666]) ).
cnf(d111,plain,
'elem$u19' != 'elem$u4',
inference(demodulation,[status(thm)],[d110,c668]) ).
cnf(d112,plain,
( i = 'elem$u4'
| 'elem$u66' = select('earray$u18','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d111,d106]) ).
cnf(d113,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u16' = 'elem$u4'
| 'elem$u66' = select('earray$u15','elem$u4') ),
inference(superposition,[status(thm)],[d112,d14]) ).
cnf(d114,plain,
s(s(s('elem$u7'))) != 'elem$u4',
inference(superposition,[status(thm)],[c701,c628]) ).
cnf(d115,plain,
s(s('elem$u10')) != 'elem$u4',
inference(demodulation,[status(thm)],[d114,c662]) ).
cnf(d116,plain,
s('elem$u13') != 'elem$u4',
inference(demodulation,[status(thm)],[d115,c664]) ).
cnf(d117,plain,
'elem$u16' != 'elem$u4',
inference(demodulation,[status(thm)],[d116,c666]) ).
cnf(d118,plain,
( i = 'elem$u4'
| 'elem$u66' = select('earray$u15','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d117,d113]) ).
cnf(d119,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u13' = 'elem$u4'
| 'elem$u66' = select('earray$u12','elem$u4') ),
inference(superposition,[status(thm)],[d118,d13]) ).
cnf(d120,plain,
( i = 'elem$u4'
| 'elem$u66' = 'elem$u5'
| 'elem$u0' = 'elem$u4'
| 'elem$u13' = 'elem$u4' ),
inference(demodulation,[status(thm)],[d119,d12]) ).
cnf(d121,plain,
s(s('elem$u7')) != 'elem$u4',
inference(superposition,[status(thm)],[c701,c629]) ).
cnf(d122,plain,
s('elem$u10') != 'elem$u4',
inference(demodulation,[status(thm)],[d121,c662]) ).
cnf(d123,plain,
'elem$u13' != 'elem$u4',
inference(demodulation,[status(thm)],[d122,c664]) ).
cnf(d124,plain,
( i = 'elem$u4'
| 'elem$u66' = 'elem$u5'
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d123,d120]) ).
cnf(d125,plain,
( 'elem$u66' = 'elem$u5'
| 'elem$u0' = 'elem$u4'
| 'elem$u4' != 'elem$u4' ),
inference(superposition,[status(thm)],[d124,d2]) ).
cnf(d126,plain,
( 'elem$u66' = 'elem$u5'
| 'elem$u0' = 'elem$u4' ),
inference(equality_resolution,[status(thm)],[d125]) ).
cnf(d127,plain,
( 'elem$u0' = 'elem$u4'
| s('elem$u5') = 'elem$u64' ),
inference(superposition,[status(thm)],[d126,c699]) ).
cnf(d128,plain,
( 'elem$u0' = 'elem$u4'
| 'elem$u8' = 'elem$u64' ),
inference(demodulation,[status(thm)],[d127,c703]) ).
cnf(d129,plain,
( 'elem$u0' = 'elem$u4'
| 'elem$u11' = s('elem$u64') ),
inference(superposition,[status(thm)],[d128,c663]) ).
cnf(d130,plain,
( 'elem$u0' = 'elem$u4'
| 'elem$u11' = 'elem$u62' ),
inference(demodulation,[status(thm)],[d129,c698]) ).
cnf(d131,plain,
( 'elem$u11' = 'elem$u62'
| 'elem$u0' != 'elem$u0' ),
inference(superposition,[status(thm)],[d130,d0]) ).
cnf(d132,plain,
'elem$u11' = 'elem$u62',
inference(equality_resolution,[status(thm)],[d131]) ).
cnf(d133,plain,
s('elem$u11') = 'elem$u60',
inference(demodulation,[status(thm)],[c697,d132]) ).
cnf(d134,plain,
'elem$u14' = 'elem$u60',
inference(demodulation,[status(thm)],[d133,c665]) ).
cnf(d135,plain,
s('elem$u14') = 'elem$u58',
inference(demodulation,[status(thm)],[c696,d134]) ).
cnf(d136,plain,
'elem$u17' = 'elem$u58',
inference(demodulation,[status(thm)],[d135,c667]) ).
cnf(d137,plain,
s('elem$u17') = 'elem$u56',
inference(demodulation,[status(thm)],[c695,d136]) ).
cnf(d138,plain,
'elem$u20' = 'elem$u56',
inference(demodulation,[status(thm)],[d137,c670]) ).
cnf(d139,plain,
s('elem$u20') = 'elem$u54',
inference(demodulation,[status(thm)],[c694,d138]) ).
cnf(d140,plain,
'elem$u23' = 'elem$u54',
inference(demodulation,[status(thm)],[d139,c672]) ).
cnf(d141,plain,
s('elem$u23') = 'elem$u52',
inference(demodulation,[status(thm)],[c693,d140]) ).
cnf(d142,plain,
'elem$u26' = 'elem$u52',
inference(demodulation,[status(thm)],[d141,c674]) ).
cnf(d143,plain,
s('elem$u26') = 'elem$u50',
inference(demodulation,[status(thm)],[c692,d142]) ).
cnf(d144,plain,
'elem$u29' = 'elem$u50',
inference(demodulation,[status(thm)],[d143,c676]) ).
cnf(d145,plain,
s('elem$u29') = 'elem$u48',
inference(demodulation,[status(thm)],[c691,d144]) ).
cnf(d146,plain,
'elem$u32' = 'elem$u48',
inference(demodulation,[status(thm)],[d145,c678]) ).
cnf(d147,plain,
s('elem$u32') = 'elem$u46',
inference(demodulation,[status(thm)],[c689,d146]) ).
cnf(d148,plain,
'elem$u35' = 'elem$u46',
inference(demodulation,[status(thm)],[d147,c680]) ).
cnf(d149,plain,
s('elem$u35') = 'elem$u44',
inference(demodulation,[status(thm)],[c688,d148]) ).
cnf(d150,plain,
'elem$u38' = 'elem$u44',
inference(demodulation,[status(thm)],[d149,c682]) ).
cnf(d151,plain,
s('elem$u38') = 'elem$u43',
inference(demodulation,[status(thm)],[c687,d150]) ).
cnf(d152,plain,
'elem$u41' = 'elem$u43',
inference(demodulation,[status(thm)],[d151,c685]) ).
cnf(d153,plain,
$false,
inference(resolution,[status(thm)],[c705,d152]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV567-1.014 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n009.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 14:30:14 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 138.21/20.33 % SZS status Unsatisfiable for theBenchmark.p
% 138.21/20.33 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------