%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWV567-1.013 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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 123.67s 23.76s
% Output : CNFRefutation 123.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 57
% Number of leaves : 65
% Syntax : Number of clauses : 267 ( 222 unt; 44 nHn; 249 RR)
% Number of literals : 344 ( 343 equ; 95 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 60 ( 60 usr; 57 con; 0-3 aty)
% Number of variables : 50 ( 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(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(hyp20,hypothesis,
'earray$u6' = store('earray$u3','elem$u4','elem$u5') ).
cnf(hyp22,hypothesis,
'earray$u62' = store('earray$u60','elem$u4','elem$u61') ).
cnf(hyp23,hypothesis,
'earray$u64' = store('earray$u62','elem$u0','elem$u63') ).
cnf(hyp24,hypothesis,
'earray$u66' = store('earray$u64',i,'elem$u65') ).
cnf(hyp25,hypothesis,
'earray$u9' = store('earray$u6','elem$u7','elem$u8') ).
cnf(hyp26,hypothesis,
'elem$u0' = s(i) ).
cnf(hyp28,hypothesis,
'elem$u10' = s('elem$u7') ).
cnf(hyp29,hypothesis,
'elem$u11' = s('elem$u8') ).
cnf(hyp30,hypothesis,
'elem$u13' = s('elem$u10') ).
cnf(hyp31,hypothesis,
'elem$u14' = s('elem$u11') ).
cnf(hyp32,hypothesis,
'elem$u16' = s('elem$u13') ).
cnf(hyp33,hypothesis,
'elem$u17' = s('elem$u14') ).
cnf(hyp34,hypothesis,
'elem$u19' = s('elem$u16') ).
cnf(hyp36,hypothesis,
'elem$u20' = s('elem$u17') ).
cnf(hyp37,hypothesis,
'elem$u22' = s('elem$u19') ).
cnf(hyp38,hypothesis,
'elem$u23' = s('elem$u20') ).
cnf(hyp39,hypothesis,
'elem$u25' = s('elem$u22') ).
cnf(hyp40,hypothesis,
'elem$u26' = s('elem$u23') ).
cnf(hyp41,hypothesis,
'elem$u28' = s('elem$u25') ).
cnf(hyp42,hypothesis,
'elem$u29' = s('elem$u26') ).
cnf(hyp43,hypothesis,
'elem$u31' = s('elem$u28') ).
cnf(hyp44,hypothesis,
'elem$u32' = s('elem$u29') ).
cnf(hyp45,hypothesis,
'elem$u34' = s('elem$u31') ).
cnf(hyp46,hypothesis,
'elem$u35' = s('elem$u32') ).
cnf(hyp47,hypothesis,
'elem$u37' = s('elem$u34') ).
cnf(hyp48,hypothesis,
'elem$u38' = s('elem$u35') ).
cnf(hyp49,hypothesis,
'elem$u4' = s('elem$u0') ).
cnf(hyp51,hypothesis,
s('elem$u41') = 'elem$u40' ).
cnf(hyp52,hypothesis,
s('elem$u43') = 'elem$u41' ).
cnf(hyp53,hypothesis,
s('elem$u45') = 'elem$u43' ).
cnf(hyp54,hypothesis,
s('elem$u47') = 'elem$u45' ).
cnf(hyp55,hypothesis,
s('elem$u49') = 'elem$u47' ).
cnf(hyp57,hypothesis,
s('elem$u51') = 'elem$u49' ).
cnf(hyp58,hypothesis,
s('elem$u53') = 'elem$u51' ).
cnf(hyp59,hypothesis,
s('elem$u55') = 'elem$u53' ).
cnf(hyp60,hypothesis,
s('elem$u57') = 'elem$u55' ).
cnf(hyp61,hypothesis,
s('elem$u59') = 'elem$u57' ).
cnf(hyp62,hypothesis,
s('elem$u61') = 'elem$u59' ).
cnf(hyp65,hypothesis,
'elem$u7' = s('elem$u4') ).
cnf(hyp66,hypothesis,
'elem$u8' = s('elem$u5') ).
cnf(hyp67,hypothesis,
'earray$u39' = 'earray$u66' ).
cnf(goal,negated_conjecture,
'elem$u38' != 'elem$u40' ).
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(c537,plain,
s(s(s(s(s(s(s(s(s(s(s(X0))))))))))) != X0,
inference(clausification,[status(esa)],[as11]) ).
cnf(c538,plain,
s(s(s(s(s(s(s(s(s(s(X0)))))))))) != X0,
inference(clausification,[status(esa)],[as10]) ).
cnf(c539,plain,
s(s(s(s(s(s(s(s(s(X0))))))))) != X0,
inference(clausification,[status(esa)],[as9]) ).
cnf(c540,plain,
s(s(s(s(s(s(s(s(X0)))))))) != X0,
inference(clausification,[status(esa)],[as8]) ).
cnf(c541,plain,
s(s(s(s(s(s(s(X0))))))) != X0,
inference(clausification,[status(esa)],[as7]) ).
cnf(c542,plain,
s(s(s(s(s(s(X0)))))) != X0,
inference(clausification,[status(esa)],[as6]) ).
cnf(c543,plain,
s(s(s(s(s(X0))))) != X0,
inference(clausification,[status(esa)],[as5]) ).
cnf(c544,plain,
s(s(s(s(X0)))) != X0,
inference(clausification,[status(esa)],[as4]) ).
cnf(c545,plain,
s(s(s(X0))) != X0,
inference(clausification,[status(esa)],[as3]) ).
cnf(c546,plain,
s(s(X0)) != X0,
inference(clausification,[status(esa)],[as2]) ).
cnf(c547,plain,
s(X0) != X0,
inference(clausification,[status(esa)],[as1]) ).
cnf(c548,plain,
'earray$u12' = store('earray$u9','elem$u10','elem$u11'),
inference(clausification,[status(esa)],[hyp0]) ).
cnf(c549,plain,
'earray$u15' = store('earray$u12','elem$u13','elem$u14'),
inference(clausification,[status(esa)],[hyp1]) ).
cnf(c550,plain,
'earray$u18' = store('earray$u15','elem$u16','elem$u17'),
inference(clausification,[status(esa)],[hyp2]) ).
cnf(c551,plain,
'earray$u21' = store('earray$u18','elem$u19','elem$u20'),
inference(clausification,[status(esa)],[hyp3]) ).
cnf(c552,plain,
'earray$u24' = store('earray$u21','elem$u22','elem$u23'),
inference(clausification,[status(esa)],[hyp4]) ).
cnf(c553,plain,
'earray$u27' = store('earray$u24','elem$u25','elem$u26'),
inference(clausification,[status(esa)],[hyp5]) ).
cnf(c555,plain,
'earray$u30' = store('earray$u27','elem$u28','elem$u29'),
inference(clausification,[status(esa)],[hyp7]) ).
cnf(c556,plain,
'earray$u33' = store('earray$u30','elem$u31','elem$u32'),
inference(clausification,[status(esa)],[hyp8]) ).
cnf(c557,plain,
'earray$u36' = store('earray$u33','elem$u34','elem$u35'),
inference(clausification,[status(esa)],[hyp9]) ).
cnf(c558,plain,
'earray$u39' = store('earray$u36','elem$u37','elem$u38'),
inference(clausification,[status(esa)],[hyp10]) ).
cnf(c568,plain,
'earray$u6' = store('earray$u3','elem$u4','elem$u5'),
inference(clausification,[status(esa)],[hyp20]) ).
cnf(c570,plain,
'earray$u62' = store('earray$u60','elem$u4','elem$u61'),
inference(clausification,[status(esa)],[hyp22]) ).
cnf(c571,plain,
'earray$u64' = store('earray$u62','elem$u0','elem$u63'),
inference(clausification,[status(esa)],[hyp23]) ).
cnf(c572,plain,
'earray$u66' = store('earray$u64',i,'elem$u65'),
inference(clausification,[status(esa)],[hyp24]) ).
cnf(c573,plain,
'earray$u9' = store('earray$u6','elem$u7','elem$u8'),
inference(clausification,[status(esa)],[hyp25]) ).
cnf(c574,plain,
'elem$u0' = s(i),
inference(clausification,[status(esa)],[hyp26]) ).
cnf(c576,plain,
'elem$u10' = s('elem$u7'),
inference(clausification,[status(esa)],[hyp28]) ).
cnf(c577,plain,
'elem$u11' = s('elem$u8'),
inference(clausification,[status(esa)],[hyp29]) ).
cnf(c578,plain,
'elem$u13' = s('elem$u10'),
inference(clausification,[status(esa)],[hyp30]) ).
cnf(c579,plain,
'elem$u14' = s('elem$u11'),
inference(clausification,[status(esa)],[hyp31]) ).
cnf(c580,plain,
'elem$u16' = s('elem$u13'),
inference(clausification,[status(esa)],[hyp32]) ).
cnf(c581,plain,
'elem$u17' = s('elem$u14'),
inference(clausification,[status(esa)],[hyp33]) ).
cnf(c582,plain,
'elem$u19' = s('elem$u16'),
inference(clausification,[status(esa)],[hyp34]) ).
cnf(c584,plain,
'elem$u20' = s('elem$u17'),
inference(clausification,[status(esa)],[hyp36]) ).
cnf(c585,plain,
'elem$u22' = s('elem$u19'),
inference(clausification,[status(esa)],[hyp37]) ).
cnf(c586,plain,
'elem$u23' = s('elem$u20'),
inference(clausification,[status(esa)],[hyp38]) ).
cnf(c587,plain,
'elem$u25' = s('elem$u22'),
inference(clausification,[status(esa)],[hyp39]) ).
cnf(c588,plain,
'elem$u26' = s('elem$u23'),
inference(clausification,[status(esa)],[hyp40]) ).
cnf(c589,plain,
'elem$u28' = s('elem$u25'),
inference(clausification,[status(esa)],[hyp41]) ).
cnf(c590,plain,
'elem$u29' = s('elem$u26'),
inference(clausification,[status(esa)],[hyp42]) ).
cnf(c591,plain,
'elem$u31' = s('elem$u28'),
inference(clausification,[status(esa)],[hyp43]) ).
cnf(c592,plain,
'elem$u32' = s('elem$u29'),
inference(clausification,[status(esa)],[hyp44]) ).
cnf(c593,plain,
'elem$u34' = s('elem$u31'),
inference(clausification,[status(esa)],[hyp45]) ).
cnf(c594,plain,
'elem$u35' = s('elem$u32'),
inference(clausification,[status(esa)],[hyp46]) ).
cnf(c595,plain,
'elem$u37' = s('elem$u34'),
inference(clausification,[status(esa)],[hyp47]) ).
cnf(c596,plain,
'elem$u38' = s('elem$u35'),
inference(clausification,[status(esa)],[hyp48]) ).
cnf(c597,plain,
'elem$u4' = s('elem$u0'),
inference(clausification,[status(esa)],[hyp49]) ).
cnf(c599,plain,
s('elem$u41') = 'elem$u40',
inference(clausification,[status(esa)],[hyp51]) ).
cnf(c600,plain,
s('elem$u43') = 'elem$u41',
inference(clausification,[status(esa)],[hyp52]) ).
cnf(c601,plain,
s('elem$u45') = 'elem$u43',
inference(clausification,[status(esa)],[hyp53]) ).
cnf(c602,plain,
s('elem$u47') = 'elem$u45',
inference(clausification,[status(esa)],[hyp54]) ).
cnf(c603,plain,
s('elem$u49') = 'elem$u47',
inference(clausification,[status(esa)],[hyp55]) ).
cnf(c605,plain,
s('elem$u51') = 'elem$u49',
inference(clausification,[status(esa)],[hyp57]) ).
cnf(c606,plain,
s('elem$u53') = 'elem$u51',
inference(clausification,[status(esa)],[hyp58]) ).
cnf(c607,plain,
s('elem$u55') = 'elem$u53',
inference(clausification,[status(esa)],[hyp59]) ).
cnf(c608,plain,
s('elem$u57') = 'elem$u55',
inference(clausification,[status(esa)],[hyp60]) ).
cnf(c609,plain,
s('elem$u59') = 'elem$u57',
inference(clausification,[status(esa)],[hyp61]) ).
cnf(c610,plain,
s('elem$u61') = 'elem$u59',
inference(clausification,[status(esa)],[hyp62]) ).
cnf(c613,plain,
'elem$u7' = s('elem$u4'),
inference(clausification,[status(esa)],[hyp65]) ).
cnf(c614,plain,
'elem$u8' = s('elem$u5'),
inference(clausification,[status(esa)],[hyp66]) ).
cnf(c615,plain,
'earray$u39' = 'earray$u66',
inference(clausification,[status(esa)],[hyp67]) ).
cnf(c616,plain,
'elem$u38' != 'elem$u40',
inference(clausification,[status(esa)],[goal]) ).
cnf(d0,plain,
'elem$u4' != 'elem$u0',
inference(superposition,[status(thm)],[c597,c547]) ).
cnf(d1,plain,
s('elem$u0') != i,
inference(superposition,[status(thm)],[c574,c546]) ).
cnf(d2,plain,
'elem$u4' != i,
inference(demodulation,[status(thm)],[d1,c597]) ).
cnf(d3,plain,
( 'elem$u10' = X0
| select('earray$u12',X0) = select('earray$u9',X0) ),
inference(superposition,[status(thm)],[c548,c1]) ).
cnf(d4,plain,
select('earray$u6','elem$u4') = 'elem$u5',
inference(superposition,[status(thm)],[c568,c0]) ).
cnf(d5,plain,
( 'elem$u7' = X0
| select('earray$u9',X0) = select('earray$u6',X0) ),
inference(superposition,[status(thm)],[c573,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)],[c613,c547]) ).
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)],[c613,c546]) ).
cnf(d11,plain,
'elem$u10' != 'elem$u4',
inference(demodulation,[status(thm)],[d10,c576]) ).
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)],[c549,c1]) ).
cnf(d14,plain,
( 'elem$u16' = X0
| select('earray$u18',X0) = select('earray$u15',X0) ),
inference(superposition,[status(thm)],[c550,c1]) ).
cnf(d15,plain,
( 'elem$u19' = X0
| select('earray$u21',X0) = select('earray$u18',X0) ),
inference(superposition,[status(thm)],[c551,c1]) ).
cnf(d16,plain,
( 'elem$u22' = X0
| select('earray$u24',X0) = select('earray$u21',X0) ),
inference(superposition,[status(thm)],[c552,c1]) ).
cnf(d17,plain,
( 'elem$u25' = X0
| select('earray$u27',X0) = select('earray$u24',X0) ),
inference(superposition,[status(thm)],[c553,c1]) ).
cnf(d18,plain,
( 'elem$u28' = X0
| select('earray$u30',X0) = select('earray$u27',X0) ),
inference(superposition,[status(thm)],[c555,c1]) ).
cnf(d19,plain,
( 'elem$u31' = X0
| select('earray$u33',X0) = select('earray$u30',X0) ),
inference(superposition,[status(thm)],[c556,c1]) ).
cnf(d20,plain,
( 'elem$u34' = X0
| select('earray$u36',X0) = select('earray$u33',X0) ),
inference(superposition,[status(thm)],[c557,c1]) ).
cnf(d21,plain,
( 'elem$u37' = X0
| select('earray$u39',X0) = select('earray$u36',X0) ),
inference(superposition,[status(thm)],[c558,c1]) ).
cnf(d22,plain,
select('earray$u62','elem$u4') = 'elem$u61',
inference(superposition,[status(thm)],[c570,c0]) ).
cnf(d23,plain,
( 'elem$u0' = X0
| select('earray$u64',X0) = select('earray$u62',X0) ),
inference(superposition,[status(thm)],[c571,c1]) ).
cnf(d24,plain,
'earray$u39' = store('earray$u64',i,'elem$u65'),
inference(demodulation,[status(thm)],[c572,c615]) ).
cnf(d25,plain,
( i = X0
| select('earray$u39',X0) = select('earray$u64',X0) ),
inference(superposition,[status(thm)],[d24,c1]) ).
cnf(d26,plain,
( i = X0
| 'elem$u0' = X0
| select('earray$u39',X0) = select('earray$u62',X0) ),
inference(superposition,[status(thm)],[d25,d23]) ).
cnf(d27,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| select('earray$u39','elem$u4') = 'elem$u61' ),
inference(superposition,[status(thm)],[d26,d22]) ).
cnf(d28,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u37' = 'elem$u4'
| 'elem$u61' = select('earray$u36','elem$u4') ),
inference(superposition,[status(thm)],[d27,d21]) ).
cnf(d29,plain,
s(s(s(s(s(s(s(s(s(s('elem$u7')))))))))) != 'elem$u4',
inference(superposition,[status(thm)],[c613,c537]) ).
cnf(d30,plain,
s(s(s(s(s(s(s(s(s('elem$u10'))))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d29,c576]) ).
cnf(d31,plain,
s(s(s(s(s(s(s(s('elem$u13')))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d30,c578]) ).
cnf(d32,plain,
s(s(s(s(s(s(s('elem$u16'))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d31,c580]) ).
cnf(d33,plain,
s(s(s(s(s(s('elem$u19')))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d32,c582]) ).
cnf(d34,plain,
s(s(s(s(s('elem$u22'))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d33,c585]) ).
cnf(d35,plain,
s(s(s(s('elem$u25')))) != 'elem$u4',
inference(demodulation,[status(thm)],[d34,c587]) ).
cnf(d36,plain,
s(s(s('elem$u28'))) != 'elem$u4',
inference(demodulation,[status(thm)],[d35,c589]) ).
cnf(d37,plain,
s(s('elem$u31')) != 'elem$u4',
inference(demodulation,[status(thm)],[d36,c591]) ).
cnf(d38,plain,
s('elem$u34') != 'elem$u4',
inference(demodulation,[status(thm)],[d37,c593]) ).
cnf(d39,plain,
'elem$u37' != 'elem$u4',
inference(demodulation,[status(thm)],[d38,c595]) ).
cnf(d40,plain,
( i = 'elem$u4'
| 'elem$u61' = select('earray$u36','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d39,d28]) ).
cnf(d41,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u34' = 'elem$u4'
| 'elem$u61' = select('earray$u33','elem$u4') ),
inference(superposition,[status(thm)],[d40,d20]) ).
cnf(d42,plain,
s(s(s(s(s(s(s(s(s('elem$u7'))))))))) != 'elem$u4',
inference(superposition,[status(thm)],[c613,c538]) ).
cnf(d43,plain,
s(s(s(s(s(s(s(s('elem$u10')))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d42,c576]) ).
cnf(d44,plain,
s(s(s(s(s(s(s('elem$u13'))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d43,c578]) ).
cnf(d45,plain,
s(s(s(s(s(s('elem$u16')))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d44,c580]) ).
cnf(d46,plain,
s(s(s(s(s('elem$u19'))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d45,c582]) ).
cnf(d47,plain,
s(s(s(s('elem$u22')))) != 'elem$u4',
inference(demodulation,[status(thm)],[d46,c585]) ).
cnf(d48,plain,
s(s(s('elem$u25'))) != 'elem$u4',
inference(demodulation,[status(thm)],[d47,c587]) ).
cnf(d49,plain,
s(s('elem$u28')) != 'elem$u4',
inference(demodulation,[status(thm)],[d48,c589]) ).
cnf(d50,plain,
s('elem$u31') != 'elem$u4',
inference(demodulation,[status(thm)],[d49,c591]) ).
cnf(d51,plain,
'elem$u34' != 'elem$u4',
inference(demodulation,[status(thm)],[d50,c593]) ).
cnf(d52,plain,
( i = 'elem$u4'
| 'elem$u61' = select('earray$u33','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d51,d41]) ).
cnf(d53,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u31' = 'elem$u4'
| 'elem$u61' = select('earray$u30','elem$u4') ),
inference(superposition,[status(thm)],[d52,d19]) ).
cnf(d54,plain,
s(s(s(s(s(s(s(s('elem$u7')))))))) != 'elem$u4',
inference(superposition,[status(thm)],[c613,c539]) ).
cnf(d55,plain,
s(s(s(s(s(s(s('elem$u10'))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d54,c576]) ).
cnf(d56,plain,
s(s(s(s(s(s('elem$u13')))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d55,c578]) ).
cnf(d57,plain,
s(s(s(s(s('elem$u16'))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d56,c580]) ).
cnf(d58,plain,
s(s(s(s('elem$u19')))) != 'elem$u4',
inference(demodulation,[status(thm)],[d57,c582]) ).
cnf(d59,plain,
s(s(s('elem$u22'))) != 'elem$u4',
inference(demodulation,[status(thm)],[d58,c585]) ).
cnf(d60,plain,
s(s('elem$u25')) != 'elem$u4',
inference(demodulation,[status(thm)],[d59,c587]) ).
cnf(d61,plain,
s('elem$u28') != 'elem$u4',
inference(demodulation,[status(thm)],[d60,c589]) ).
cnf(d62,plain,
'elem$u31' != 'elem$u4',
inference(demodulation,[status(thm)],[d61,c591]) ).
cnf(d63,plain,
( i = 'elem$u4'
| 'elem$u61' = select('earray$u30','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d62,d53]) ).
cnf(d64,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u28' = 'elem$u4'
| 'elem$u61' = select('earray$u27','elem$u4') ),
inference(superposition,[status(thm)],[d63,d18]) ).
cnf(d65,plain,
s(s(s(s(s(s(s('elem$u7'))))))) != 'elem$u4',
inference(superposition,[status(thm)],[c613,c540]) ).
cnf(d66,plain,
s(s(s(s(s(s('elem$u10')))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d65,c576]) ).
cnf(d67,plain,
s(s(s(s(s('elem$u13'))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d66,c578]) ).
cnf(d68,plain,
s(s(s(s('elem$u16')))) != 'elem$u4',
inference(demodulation,[status(thm)],[d67,c580]) ).
cnf(d69,plain,
s(s(s('elem$u19'))) != 'elem$u4',
inference(demodulation,[status(thm)],[d68,c582]) ).
cnf(d70,plain,
s(s('elem$u22')) != 'elem$u4',
inference(demodulation,[status(thm)],[d69,c585]) ).
cnf(d71,plain,
s('elem$u25') != 'elem$u4',
inference(demodulation,[status(thm)],[d70,c587]) ).
cnf(d72,plain,
'elem$u28' != 'elem$u4',
inference(demodulation,[status(thm)],[d71,c589]) ).
cnf(d73,plain,
( i = 'elem$u4'
| 'elem$u61' = select('earray$u27','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d72,d64]) ).
cnf(d74,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u25' = 'elem$u4'
| 'elem$u61' = select('earray$u24','elem$u4') ),
inference(superposition,[status(thm)],[d73,d17]) ).
cnf(d75,plain,
s(s(s(s(s(s('elem$u7')))))) != 'elem$u4',
inference(superposition,[status(thm)],[c613,c541]) ).
cnf(d76,plain,
s(s(s(s(s('elem$u10'))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d75,c576]) ).
cnf(d77,plain,
s(s(s(s('elem$u13')))) != 'elem$u4',
inference(demodulation,[status(thm)],[d76,c578]) ).
cnf(d78,plain,
s(s(s('elem$u16'))) != 'elem$u4',
inference(demodulation,[status(thm)],[d77,c580]) ).
cnf(d79,plain,
s(s('elem$u19')) != 'elem$u4',
inference(demodulation,[status(thm)],[d78,c582]) ).
cnf(d80,plain,
s('elem$u22') != 'elem$u4',
inference(demodulation,[status(thm)],[d79,c585]) ).
cnf(d81,plain,
'elem$u25' != 'elem$u4',
inference(demodulation,[status(thm)],[d80,c587]) ).
cnf(d82,plain,
( i = 'elem$u4'
| 'elem$u61' = select('earray$u24','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d81,d74]) ).
cnf(d83,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u22' = 'elem$u4'
| 'elem$u61' = select('earray$u21','elem$u4') ),
inference(superposition,[status(thm)],[d82,d16]) ).
cnf(d84,plain,
s(s(s(s(s('elem$u7'))))) != 'elem$u4',
inference(superposition,[status(thm)],[c613,c542]) ).
cnf(d85,plain,
s(s(s(s('elem$u10')))) != 'elem$u4',
inference(demodulation,[status(thm)],[d84,c576]) ).
cnf(d86,plain,
s(s(s('elem$u13'))) != 'elem$u4',
inference(demodulation,[status(thm)],[d85,c578]) ).
cnf(d87,plain,
s(s('elem$u16')) != 'elem$u4',
inference(demodulation,[status(thm)],[d86,c580]) ).
cnf(d88,plain,
s('elem$u19') != 'elem$u4',
inference(demodulation,[status(thm)],[d87,c582]) ).
cnf(d89,plain,
'elem$u22' != 'elem$u4',
inference(demodulation,[status(thm)],[d88,c585]) ).
cnf(d90,plain,
( i = 'elem$u4'
| 'elem$u61' = select('earray$u21','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d89,d83]) ).
cnf(d91,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u19' = 'elem$u4'
| 'elem$u61' = select('earray$u18','elem$u4') ),
inference(superposition,[status(thm)],[d90,d15]) ).
cnf(d92,plain,
s(s(s(s('elem$u7')))) != 'elem$u4',
inference(superposition,[status(thm)],[c613,c543]) ).
cnf(d93,plain,
s(s(s('elem$u10'))) != 'elem$u4',
inference(demodulation,[status(thm)],[d92,c576]) ).
cnf(d94,plain,
s(s('elem$u13')) != 'elem$u4',
inference(demodulation,[status(thm)],[d93,c578]) ).
cnf(d95,plain,
s('elem$u16') != 'elem$u4',
inference(demodulation,[status(thm)],[d94,c580]) ).
cnf(d96,plain,
'elem$u19' != 'elem$u4',
inference(demodulation,[status(thm)],[d95,c582]) ).
cnf(d97,plain,
( i = 'elem$u4'
| 'elem$u61' = select('earray$u18','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d96,d91]) ).
cnf(d98,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u16' = 'elem$u4'
| 'elem$u61' = select('earray$u15','elem$u4') ),
inference(superposition,[status(thm)],[d97,d14]) ).
cnf(d99,plain,
s(s(s('elem$u7'))) != 'elem$u4',
inference(superposition,[status(thm)],[c613,c544]) ).
cnf(d100,plain,
s(s('elem$u10')) != 'elem$u4',
inference(demodulation,[status(thm)],[d99,c576]) ).
cnf(d101,plain,
s('elem$u13') != 'elem$u4',
inference(demodulation,[status(thm)],[d100,c578]) ).
cnf(d102,plain,
'elem$u16' != 'elem$u4',
inference(demodulation,[status(thm)],[d101,c580]) ).
cnf(d103,plain,
( i = 'elem$u4'
| 'elem$u61' = select('earray$u15','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d102,d98]) ).
cnf(d104,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u13' = 'elem$u4'
| 'elem$u61' = select('earray$u12','elem$u4') ),
inference(superposition,[status(thm)],[d103,d13]) ).
cnf(d105,plain,
( i = 'elem$u4'
| 'elem$u61' = 'elem$u5'
| 'elem$u0' = 'elem$u4'
| 'elem$u13' = 'elem$u4' ),
inference(demodulation,[status(thm)],[d104,d12]) ).
cnf(d106,plain,
s(s('elem$u7')) != 'elem$u4',
inference(superposition,[status(thm)],[c613,c545]) ).
cnf(d107,plain,
s('elem$u10') != 'elem$u4',
inference(demodulation,[status(thm)],[d106,c576]) ).
cnf(d108,plain,
'elem$u13' != 'elem$u4',
inference(demodulation,[status(thm)],[d107,c578]) ).
cnf(d109,plain,
( i = 'elem$u4'
| 'elem$u61' = 'elem$u5'
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d108,d105]) ).
cnf(d110,plain,
( 'elem$u61' = 'elem$u5'
| 'elem$u0' = 'elem$u4'
| 'elem$u4' != 'elem$u4' ),
inference(superposition,[status(thm)],[d109,d2]) ).
cnf(d111,plain,
( 'elem$u61' = 'elem$u5'
| 'elem$u0' = 'elem$u4' ),
inference(equality_resolution,[status(thm)],[d110]) ).
cnf(d112,plain,
( 'elem$u0' = 'elem$u4'
| s('elem$u5') = 'elem$u59' ),
inference(superposition,[status(thm)],[d111,c610]) ).
cnf(d113,plain,
( 'elem$u0' = 'elem$u4'
| 'elem$u8' = 'elem$u59' ),
inference(demodulation,[status(thm)],[d112,c614]) ).
cnf(d114,plain,
( 'elem$u0' = 'elem$u4'
| 'elem$u11' = s('elem$u59') ),
inference(superposition,[status(thm)],[d113,c577]) ).
cnf(d115,plain,
( 'elem$u0' = 'elem$u4'
| 'elem$u11' = 'elem$u57' ),
inference(demodulation,[status(thm)],[d114,c609]) ).
cnf(d116,plain,
( 'elem$u11' = 'elem$u57'
| 'elem$u0' != 'elem$u0' ),
inference(superposition,[status(thm)],[d115,d0]) ).
cnf(d117,plain,
'elem$u11' = 'elem$u57',
inference(equality_resolution,[status(thm)],[d116]) ).
cnf(d118,plain,
s('elem$u11') = 'elem$u55',
inference(demodulation,[status(thm)],[c608,d117]) ).
cnf(d119,plain,
'elem$u14' = 'elem$u55',
inference(demodulation,[status(thm)],[d118,c579]) ).
cnf(d120,plain,
s('elem$u14') = 'elem$u53',
inference(demodulation,[status(thm)],[c607,d119]) ).
cnf(d121,plain,
'elem$u17' = 'elem$u53',
inference(demodulation,[status(thm)],[d120,c581]) ).
cnf(d122,plain,
s('elem$u17') = 'elem$u51',
inference(demodulation,[status(thm)],[c606,d121]) ).
cnf(d123,plain,
'elem$u20' = 'elem$u51',
inference(demodulation,[status(thm)],[d122,c584]) ).
cnf(d124,plain,
s('elem$u20') = 'elem$u49',
inference(demodulation,[status(thm)],[c605,d123]) ).
cnf(d125,plain,
'elem$u23' = 'elem$u49',
inference(demodulation,[status(thm)],[d124,c586]) ).
cnf(d126,plain,
s('elem$u23') = 'elem$u47',
inference(demodulation,[status(thm)],[c603,d125]) ).
cnf(d127,plain,
'elem$u26' = 'elem$u47',
inference(demodulation,[status(thm)],[d126,c588]) ).
cnf(d128,plain,
s('elem$u26') = 'elem$u45',
inference(demodulation,[status(thm)],[c602,d127]) ).
cnf(d129,plain,
'elem$u29' = 'elem$u45',
inference(demodulation,[status(thm)],[d128,c590]) ).
cnf(d130,plain,
s('elem$u29') = 'elem$u43',
inference(demodulation,[status(thm)],[c601,d129]) ).
cnf(d131,plain,
'elem$u32' = 'elem$u43',
inference(demodulation,[status(thm)],[d130,c592]) ).
cnf(d132,plain,
s('elem$u32') = 'elem$u41',
inference(demodulation,[status(thm)],[c600,d131]) ).
cnf(d133,plain,
'elem$u35' = 'elem$u41',
inference(demodulation,[status(thm)],[d132,c594]) ).
cnf(d134,plain,
s('elem$u35') = 'elem$u40',
inference(demodulation,[status(thm)],[c599,d133]) ).
cnf(d135,plain,
'elem$u38' = 'elem$u40',
inference(demodulation,[status(thm)],[d134,c596]) ).
cnf(d136,plain,
$false,
inference(resolution,[status(thm)],[c616,d135]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV567-1.013 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.41 % Computer : n019.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Sat Sep 26 14:29:34 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.42 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 123.67/23.76 % SZS status Unsatisfiable for theBenchmark.p
% 123.67/23.76 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------