%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWV567-1.015 : 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 : n016.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:21 AM UTC 2026
% Result : Unsatisfiable 139.16s 62.64s
% Output : CNFRefutation 139.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 67
% Number of leaves : 75
% Syntax : Number of clauses : 322 ( 250 unt; 72 nHn; 302 RR)
% Number of literals : 432 ( 431 equ; 124 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 14 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 68 ( 68 usr; 65 con; 0-3 aty)
% Number of variables : 56 ( 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(as13,axiom,
s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))) != X0 ).
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(hyp12,hypothesis,
'earray$u45' = store('earray$u42','elem$u43','elem$u44') ).
cnf(hyp19,hypothesis,
'earray$u6' = store('earray$u3','elem$u4','elem$u5') ).
cnf(hyp26,hypothesis,
'earray$u72' = store('earray$u70','elem$u4','elem$u71') ).
cnf(hyp27,hypothesis,
'earray$u74' = store('earray$u72','elem$u0','elem$u73') ).
cnf(hyp28,hypothesis,
'earray$u76' = store('earray$u74',i,'elem$u75') ).
cnf(hyp29,hypothesis,
'earray$u9' = store('earray$u6','elem$u7','elem$u8') ).
cnf(hyp30,hypothesis,
'elem$u0' = s(i) ).
cnf(hyp32,hypothesis,
'elem$u10' = s('elem$u7') ).
cnf(hyp33,hypothesis,
'elem$u11' = s('elem$u8') ).
cnf(hyp34,hypothesis,
'elem$u13' = s('elem$u10') ).
cnf(hyp35,hypothesis,
'elem$u14' = s('elem$u11') ).
cnf(hyp36,hypothesis,
'elem$u16' = s('elem$u13') ).
cnf(hyp37,hypothesis,
'elem$u17' = s('elem$u14') ).
cnf(hyp38,hypothesis,
'elem$u19' = s('elem$u16') ).
cnf(hyp40,hypothesis,
'elem$u20' = s('elem$u17') ).
cnf(hyp41,hypothesis,
'elem$u22' = s('elem$u19') ).
cnf(hyp42,hypothesis,
'elem$u23' = s('elem$u20') ).
cnf(hyp43,hypothesis,
'elem$u25' = s('elem$u22') ).
cnf(hyp44,hypothesis,
'elem$u26' = s('elem$u23') ).
cnf(hyp45,hypothesis,
'elem$u28' = s('elem$u25') ).
cnf(hyp46,hypothesis,
'elem$u29' = s('elem$u26') ).
cnf(hyp47,hypothesis,
'elem$u31' = s('elem$u28') ).
cnf(hyp48,hypothesis,
'elem$u32' = s('elem$u29') ).
cnf(hyp49,hypothesis,
'elem$u34' = s('elem$u31') ).
cnf(hyp50,hypothesis,
'elem$u35' = s('elem$u32') ).
cnf(hyp51,hypothesis,
'elem$u37' = s('elem$u34') ).
cnf(hyp52,hypothesis,
'elem$u38' = s('elem$u35') ).
cnf(hyp53,hypothesis,
'elem$u4' = s('elem$u0') ).
cnf(hyp54,hypothesis,
'elem$u40' = s('elem$u37') ).
cnf(hyp55,hypothesis,
'elem$u41' = s('elem$u38') ).
cnf(hyp56,hypothesis,
'elem$u43' = s('elem$u40') ).
cnf(hyp57,hypothesis,
'elem$u44' = s('elem$u41') ).
cnf(hyp59,hypothesis,
s('elem$u47') = 'elem$u46' ).
cnf(hyp60,hypothesis,
s('elem$u49') = 'elem$u47' ).
cnf(hyp62,hypothesis,
s('elem$u51') = 'elem$u49' ).
cnf(hyp63,hypothesis,
s('elem$u53') = 'elem$u51' ).
cnf(hyp64,hypothesis,
s('elem$u55') = 'elem$u53' ).
cnf(hyp65,hypothesis,
s('elem$u57') = 'elem$u55' ).
cnf(hyp66,hypothesis,
s('elem$u59') = 'elem$u57' ).
cnf(hyp67,hypothesis,
s('elem$u61') = 'elem$u59' ).
cnf(hyp68,hypothesis,
s('elem$u63') = 'elem$u61' ).
cnf(hyp69,hypothesis,
s('elem$u65') = 'elem$u63' ).
cnf(hyp70,hypothesis,
s('elem$u67') = 'elem$u65' ).
cnf(hyp71,hypothesis,
s('elem$u69') = 'elem$u67' ).
cnf(hyp72,hypothesis,
'elem$u7' = s('elem$u4') ).
cnf(hyp73,hypothesis,
s('elem$u71') = 'elem$u69' ).
cnf(hyp76,hypothesis,
'elem$u8' = s('elem$u5') ).
cnf(hyp77,hypothesis,
'earray$u45' = 'earray$u76' ).
cnf(goal,negated_conjecture,
'elem$u44' != 'elem$u46' ).
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(c709,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))) != X0,
inference(clausification,[status(esa)],[as13]) ).
cnf(c710,plain,
s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))) != X0,
inference(clausification,[status(esa)],[as12]) ).
cnf(c711,plain,
s(s(s(s(s(s(s(s(s(s(s(X0))))))))))) != X0,
inference(clausification,[status(esa)],[as11]) ).
cnf(c712,plain,
s(s(s(s(s(s(s(s(s(s(X0)))))))))) != X0,
inference(clausification,[status(esa)],[as10]) ).
cnf(c713,plain,
s(s(s(s(s(s(s(s(s(X0))))))))) != X0,
inference(clausification,[status(esa)],[as9]) ).
cnf(c714,plain,
s(s(s(s(s(s(s(s(X0)))))))) != X0,
inference(clausification,[status(esa)],[as8]) ).
cnf(c715,plain,
s(s(s(s(s(s(s(X0))))))) != X0,
inference(clausification,[status(esa)],[as7]) ).
cnf(c716,plain,
s(s(s(s(s(s(X0)))))) != X0,
inference(clausification,[status(esa)],[as6]) ).
cnf(c717,plain,
s(s(s(s(s(X0))))) != X0,
inference(clausification,[status(esa)],[as5]) ).
cnf(c718,plain,
s(s(s(s(X0)))) != X0,
inference(clausification,[status(esa)],[as4]) ).
cnf(c719,plain,
s(s(s(X0))) != X0,
inference(clausification,[status(esa)],[as3]) ).
cnf(c720,plain,
s(s(X0)) != X0,
inference(clausification,[status(esa)],[as2]) ).
cnf(c721,plain,
s(X0) != X0,
inference(clausification,[status(esa)],[as1]) ).
cnf(c722,plain,
'earray$u12' = store('earray$u9','elem$u10','elem$u11'),
inference(clausification,[status(esa)],[hyp0]) ).
cnf(c723,plain,
'earray$u15' = store('earray$u12','elem$u13','elem$u14'),
inference(clausification,[status(esa)],[hyp1]) ).
cnf(c724,plain,
'earray$u18' = store('earray$u15','elem$u16','elem$u17'),
inference(clausification,[status(esa)],[hyp2]) ).
cnf(c725,plain,
'earray$u21' = store('earray$u18','elem$u19','elem$u20'),
inference(clausification,[status(esa)],[hyp3]) ).
cnf(c726,plain,
'earray$u24' = store('earray$u21','elem$u22','elem$u23'),
inference(clausification,[status(esa)],[hyp4]) ).
cnf(c727,plain,
'earray$u27' = store('earray$u24','elem$u25','elem$u26'),
inference(clausification,[status(esa)],[hyp5]) ).
cnf(c729,plain,
'earray$u30' = store('earray$u27','elem$u28','elem$u29'),
inference(clausification,[status(esa)],[hyp7]) ).
cnf(c730,plain,
'earray$u33' = store('earray$u30','elem$u31','elem$u32'),
inference(clausification,[status(esa)],[hyp8]) ).
cnf(c731,plain,
'earray$u36' = store('earray$u33','elem$u34','elem$u35'),
inference(clausification,[status(esa)],[hyp9]) ).
cnf(c732,plain,
'earray$u39' = store('earray$u36','elem$u37','elem$u38'),
inference(clausification,[status(esa)],[hyp10]) ).
cnf(c733,plain,
'earray$u42' = store('earray$u39','elem$u40','elem$u41'),
inference(clausification,[status(esa)],[hyp11]) ).
cnf(c734,plain,
'earray$u45' = store('earray$u42','elem$u43','elem$u44'),
inference(clausification,[status(esa)],[hyp12]) ).
cnf(c741,plain,
'earray$u6' = store('earray$u3','elem$u4','elem$u5'),
inference(clausification,[status(esa)],[hyp19]) ).
cnf(c748,plain,
'earray$u72' = store('earray$u70','elem$u4','elem$u71'),
inference(clausification,[status(esa)],[hyp26]) ).
cnf(c749,plain,
'earray$u74' = store('earray$u72','elem$u0','elem$u73'),
inference(clausification,[status(esa)],[hyp27]) ).
cnf(c750,plain,
'earray$u76' = store('earray$u74',i,'elem$u75'),
inference(clausification,[status(esa)],[hyp28]) ).
cnf(c751,plain,
'earray$u9' = store('earray$u6','elem$u7','elem$u8'),
inference(clausification,[status(esa)],[hyp29]) ).
cnf(c752,plain,
'elem$u0' = s(i),
inference(clausification,[status(esa)],[hyp30]) ).
cnf(c754,plain,
'elem$u10' = s('elem$u7'),
inference(clausification,[status(esa)],[hyp32]) ).
cnf(c755,plain,
'elem$u11' = s('elem$u8'),
inference(clausification,[status(esa)],[hyp33]) ).
cnf(c756,plain,
'elem$u13' = s('elem$u10'),
inference(clausification,[status(esa)],[hyp34]) ).
cnf(c757,plain,
'elem$u14' = s('elem$u11'),
inference(clausification,[status(esa)],[hyp35]) ).
cnf(c758,plain,
'elem$u16' = s('elem$u13'),
inference(clausification,[status(esa)],[hyp36]) ).
cnf(c759,plain,
'elem$u17' = s('elem$u14'),
inference(clausification,[status(esa)],[hyp37]) ).
cnf(c760,plain,
'elem$u19' = s('elem$u16'),
inference(clausification,[status(esa)],[hyp38]) ).
cnf(c762,plain,
'elem$u20' = s('elem$u17'),
inference(clausification,[status(esa)],[hyp40]) ).
cnf(c763,plain,
'elem$u22' = s('elem$u19'),
inference(clausification,[status(esa)],[hyp41]) ).
cnf(c764,plain,
'elem$u23' = s('elem$u20'),
inference(clausification,[status(esa)],[hyp42]) ).
cnf(c765,plain,
'elem$u25' = s('elem$u22'),
inference(clausification,[status(esa)],[hyp43]) ).
cnf(c766,plain,
'elem$u26' = s('elem$u23'),
inference(clausification,[status(esa)],[hyp44]) ).
cnf(c767,plain,
'elem$u28' = s('elem$u25'),
inference(clausification,[status(esa)],[hyp45]) ).
cnf(c768,plain,
'elem$u29' = s('elem$u26'),
inference(clausification,[status(esa)],[hyp46]) ).
cnf(c769,plain,
'elem$u31' = s('elem$u28'),
inference(clausification,[status(esa)],[hyp47]) ).
cnf(c770,plain,
'elem$u32' = s('elem$u29'),
inference(clausification,[status(esa)],[hyp48]) ).
cnf(c771,plain,
'elem$u34' = s('elem$u31'),
inference(clausification,[status(esa)],[hyp49]) ).
cnf(c772,plain,
'elem$u35' = s('elem$u32'),
inference(clausification,[status(esa)],[hyp50]) ).
cnf(c773,plain,
'elem$u37' = s('elem$u34'),
inference(clausification,[status(esa)],[hyp51]) ).
cnf(c774,plain,
'elem$u38' = s('elem$u35'),
inference(clausification,[status(esa)],[hyp52]) ).
cnf(c775,plain,
'elem$u4' = s('elem$u0'),
inference(clausification,[status(esa)],[hyp53]) ).
cnf(c776,plain,
'elem$u40' = s('elem$u37'),
inference(clausification,[status(esa)],[hyp54]) ).
cnf(c777,plain,
'elem$u41' = s('elem$u38'),
inference(clausification,[status(esa)],[hyp55]) ).
cnf(c778,plain,
'elem$u43' = s('elem$u40'),
inference(clausification,[status(esa)],[hyp56]) ).
cnf(c779,plain,
'elem$u44' = s('elem$u41'),
inference(clausification,[status(esa)],[hyp57]) ).
cnf(c781,plain,
s('elem$u47') = 'elem$u46',
inference(clausification,[status(esa)],[hyp59]) ).
cnf(c782,plain,
s('elem$u49') = 'elem$u47',
inference(clausification,[status(esa)],[hyp60]) ).
cnf(c784,plain,
s('elem$u51') = 'elem$u49',
inference(clausification,[status(esa)],[hyp62]) ).
cnf(c785,plain,
s('elem$u53') = 'elem$u51',
inference(clausification,[status(esa)],[hyp63]) ).
cnf(c786,plain,
s('elem$u55') = 'elem$u53',
inference(clausification,[status(esa)],[hyp64]) ).
cnf(c787,plain,
s('elem$u57') = 'elem$u55',
inference(clausification,[status(esa)],[hyp65]) ).
cnf(c788,plain,
s('elem$u59') = 'elem$u57',
inference(clausification,[status(esa)],[hyp66]) ).
cnf(c789,plain,
s('elem$u61') = 'elem$u59',
inference(clausification,[status(esa)],[hyp67]) ).
cnf(c790,plain,
s('elem$u63') = 'elem$u61',
inference(clausification,[status(esa)],[hyp68]) ).
cnf(c791,plain,
s('elem$u65') = 'elem$u63',
inference(clausification,[status(esa)],[hyp69]) ).
cnf(c792,plain,
s('elem$u67') = 'elem$u65',
inference(clausification,[status(esa)],[hyp70]) ).
cnf(c793,plain,
s('elem$u69') = 'elem$u67',
inference(clausification,[status(esa)],[hyp71]) ).
cnf(c794,plain,
'elem$u7' = s('elem$u4'),
inference(clausification,[status(esa)],[hyp72]) ).
cnf(c795,plain,
s('elem$u71') = 'elem$u69',
inference(clausification,[status(esa)],[hyp73]) ).
cnf(c798,plain,
'elem$u8' = s('elem$u5'),
inference(clausification,[status(esa)],[hyp76]) ).
cnf(c799,plain,
'earray$u45' = 'earray$u76',
inference(clausification,[status(esa)],[hyp77]) ).
cnf(c800,plain,
'elem$u44' != 'elem$u46',
inference(clausification,[status(esa)],[goal]) ).
cnf(d0,plain,
s('elem$u0') != i,
inference(superposition,[status(thm)],[c752,c720]) ).
cnf(d1,plain,
'elem$u4' != i,
inference(demodulation,[status(thm)],[d0,c775]) ).
cnf(d2,plain,
( 'elem$u10' = X0
| select('earray$u12',X0) = select('earray$u9',X0) ),
inference(superposition,[status(thm)],[c722,c1]) ).
cnf(d3,plain,
select('earray$u6','elem$u4') = 'elem$u5',
inference(superposition,[status(thm)],[c741,c0]) ).
cnf(d4,plain,
( 'elem$u7' = X0
| select('earray$u9',X0) = select('earray$u6',X0) ),
inference(superposition,[status(thm)],[c751,c1]) ).
cnf(d5,plain,
( 'elem$u7' = 'elem$u4'
| select('earray$u9','elem$u4') = 'elem$u5' ),
inference(superposition,[status(thm)],[d4,d3]) ).
cnf(d6,plain,
'elem$u7' != 'elem$u4',
inference(superposition,[status(thm)],[c794,c721]) ).
cnf(d7,plain,
select('earray$u9','elem$u4') = 'elem$u5',
inference(resolution,[status(thm)],[d6,d5]) ).
cnf(d8,plain,
( 'elem$u10' = 'elem$u4'
| select('earray$u12','elem$u4') = 'elem$u5' ),
inference(superposition,[status(thm)],[d7,d2]) ).
cnf(d9,plain,
s('elem$u7') != 'elem$u4',
inference(superposition,[status(thm)],[c794,c720]) ).
cnf(d10,plain,
'elem$u10' != 'elem$u4',
inference(demodulation,[status(thm)],[d9,c754]) ).
cnf(d11,plain,
select('earray$u12','elem$u4') = 'elem$u5',
inference(resolution,[status(thm)],[d10,d8]) ).
cnf(d12,plain,
( 'elem$u13' = X0
| select('earray$u15',X0) = select('earray$u12',X0) ),
inference(superposition,[status(thm)],[c723,c1]) ).
cnf(d13,plain,
( 'elem$u16' = X0
| select('earray$u18',X0) = select('earray$u15',X0) ),
inference(superposition,[status(thm)],[c724,c1]) ).
cnf(d14,plain,
( 'elem$u19' = X0
| select('earray$u21',X0) = select('earray$u18',X0) ),
inference(superposition,[status(thm)],[c725,c1]) ).
cnf(d15,plain,
( 'elem$u22' = X0
| select('earray$u24',X0) = select('earray$u21',X0) ),
inference(superposition,[status(thm)],[c726,c1]) ).
cnf(d16,plain,
( 'elem$u25' = X0
| select('earray$u27',X0) = select('earray$u24',X0) ),
inference(superposition,[status(thm)],[c727,c1]) ).
cnf(d17,plain,
( 'elem$u28' = X0
| select('earray$u30',X0) = select('earray$u27',X0) ),
inference(superposition,[status(thm)],[c729,c1]) ).
cnf(d18,plain,
( 'elem$u31' = X0
| select('earray$u33',X0) = select('earray$u30',X0) ),
inference(superposition,[status(thm)],[c730,c1]) ).
cnf(d19,plain,
( 'elem$u34' = X0
| select('earray$u36',X0) = select('earray$u33',X0) ),
inference(superposition,[status(thm)],[c731,c1]) ).
cnf(d20,plain,
( 'elem$u37' = X0
| select('earray$u39',X0) = select('earray$u36',X0) ),
inference(superposition,[status(thm)],[c732,c1]) ).
cnf(d21,plain,
( 'elem$u40' = X0
| select('earray$u42',X0) = select('earray$u39',X0) ),
inference(superposition,[status(thm)],[c733,c1]) ).
cnf(d22,plain,
( 'elem$u43' = X0
| select('earray$u45',X0) = select('earray$u42',X0) ),
inference(superposition,[status(thm)],[c734,c1]) ).
cnf(d23,plain,
select('earray$u72','elem$u4') = 'elem$u71',
inference(superposition,[status(thm)],[c748,c0]) ).
cnf(d24,plain,
( 'elem$u0' = X0
| select('earray$u74',X0) = select('earray$u72',X0) ),
inference(superposition,[status(thm)],[c749,c1]) ).
cnf(d25,plain,
'earray$u45' = store('earray$u74',i,'elem$u75'),
inference(demodulation,[status(thm)],[c750,c799]) ).
cnf(d26,plain,
( i = X0
| select('earray$u45',X0) = select('earray$u74',X0) ),
inference(superposition,[status(thm)],[d25,c1]) ).
cnf(d27,plain,
( i = X0
| 'elem$u0' = X0
| select('earray$u45',X0) = select('earray$u72',X0) ),
inference(superposition,[status(thm)],[d26,d24]) ).
cnf(d28,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| select('earray$u45','elem$u4') = 'elem$u71' ),
inference(superposition,[status(thm)],[d27,d23]) ).
cnf(d29,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u43' = 'elem$u4'
| 'elem$u71' = select('earray$u42','elem$u4') ),
inference(superposition,[status(thm)],[d28,d22]) ).
cnf(d30,plain,
s(s(s(s(s(s(s(s(s(s(s(s('elem$u7')))))))))))) != 'elem$u4',
inference(superposition,[status(thm)],[c794,c709]) ).
cnf(d31,plain,
s(s(s(s(s(s(s(s(s(s(s('elem$u10'))))))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d30,c754]) ).
cnf(d32,plain,
s(s(s(s(s(s(s(s(s(s('elem$u13')))))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d31,c756]) ).
cnf(d33,plain,
s(s(s(s(s(s(s(s(s('elem$u16'))))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d32,c758]) ).
cnf(d34,plain,
s(s(s(s(s(s(s(s('elem$u19')))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d33,c760]) ).
cnf(d35,plain,
s(s(s(s(s(s(s('elem$u22'))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d34,c763]) ).
cnf(d36,plain,
s(s(s(s(s(s('elem$u25')))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d35,c765]) ).
cnf(d37,plain,
s(s(s(s(s('elem$u28'))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d36,c767]) ).
cnf(d38,plain,
s(s(s(s('elem$u31')))) != 'elem$u4',
inference(demodulation,[status(thm)],[d37,c769]) ).
cnf(d39,plain,
s(s(s('elem$u34'))) != 'elem$u4',
inference(demodulation,[status(thm)],[d38,c771]) ).
cnf(d40,plain,
s(s('elem$u37')) != 'elem$u4',
inference(demodulation,[status(thm)],[d39,c773]) ).
cnf(d41,plain,
s('elem$u40') != 'elem$u4',
inference(demodulation,[status(thm)],[d40,c776]) ).
cnf(d42,plain,
'elem$u43' != 'elem$u4',
inference(demodulation,[status(thm)],[d41,c778]) ).
cnf(d43,plain,
( i = 'elem$u4'
| 'elem$u71' = select('earray$u42','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d42,d29]) ).
cnf(d44,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u40' = 'elem$u4'
| 'elem$u71' = select('earray$u39','elem$u4') ),
inference(superposition,[status(thm)],[d43,d21]) ).
cnf(d45,plain,
s(s(s(s(s(s(s(s(s(s(s('elem$u7'))))))))))) != 'elem$u4',
inference(superposition,[status(thm)],[c794,c710]) ).
cnf(d46,plain,
s(s(s(s(s(s(s(s(s(s('elem$u10')))))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d45,c754]) ).
cnf(d47,plain,
s(s(s(s(s(s(s(s(s('elem$u13'))))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d46,c756]) ).
cnf(d48,plain,
s(s(s(s(s(s(s(s('elem$u16')))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d47,c758]) ).
cnf(d49,plain,
s(s(s(s(s(s(s('elem$u19'))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d48,c760]) ).
cnf(d50,plain,
s(s(s(s(s(s('elem$u22')))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d49,c763]) ).
cnf(d51,plain,
s(s(s(s(s('elem$u25'))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d50,c765]) ).
cnf(d52,plain,
s(s(s(s('elem$u28')))) != 'elem$u4',
inference(demodulation,[status(thm)],[d51,c767]) ).
cnf(d53,plain,
s(s(s('elem$u31'))) != 'elem$u4',
inference(demodulation,[status(thm)],[d52,c769]) ).
cnf(d54,plain,
s(s('elem$u34')) != 'elem$u4',
inference(demodulation,[status(thm)],[d53,c771]) ).
cnf(d55,plain,
s('elem$u37') != 'elem$u4',
inference(demodulation,[status(thm)],[d54,c773]) ).
cnf(d56,plain,
'elem$u40' != 'elem$u4',
inference(demodulation,[status(thm)],[d55,c776]) ).
cnf(d57,plain,
( i = 'elem$u4'
| 'elem$u71' = select('earray$u39','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d56,d44]) ).
cnf(d58,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u37' = 'elem$u4'
| 'elem$u71' = select('earray$u36','elem$u4') ),
inference(superposition,[status(thm)],[d57,d20]) ).
cnf(d59,plain,
s(s(s(s(s(s(s(s(s(s('elem$u7')))))))))) != 'elem$u4',
inference(superposition,[status(thm)],[c794,c711]) ).
cnf(d60,plain,
s(s(s(s(s(s(s(s(s('elem$u10'))))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d59,c754]) ).
cnf(d61,plain,
s(s(s(s(s(s(s(s('elem$u13')))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d60,c756]) ).
cnf(d62,plain,
s(s(s(s(s(s(s('elem$u16'))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d61,c758]) ).
cnf(d63,plain,
s(s(s(s(s(s('elem$u19')))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d62,c760]) ).
cnf(d64,plain,
s(s(s(s(s('elem$u22'))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d63,c763]) ).
cnf(d65,plain,
s(s(s(s('elem$u25')))) != 'elem$u4',
inference(demodulation,[status(thm)],[d64,c765]) ).
cnf(d66,plain,
s(s(s('elem$u28'))) != 'elem$u4',
inference(demodulation,[status(thm)],[d65,c767]) ).
cnf(d67,plain,
s(s('elem$u31')) != 'elem$u4',
inference(demodulation,[status(thm)],[d66,c769]) ).
cnf(d68,plain,
s('elem$u34') != 'elem$u4',
inference(demodulation,[status(thm)],[d67,c771]) ).
cnf(d69,plain,
'elem$u37' != 'elem$u4',
inference(demodulation,[status(thm)],[d68,c773]) ).
cnf(d70,plain,
( i = 'elem$u4'
| 'elem$u71' = select('earray$u36','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d69,d58]) ).
cnf(d71,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u34' = 'elem$u4'
| 'elem$u71' = select('earray$u33','elem$u4') ),
inference(superposition,[status(thm)],[d70,d19]) ).
cnf(d72,plain,
s(s(s(s(s(s(s(s(s('elem$u7'))))))))) != 'elem$u4',
inference(superposition,[status(thm)],[c794,c712]) ).
cnf(d73,plain,
s(s(s(s(s(s(s(s('elem$u10')))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d72,c754]) ).
cnf(d74,plain,
s(s(s(s(s(s(s('elem$u13'))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d73,c756]) ).
cnf(d75,plain,
s(s(s(s(s(s('elem$u16')))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d74,c758]) ).
cnf(d76,plain,
s(s(s(s(s('elem$u19'))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d75,c760]) ).
cnf(d77,plain,
s(s(s(s('elem$u22')))) != 'elem$u4',
inference(demodulation,[status(thm)],[d76,c763]) ).
cnf(d78,plain,
s(s(s('elem$u25'))) != 'elem$u4',
inference(demodulation,[status(thm)],[d77,c765]) ).
cnf(d79,plain,
s(s('elem$u28')) != 'elem$u4',
inference(demodulation,[status(thm)],[d78,c767]) ).
cnf(d80,plain,
s('elem$u31') != 'elem$u4',
inference(demodulation,[status(thm)],[d79,c769]) ).
cnf(d81,plain,
'elem$u34' != 'elem$u4',
inference(demodulation,[status(thm)],[d80,c771]) ).
cnf(d82,plain,
( i = 'elem$u4'
| 'elem$u71' = select('earray$u33','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d81,d71]) ).
cnf(d83,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u31' = 'elem$u4'
| 'elem$u71' = select('earray$u30','elem$u4') ),
inference(superposition,[status(thm)],[d82,d18]) ).
cnf(d84,plain,
s(s(s(s(s(s(s(s('elem$u7')))))))) != 'elem$u4',
inference(superposition,[status(thm)],[c794,c713]) ).
cnf(d85,plain,
s(s(s(s(s(s(s('elem$u10'))))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d84,c754]) ).
cnf(d86,plain,
s(s(s(s(s(s('elem$u13')))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d85,c756]) ).
cnf(d87,plain,
s(s(s(s(s('elem$u16'))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d86,c758]) ).
cnf(d88,plain,
s(s(s(s('elem$u19')))) != 'elem$u4',
inference(demodulation,[status(thm)],[d87,c760]) ).
cnf(d89,plain,
s(s(s('elem$u22'))) != 'elem$u4',
inference(demodulation,[status(thm)],[d88,c763]) ).
cnf(d90,plain,
s(s('elem$u25')) != 'elem$u4',
inference(demodulation,[status(thm)],[d89,c765]) ).
cnf(d91,plain,
s('elem$u28') != 'elem$u4',
inference(demodulation,[status(thm)],[d90,c767]) ).
cnf(d92,plain,
'elem$u31' != 'elem$u4',
inference(demodulation,[status(thm)],[d91,c769]) ).
cnf(d93,plain,
( i = 'elem$u4'
| 'elem$u71' = select('earray$u30','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d92,d83]) ).
cnf(d94,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u28' = 'elem$u4'
| 'elem$u71' = select('earray$u27','elem$u4') ),
inference(superposition,[status(thm)],[d93,d17]) ).
cnf(d95,plain,
s(s(s(s(s(s(s('elem$u7'))))))) != 'elem$u4',
inference(superposition,[status(thm)],[c794,c714]) ).
cnf(d96,plain,
s(s(s(s(s(s('elem$u10')))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d95,c754]) ).
cnf(d97,plain,
s(s(s(s(s('elem$u13'))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d96,c756]) ).
cnf(d98,plain,
s(s(s(s('elem$u16')))) != 'elem$u4',
inference(demodulation,[status(thm)],[d97,c758]) ).
cnf(d99,plain,
s(s(s('elem$u19'))) != 'elem$u4',
inference(demodulation,[status(thm)],[d98,c760]) ).
cnf(d100,plain,
s(s('elem$u22')) != 'elem$u4',
inference(demodulation,[status(thm)],[d99,c763]) ).
cnf(d101,plain,
s('elem$u25') != 'elem$u4',
inference(demodulation,[status(thm)],[d100,c765]) ).
cnf(d102,plain,
'elem$u28' != 'elem$u4',
inference(demodulation,[status(thm)],[d101,c767]) ).
cnf(d103,plain,
( i = 'elem$u4'
| 'elem$u71' = select('earray$u27','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d102,d94]) ).
cnf(d104,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u25' = 'elem$u4'
| 'elem$u71' = select('earray$u24','elem$u4') ),
inference(superposition,[status(thm)],[d103,d16]) ).
cnf(d105,plain,
s(s(s(s(s(s('elem$u7')))))) != 'elem$u4',
inference(superposition,[status(thm)],[c794,c715]) ).
cnf(d106,plain,
s(s(s(s(s('elem$u10'))))) != 'elem$u4',
inference(demodulation,[status(thm)],[d105,c754]) ).
cnf(d107,plain,
s(s(s(s('elem$u13')))) != 'elem$u4',
inference(demodulation,[status(thm)],[d106,c756]) ).
cnf(d108,plain,
s(s(s('elem$u16'))) != 'elem$u4',
inference(demodulation,[status(thm)],[d107,c758]) ).
cnf(d109,plain,
s(s('elem$u19')) != 'elem$u4',
inference(demodulation,[status(thm)],[d108,c760]) ).
cnf(d110,plain,
s('elem$u22') != 'elem$u4',
inference(demodulation,[status(thm)],[d109,c763]) ).
cnf(d111,plain,
'elem$u25' != 'elem$u4',
inference(demodulation,[status(thm)],[d110,c765]) ).
cnf(d112,plain,
( i = 'elem$u4'
| 'elem$u71' = select('earray$u24','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d111,d104]) ).
cnf(d113,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u22' = 'elem$u4'
| 'elem$u71' = select('earray$u21','elem$u4') ),
inference(superposition,[status(thm)],[d112,d15]) ).
cnf(d114,plain,
s(s(s(s(s('elem$u7'))))) != 'elem$u4',
inference(superposition,[status(thm)],[c794,c716]) ).
cnf(d115,plain,
s(s(s(s('elem$u10')))) != 'elem$u4',
inference(demodulation,[status(thm)],[d114,c754]) ).
cnf(d116,plain,
s(s(s('elem$u13'))) != 'elem$u4',
inference(demodulation,[status(thm)],[d115,c756]) ).
cnf(d117,plain,
s(s('elem$u16')) != 'elem$u4',
inference(demodulation,[status(thm)],[d116,c758]) ).
cnf(d118,plain,
s('elem$u19') != 'elem$u4',
inference(demodulation,[status(thm)],[d117,c760]) ).
cnf(d119,plain,
'elem$u22' != 'elem$u4',
inference(demodulation,[status(thm)],[d118,c763]) ).
cnf(d120,plain,
( i = 'elem$u4'
| 'elem$u71' = select('earray$u21','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d119,d113]) ).
cnf(d121,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u19' = 'elem$u4'
| 'elem$u71' = select('earray$u18','elem$u4') ),
inference(superposition,[status(thm)],[d120,d14]) ).
cnf(d122,plain,
s(s(s(s('elem$u7')))) != 'elem$u4',
inference(superposition,[status(thm)],[c794,c717]) ).
cnf(d123,plain,
s(s(s('elem$u10'))) != 'elem$u4',
inference(demodulation,[status(thm)],[d122,c754]) ).
cnf(d124,plain,
s(s('elem$u13')) != 'elem$u4',
inference(demodulation,[status(thm)],[d123,c756]) ).
cnf(d125,plain,
s('elem$u16') != 'elem$u4',
inference(demodulation,[status(thm)],[d124,c758]) ).
cnf(d126,plain,
'elem$u19' != 'elem$u4',
inference(demodulation,[status(thm)],[d125,c760]) ).
cnf(d127,plain,
( i = 'elem$u4'
| 'elem$u71' = select('earray$u18','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d126,d121]) ).
cnf(d128,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u16' = 'elem$u4'
| 'elem$u71' = select('earray$u15','elem$u4') ),
inference(superposition,[status(thm)],[d127,d13]) ).
cnf(d129,plain,
s(s(s('elem$u7'))) != 'elem$u4',
inference(superposition,[status(thm)],[c794,c718]) ).
cnf(d130,plain,
s(s('elem$u10')) != 'elem$u4',
inference(demodulation,[status(thm)],[d129,c754]) ).
cnf(d131,plain,
s('elem$u13') != 'elem$u4',
inference(demodulation,[status(thm)],[d130,c756]) ).
cnf(d132,plain,
'elem$u16' != 'elem$u4',
inference(demodulation,[status(thm)],[d131,c758]) ).
cnf(d133,plain,
( i = 'elem$u4'
| 'elem$u71' = select('earray$u15','elem$u4')
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d132,d128]) ).
cnf(d134,plain,
( i = 'elem$u4'
| 'elem$u0' = 'elem$u4'
| 'elem$u13' = 'elem$u4'
| 'elem$u71' = select('earray$u12','elem$u4') ),
inference(superposition,[status(thm)],[d133,d12]) ).
cnf(d135,plain,
( i = 'elem$u4'
| 'elem$u71' = 'elem$u5'
| 'elem$u0' = 'elem$u4'
| 'elem$u13' = 'elem$u4' ),
inference(demodulation,[status(thm)],[d134,d11]) ).
cnf(d136,plain,
s(s('elem$u7')) != 'elem$u4',
inference(superposition,[status(thm)],[c794,c719]) ).
cnf(d137,plain,
s('elem$u10') != 'elem$u4',
inference(demodulation,[status(thm)],[d136,c754]) ).
cnf(d138,plain,
'elem$u13' != 'elem$u4',
inference(demodulation,[status(thm)],[d137,c756]) ).
cnf(d139,plain,
( i = 'elem$u4'
| 'elem$u71' = 'elem$u5'
| 'elem$u0' = 'elem$u4' ),
inference(resolution,[status(thm)],[d138,d135]) ).
cnf(d140,plain,
( 'elem$u71' = 'elem$u5'
| 'elem$u0' = 'elem$u4'
| 'elem$u4' != 'elem$u4' ),
inference(superposition,[status(thm)],[d139,d1]) ).
cnf(d141,plain,
( 'elem$u71' = 'elem$u5'
| 'elem$u0' = 'elem$u4' ),
inference(equality_resolution,[status(thm)],[d140]) ).
cnf(d142,plain,
( 'elem$u0' = 'elem$u4'
| s('elem$u5') = 'elem$u69' ),
inference(superposition,[status(thm)],[d141,c795]) ).
cnf(d143,plain,
( 'elem$u0' = 'elem$u4'
| 'elem$u8' = 'elem$u69' ),
inference(demodulation,[status(thm)],[d142,c798]) ).
cnf(d144,plain,
( 'elem$u0' = 'elem$u4'
| 'elem$u11' = s('elem$u69') ),
inference(superposition,[status(thm)],[d143,c755]) ).
cnf(d145,plain,
( 'elem$u0' = 'elem$u4'
| 'elem$u11' = 'elem$u67' ),
inference(demodulation,[status(thm)],[d144,c793]) ).
cnf(d146,plain,
( 'elem$u0' = 'elem$u4'
| s('elem$u11') = 'elem$u65' ),
inference(superposition,[status(thm)],[d145,c792]) ).
cnf(d147,plain,
( 'elem$u0' = 'elem$u4'
| 'elem$u14' = 'elem$u65' ),
inference(demodulation,[status(thm)],[d146,c757]) ).
cnf(d148,plain,
( 'elem$u0' = 'elem$u4'
| s('elem$u14') = 'elem$u63' ),
inference(superposition,[status(thm)],[d147,c791]) ).
cnf(d149,plain,
( 'elem$u0' = 'elem$u4'
| 'elem$u17' = 'elem$u63' ),
inference(demodulation,[status(thm)],[d148,c759]) ).
cnf(d150,plain,
( 'elem$u0' = 'elem$u4'
| s('elem$u17') = 'elem$u61' ),
inference(superposition,[status(thm)],[d149,c790]) ).
cnf(d151,plain,
( 'elem$u0' = 'elem$u4'
| 'elem$u20' = 'elem$u61' ),
inference(demodulation,[status(thm)],[d150,c762]) ).
cnf(d152,plain,
( 'elem$u0' = 'elem$u4'
| s('elem$u20') = 'elem$u59' ),
inference(superposition,[status(thm)],[d151,c789]) ).
cnf(d153,plain,
( 'elem$u0' = 'elem$u4'
| 'elem$u23' = 'elem$u59' ),
inference(demodulation,[status(thm)],[d152,c764]) ).
cnf(d154,plain,
( 'elem$u0' = 'elem$u4'
| s('elem$u23') = 'elem$u57' ),
inference(superposition,[status(thm)],[d153,c788]) ).
cnf(d155,plain,
( 'elem$u0' = 'elem$u4'
| 'elem$u26' = 'elem$u57' ),
inference(demodulation,[status(thm)],[d154,c766]) ).
cnf(d156,plain,
( 'elem$u0' = 'elem$u4'
| s('elem$u26') = 'elem$u55' ),
inference(superposition,[status(thm)],[d155,c787]) ).
cnf(d157,plain,
( 'elem$u0' = 'elem$u4'
| 'elem$u29' = 'elem$u55' ),
inference(demodulation,[status(thm)],[d156,c768]) ).
cnf(d158,plain,
( 'elem$u0' = 'elem$u4'
| s('elem$u29') = 'elem$u53' ),
inference(superposition,[status(thm)],[d157,c786]) ).
cnf(d159,plain,
( 'elem$u0' = 'elem$u4'
| 'elem$u32' = 'elem$u53' ),
inference(demodulation,[status(thm)],[d158,c770]) ).
cnf(d160,plain,
( 'elem$u0' = 'elem$u4'
| s('elem$u32') = 'elem$u51' ),
inference(superposition,[status(thm)],[d159,c785]) ).
cnf(d161,plain,
( 'elem$u0' = 'elem$u4'
| 'elem$u35' = 'elem$u51' ),
inference(demodulation,[status(thm)],[d160,c772]) ).
cnf(d162,plain,
( 'elem$u0' = 'elem$u4'
| s('elem$u35') = 'elem$u49' ),
inference(superposition,[status(thm)],[d161,c784]) ).
cnf(d163,plain,
( 'elem$u0' = 'elem$u4'
| 'elem$u38' = 'elem$u49' ),
inference(demodulation,[status(thm)],[d162,c774]) ).
cnf(d164,plain,
( 'elem$u0' = 'elem$u4'
| s('elem$u38') = 'elem$u47' ),
inference(superposition,[status(thm)],[d163,c782]) ).
cnf(d165,plain,
( 'elem$u0' = 'elem$u4'
| 'elem$u41' = 'elem$u47' ),
inference(demodulation,[status(thm)],[d164,c777]) ).
cnf(d166,plain,
( 'elem$u0' = 'elem$u4'
| s('elem$u41') = 'elem$u46' ),
inference(superposition,[status(thm)],[d165,c781]) ).
cnf(d167,plain,
( 'elem$u0' = 'elem$u4'
| 'elem$u44' = 'elem$u46' ),
inference(demodulation,[status(thm)],[d166,c779]) ).
cnf(d168,plain,
'elem$u0' = 'elem$u4',
inference(resolution,[status(thm)],[c800,d167]) ).
cnf(d169,plain,
'elem$u4' != 'elem$u0',
inference(superposition,[status(thm)],[c775,c721]) ).
cnf(d170,plain,
'elem$u0' != 'elem$u0',
inference(demodulation,[status(thm)],[d169,d168]) ).
cnf(d171,plain,
$false,
inference(equality_resolution,[status(thm)],[d170]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV567-1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n016.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sat Sep 26 14:35:17 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 139.16/62.64 % SZS status Unsatisfiable for theBenchmark.p
% 139.16/62.64 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------