%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWW615_2 : TPTP v9.0.0. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 09:53:05 PM UTC 2025
% Result : Theorem 20.89s 6.95s
% Output : CNFRefutation 20.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 6
% Syntax : Number of formulae : 80 ( 53 unt; 0 typ; 0 def)
% Number of atoms : 137 ( 113 equ)
% Maximal formula atoms : 15 ( 1 avg)
% Number of connectives : 77 ( 20 ~; 34 |; 12 &)
% ( 0 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of types : 9 ( 7 usr; 1 ari)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-4 aty)
% Number of functors : 62 ( 62 usr; 27 con; 0-5 aty)
% Number of variables : 73 ( 67 !; 6 ?; 73 :)
% Comments :
%------------------------------------------------------------------------------
%$ list_seg > mem > disjoint > sort > no_repet > set > match_list > match_bool > get > infix_plpl > const > cons > tail > reverse > mk_ref > map > length > head > contents > cons_proj_2 > cons_proj_1 > #nlpp > witness > tb2t2 > tb2t1 > tb2t > t2tb2 > t2tb1 > t2tb > ref > nil > list > tuple02 > tuple01 > true > real > qtmark > null > loc1 > int > false > bool1 > #skF_3 > #skF_5 > #skF_18 > #skF_20 > #skF_21 > #skF_23 > #skF_15 > #skF_24 > #skF_9 > #skF_10 > #skF_16 > #skF_19 > #skF_12 > #skF_4 > #skF_11 > #skF_6 > #skF_14 > #skF_1 > #skF_22 > #skF_7 > #skF_13 > #skF_8 > #skF_17 > #skF_2
%Foreground sorts:
tff(loc,type,
loc: $tType ).
tff(list_loc,type,
list_loc: $tType ).
tff(bool,type,
bool: $tType ).
tff(tuple0,type,
tuple0: $tType ).
tff(map_loc_loc,type,
map_loc_loc: $tType ).
tff(ty,type,
ty: $tType ).
tff(uni,type,
uni: $tType ).
%Background operators:
tff('#skE_2',type,
'#skE_2': $int ).
tff('#skE_1',type,
'#skE_1': $int ).
%Foreground operators:
tff(list,type,
list: ty > ty ).
tff('#skF_3',type,
'#skF_3': ( ty * uni * uni ) > uni ).
tff('#skF_5',type,
'#skF_5': ( loc * map_loc_loc * list_loc * loc ) > map_loc_loc ).
tff('#skF_18',type,
'#skF_18': map_loc_loc ).
tff(tail,type,
tail: ( ty * uni ) > uni ).
tff(t2tb1,type,
t2tb1: map_loc_loc > uni ).
tff(cons_proj_1,type,
cons_proj_1: ( ty * uni ) > uni ).
tff(cons,type,
cons: ( ty * uni * uni ) > uni ).
tff(nil,type,
nil: ty > uni ).
tff('#skF_20',type,
'#skF_20': loc ).
tff(t2tb2,type,
t2tb2: loc > uni ).
tff('#skF_21',type,
'#skF_21': list_loc ).
tff(tuple02,type,
tuple02: tuple0 ).
tff(const,type,
const: ( ty * ty * uni ) > uni ).
tff('#skF_23',type,
'#skF_23': loc ).
tff('#skF_15',type,
'#skF_15': list_loc ).
tff(tuple01,type,
tuple01: ty ).
tff(int,type,
int: ty ).
tff(null,type,
null: loc ).
tff(t2tb,type,
t2tb: list_loc > uni ).
tff(disjoint,type,
disjoint: ( ty * uni * uni ) > $o ).
tff(contents,type,
contents: ( ty * uni ) > uni ).
tff(list_seg,type,
list_seg: ( loc * map_loc_loc * list_loc * loc ) > $o ).
tff(real,type,
real: ty ).
tff('#skF_24',type,
'#skF_24': list_loc ).
tff('#skF_9',type,
'#skF_9': ( loc * map_loc_loc * list_loc * loc ) > list_loc ).
tff(match_bool,type,
match_bool: ( ty * bool * uni * uni ) > uni ).
tff(false,type,
false: bool ).
tff(set,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff('#skF_10',type,
'#skF_10': loc ).
tff(reverse,type,
reverse: ( ty * uni ) > uni ).
tff('#skF_16',type,
'#skF_16': loc ).
tff(length,type,
length: ( ty * uni ) > $int ).
tff('#skF_19',type,
'#skF_19': loc ).
tff('#skF_12',type,
'#skF_12': map_loc_loc ).
tff(tb2t1,type,
tb2t1: uni > map_loc_loc ).
tff('#skF_4',type,
'#skF_4': ( loc * map_loc_loc * list_loc * loc ) > loc ).
tff('#skF_11',type,
'#skF_11': list_loc ).
tff(qtmark,type,
qtmark: ty ).
tff(get,type,
get: ( ty * ty * uni * uni ) > uni ).
tff('#skF_6',type,
'#skF_6': ( loc * map_loc_loc * list_loc * loc ) > loc ).
tff(bool1,type,
bool1: ty ).
tff(no_repet,type,
no_repet: ( ty * uni ) > $o ).
tff('#skF_14',type,
'#skF_14': loc ).
tff(tb2t,type,
tb2t: uni > list_loc ).
tff('#skF_1',type,
'#skF_1': ( ty * uni * uni ) > uni ).
tff(map,type,
map: ( ty * ty ) > ty ).
tff('#skF_22',type,
'#skF_22': list_loc ).
tff(tb2t2,type,
tb2t2: uni > loc ).
tff(match_list,type,
match_list: ( ty * ty * uni * uni * uni ) > uni ).
tff('#skF_7',type,
'#skF_7': ( loc * map_loc_loc * list_loc * loc ) > loc ).
tff(head,type,
head: ( ty * uni ) > uni ).
tff(sort,type,
sort: ( ty * uni ) > $o ).
tff(true,type,
true: bool ).
tff(ref,type,
ref: ty > ty ).
tff(cons_proj_2,type,
cons_proj_2: ( ty * uni ) > uni ).
tff(mem,type,
mem: ( ty * uni * uni ) > $o ).
tff('#skF_13',type,
'#skF_13': list_loc ).
tff('#skF_8',type,
'#skF_8': ( loc * map_loc_loc * list_loc * loc ) > map_loc_loc ).
tff(witness,type,
witness: ty > uni ).
tff('#skF_17',type,
'#skF_17': map_loc_loc ).
tff(infix_plpl,type,
infix_plpl: ( ty * uni * uni ) > uni ).
tff('#skF_2',type,
'#skF_2': ( ty * uni * uni ) > uni ).
tff(loc1,type,
loc1: ty ).
tff(mk_ref,type,
mk_ref: ( ty * uni ) > uni ).
tff(f_71,axiom,
! [A: ty,V: uni,V1: uni] : ( nil(A) != cons(A,V,V1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nil_Cons) ).
tff(f_352,negated_conjecture,
~ ! [L: loc,LM: list_loc,Next: map_loc_loc] :
( list_seg(L,Next,LM,null)
=> ! [RM: list_loc,R: loc,PM: list_loc,P: loc,Next1: map_loc_loc] :
( ( list_seg(P,Next1,PM,null)
& list_seg(R,Next1,RM,null)
& disjoint(loc1,t2tb(PM),t2tb(RM))
& ( tb2t(infix_plpl(loc1,reverse(loc1,t2tb(PM)),t2tb(RM))) = tb2t(reverse(loc1,t2tb(LM))) ) )
=> ( ( P != null )
=> ! [Next2: map_loc_loc] :
( ( Next2 = tb2t1(set(loc1,loc1,t2tb1(Next1),t2tb2(P),t2tb2(R))) )
=> ( list_seg(R,Next2,RM,null)
=> ! [R1: loc] :
( ( R1 = P )
=> ! [P1: loc] :
( ( P1 = tb2t2(get(loc1,loc1,t2tb1(Next1),t2tb2(P))) )
=> ! [RM1: list_loc] :
( ( RM1 = tb2t(cons(loc1,head(loc1,t2tb(PM)),t2tb(RM))) )
=> ! [PM1: list_loc] :
( ( PM1 = tb2t(tail(loc1,t2tb(PM))) )
=> ( ( PM != tb2t(nil(loc1)) )
& ! [X: loc,X1: list_loc] :
( ( PM = tb2t(cons(loc1,t2tb2(X),t2tb(X1))) )
=> ( X1 = PM1 ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_in_place_reverse) ).
tff(f_225,axiom,
! [I: list_loc] : ( tb2t(t2tb(I)) = I ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeL) ).
tff(f_227,axiom,
! [J: uni] : ( t2tb(tb2t(J)) = J ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR) ).
tff(f_277,axiom,
! [Z: loc,Z1: map_loc_loc,Z2: list_loc,Z3: loc] :
( list_seg(Z,Z1,Z2,Z3)
=> ( ? [P: loc,Next: map_loc_loc] :
( ( Z = P )
& ( Z1 = Next )
& ( Z2 = tb2t(nil(loc1)) )
& ( Z3 = P ) )
| ? [P: loc,Q: loc,Next: map_loc_loc,L: list_loc] :
( ( P != null )
& list_seg(tb2t2(get(loc1,loc1,t2tb1(Next),t2tb2(P))),Next,L,Q)
& ( Z = P )
& ( Z1 = Next )
& ( Z2 = tb2t(cons(loc1,t2tb2(P),t2tb(L))) )
& ( Z3 = Q ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',list_seg_inversion) ).
tff(f_95,axiom,
! [A: ty,X: uni,L: uni] : ( tail(A,cons(A,X,L)) = L ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tail_cons) ).
tff(c_28,plain,
! [A_36: ty,V_37: uni,V1_38: uni] : ( cons(A_36,V_37,V1_38) != nil(A_36) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_247,plain,
( ( '#skF_24' != '#skF_22' )
| ( tb2t(nil(loc1)) = '#skF_15' ) ),
inference(cnfTransformation,[status(thm)],[f_352]) ).
tff(c_419,plain,
'#skF_24' != '#skF_22',
inference(splitLeft,[status(thm)],[c_247]) ).
tff(c_139,plain,
! [I_165: list_loc] : ( tb2t(t2tb(I_165)) = I_165 ),
inference(cnfTransformation,[status(thm)],[f_225]) ).
tff(c_223,plain,
tb2t(tail(loc1,t2tb('#skF_15'))) = '#skF_22',
inference(cnfTransformation,[status(thm)],[f_352]) ).
tff(c_141,plain,
! [J_166: uni] : ( t2tb(tb2t(J_166)) = J_166 ),
inference(cnfTransformation,[status(thm)],[f_227]) ).
tff(c_413,plain,
tail(loc1,t2tb('#skF_15')) = t2tb('#skF_22'),
inference(superposition,[status(thm),theory(equality)],[c_223,c_141]) ).
tff(c_249,plain,
( ( tb2t(cons(loc1,t2tb2('#skF_23'),t2tb('#skF_24'))) = '#skF_15' )
| ( tb2t(nil(loc1)) = '#skF_15' ) ),
inference(cnfTransformation,[status(thm)],[f_352]) ).
tff(c_550,plain,
tb2t(nil(loc1)) = '#skF_15',
inference(splitLeft,[status(thm)],[c_249]) ).
tff(c_555,plain,
t2tb('#skF_15') = nil(loc1),
inference(superposition,[status(thm),theory(equality)],[c_550,c_141]) ).
tff(c_229,plain,
'#skF_16' = '#skF_19',
inference(cnfTransformation,[status(thm)],[f_352]) ).
tff(c_235,plain,
null != '#skF_16',
inference(cnfTransformation,[status(thm)],[f_352]) ).
tff(c_293,plain,
null != '#skF_19',
inference(demodulation,[status(thm),theory(equality)],[c_229,c_235]) ).
tff(c_243,plain,
list_seg('#skF_16','#skF_17','#skF_15',null),
inference(cnfTransformation,[status(thm)],[f_352]) ).
tff(c_294,plain,
list_seg('#skF_19','#skF_17','#skF_15',null),
inference(demodulation,[status(thm),theory(equality)],[c_229,c_243]) ).
tff(c_5771,plain,
! [Z_1309: loc,Z1_1310: map_loc_loc,Z2_1311: list_loc,Z3_1312: loc] :
( ( '#skF_4'(Z_1309,Z1_1310,Z2_1311,Z3_1312) = Z_1309 )
| ( '#skF_6'(Z_1309,Z1_1310,Z2_1311,Z3_1312) = Z_1309 )
| ~ list_seg(Z_1309,Z1_1310,Z2_1311,Z3_1312) ),
inference(cnfTransformation,[status(thm)],[f_277]) ).
tff(c_5788,plain,
( ( '#skF_4'('#skF_19','#skF_17','#skF_15',null) = '#skF_19' )
| ( '#skF_6'('#skF_19','#skF_17','#skF_15',null) = '#skF_19' ) ),
inference(resolution,[status(thm)],[c_294,c_5771]) ).
tff(c_5928,plain,
'#skF_6'('#skF_19','#skF_17','#skF_15',null) = '#skF_19',
inference(splitLeft,[status(thm)],[c_5788]) ).
tff(c_10030,plain,
! [Z_1544: loc,Z1_1545: map_loc_loc,Z2_1546: list_loc,Z3_1547: loc] :
( ( '#skF_4'(Z_1544,Z1_1545,Z2_1546,Z3_1547) = Z_1544 )
| ( tb2t(cons(loc1,t2tb2('#skF_6'(Z_1544,Z1_1545,Z2_1546,Z3_1547)),t2tb('#skF_9'(Z_1544,Z1_1545,Z2_1546,Z3_1547)))) = Z2_1546 )
| ~ list_seg(Z_1544,Z1_1545,Z2_1546,Z3_1547) ),
inference(cnfTransformation,[status(thm)],[f_277]) ).
tff(c_10045,plain,
( ( '#skF_4'('#skF_19','#skF_17','#skF_15',null) = '#skF_19' )
| ( tb2t(cons(loc1,t2tb2('#skF_6'('#skF_19','#skF_17','#skF_15',null)),t2tb('#skF_9'('#skF_19','#skF_17','#skF_15',null)))) = '#skF_15' ) ),
inference(resolution,[status(thm)],[c_294,c_10030]) ).
tff(c_10060,plain,
( ( '#skF_4'('#skF_19','#skF_17','#skF_15',null) = '#skF_19' )
| ( tb2t(cons(loc1,t2tb2('#skF_19'),t2tb('#skF_9'('#skF_19','#skF_17','#skF_15',null)))) = '#skF_15' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_5928,c_10045]) ).
tff(c_11628,plain,
tb2t(cons(loc1,t2tb2('#skF_19'),t2tb('#skF_9'('#skF_19','#skF_17','#skF_15',null)))) = '#skF_15',
inference(splitLeft,[status(thm)],[c_10060]) ).
tff(c_11759,plain,
cons(loc1,t2tb2('#skF_19'),t2tb('#skF_9'('#skF_19','#skF_17','#skF_15',null))) = t2tb('#skF_15'),
inference(superposition,[status(thm),theory(equality)],[c_11628,c_141]) ).
tff(c_11762,plain,
cons(loc1,t2tb2('#skF_19'),t2tb('#skF_9'('#skF_19','#skF_17','#skF_15',null))) = nil(loc1),
inference(demodulation,[status(thm),theory(equality)],[c_555,c_11759]) ).
tff(c_11764,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_28,c_11762]) ).
tff(c_11765,plain,
'#skF_4'('#skF_19','#skF_17','#skF_15',null) = '#skF_19',
inference(splitRight,[status(thm)],[c_10060]) ).
tff(c_9790,plain,
! [Z_1538: loc,Z1_1539: map_loc_loc,Z2_1540: list_loc,Z3_1541: loc] :
( ( '#skF_4'(Z_1538,Z1_1539,Z2_1540,Z3_1541) = Z3_1541 )
| ( tb2t(cons(loc1,t2tb2('#skF_6'(Z_1538,Z1_1539,Z2_1540,Z3_1541)),t2tb('#skF_9'(Z_1538,Z1_1539,Z2_1540,Z3_1541)))) = Z2_1540 )
| ~ list_seg(Z_1538,Z1_1539,Z2_1540,Z3_1541) ),
inference(cnfTransformation,[status(thm)],[f_277]) ).
tff(c_9802,plain,
( ( '#skF_4'('#skF_19','#skF_17','#skF_15',null) = null )
| ( tb2t(cons(loc1,t2tb2('#skF_6'('#skF_19','#skF_17','#skF_15',null)),t2tb('#skF_9'('#skF_19','#skF_17','#skF_15',null)))) = '#skF_15' ) ),
inference(resolution,[status(thm)],[c_294,c_9790]) ).
tff(c_9816,plain,
( ( '#skF_4'('#skF_19','#skF_17','#skF_15',null) = null )
| ( tb2t(cons(loc1,t2tb2('#skF_19'),t2tb('#skF_9'('#skF_19','#skF_17','#skF_15',null)))) = '#skF_15' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_5928,c_9802]) ).
tff(c_11855,plain,
( ( null = '#skF_19' )
| ( tb2t(cons(loc1,t2tb2('#skF_19'),t2tb('#skF_9'('#skF_19','#skF_17','#skF_15',null)))) = '#skF_15' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_11765,c_9816]) ).
tff(c_11856,plain,
tb2t(cons(loc1,t2tb2('#skF_19'),t2tb('#skF_9'('#skF_19','#skF_17','#skF_15',null)))) = '#skF_15',
inference(negUnitSimplification,[status(thm)],[c_293,c_11855]) ).
tff(c_11860,plain,
cons(loc1,t2tb2('#skF_19'),t2tb('#skF_9'('#skF_19','#skF_17','#skF_15',null))) = t2tb('#skF_15'),
inference(superposition,[status(thm),theory(equality)],[c_11856,c_141]) ).
tff(c_11863,plain,
cons(loc1,t2tb2('#skF_19'),t2tb('#skF_9'('#skF_19','#skF_17','#skF_15',null))) = nil(loc1),
inference(demodulation,[status(thm),theory(equality)],[c_555,c_11860]) ).
tff(c_11865,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_28,c_11863]) ).
tff(c_11867,plain,
'#skF_6'('#skF_19','#skF_17','#skF_15',null) != '#skF_19',
inference(splitRight,[status(thm)],[c_5788]) ).
tff(c_11866,plain,
'#skF_4'('#skF_19','#skF_17','#skF_15',null) = '#skF_19',
inference(splitRight,[status(thm)],[c_5788]) ).
tff(c_11967,plain,
! [Z_1598: loc,Z1_1599: map_loc_loc,Z2_1600: list_loc,Z3_1601: loc] :
( ( '#skF_4'(Z_1598,Z1_1599,Z2_1600,Z3_1601) = Z3_1601 )
| ( '#skF_6'(Z_1598,Z1_1599,Z2_1600,Z3_1601) = Z_1598 )
| ~ list_seg(Z_1598,Z1_1599,Z2_1600,Z3_1601) ),
inference(cnfTransformation,[status(thm)],[f_277]) ).
tff(c_11973,plain,
( ( '#skF_4'('#skF_19','#skF_17','#skF_15',null) = null )
| ( '#skF_6'('#skF_19','#skF_17','#skF_15',null) = '#skF_19' ) ),
inference(resolution,[status(thm)],[c_294,c_11967]) ).
tff(c_11985,plain,
( ( null = '#skF_19' )
| ( '#skF_6'('#skF_19','#skF_17','#skF_15',null) = '#skF_19' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_11866,c_11973]) ).
tff(c_11987,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_11867,c_293,c_11985]) ).
tff(c_11988,plain,
tb2t(cons(loc1,t2tb2('#skF_23'),t2tb('#skF_24'))) = '#skF_15',
inference(splitRight,[status(thm)],[c_249]) ).
tff(c_12019,plain,
cons(loc1,t2tb2('#skF_23'),t2tb('#skF_24')) = t2tb('#skF_15'),
inference(superposition,[status(thm),theory(equality)],[c_11988,c_141]) ).
tff(c_46,plain,
! [A_58: ty,X_59: uni,L_60: uni] : ( tail(A_58,cons(A_58,X_59,L_60)) = L_60 ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_12081,plain,
tail(loc1,t2tb('#skF_15')) = t2tb('#skF_24'),
inference(superposition,[status(thm),theory(equality)],[c_12019,c_46]) ).
tff(c_12090,plain,
t2tb('#skF_24') = t2tb('#skF_22'),
inference(demodulation,[status(thm),theory(equality)],[c_413,c_12081]) ).
tff(c_12096,plain,
tb2t(t2tb('#skF_22')) = '#skF_24',
inference(superposition,[status(thm),theory(equality)],[c_12090,c_139]) ).
tff(c_12099,plain,
'#skF_24' = '#skF_22',
inference(demodulation,[status(thm),theory(equality)],[c_139,c_12096]) ).
tff(c_12101,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_419,c_12099]) ).
tff(c_12102,plain,
tb2t(nil(loc1)) = '#skF_15',
inference(splitRight,[status(thm)],[c_247]) ).
tff(c_12118,plain,
t2tb('#skF_15') = nil(loc1),
inference(superposition,[status(thm),theory(equality)],[c_12102,c_141]) ).
tff(c_18127,plain,
! [Z_2119: loc,Z1_2120: map_loc_loc,Z2_2121: list_loc,Z3_2122: loc] :
( ( '#skF_4'(Z_2119,Z1_2120,Z2_2121,Z3_2122) = Z_2119 )
| ( '#skF_6'(Z_2119,Z1_2120,Z2_2121,Z3_2122) = Z_2119 )
| ~ list_seg(Z_2119,Z1_2120,Z2_2121,Z3_2122) ),
inference(cnfTransformation,[status(thm)],[f_277]) ).
tff(c_18144,plain,
( ( '#skF_4'('#skF_19','#skF_17','#skF_15',null) = '#skF_19' )
| ( '#skF_6'('#skF_19','#skF_17','#skF_15',null) = '#skF_19' ) ),
inference(resolution,[status(thm)],[c_294,c_18127]) ).
tff(c_18208,plain,
'#skF_6'('#skF_19','#skF_17','#skF_15',null) = '#skF_19',
inference(splitLeft,[status(thm)],[c_18144]) ).
tff(c_21341,plain,
! [Z_2278: loc,Z1_2279: map_loc_loc,Z2_2280: list_loc,Z3_2281: loc] :
( ( '#skF_4'(Z_2278,Z1_2279,Z2_2280,Z3_2281) = Z3_2281 )
| ( tb2t(cons(loc1,t2tb2('#skF_6'(Z_2278,Z1_2279,Z2_2280,Z3_2281)),t2tb('#skF_9'(Z_2278,Z1_2279,Z2_2280,Z3_2281)))) = Z2_2280 )
| ~ list_seg(Z_2278,Z1_2279,Z2_2280,Z3_2281) ),
inference(cnfTransformation,[status(thm)],[f_277]) ).
tff(c_21353,plain,
( ( '#skF_4'('#skF_19','#skF_17','#skF_15',null) = null )
| ( tb2t(cons(loc1,t2tb2('#skF_6'('#skF_19','#skF_17','#skF_15',null)),t2tb('#skF_9'('#skF_19','#skF_17','#skF_15',null)))) = '#skF_15' ) ),
inference(resolution,[status(thm)],[c_294,c_21341]) ).
tff(c_21367,plain,
( ( '#skF_4'('#skF_19','#skF_17','#skF_15',null) = null )
| ( tb2t(cons(loc1,t2tb2('#skF_19'),t2tb('#skF_9'('#skF_19','#skF_17','#skF_15',null)))) = '#skF_15' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_18208,c_21353]) ).
tff(c_21454,plain,
tb2t(cons(loc1,t2tb2('#skF_19'),t2tb('#skF_9'('#skF_19','#skF_17','#skF_15',null)))) = '#skF_15',
inference(splitLeft,[status(thm)],[c_21367]) ).
tff(c_23061,plain,
cons(loc1,t2tb2('#skF_19'),t2tb('#skF_9'('#skF_19','#skF_17','#skF_15',null))) = t2tb('#skF_15'),
inference(superposition,[status(thm),theory(equality)],[c_21454,c_141]) ).
tff(c_23064,plain,
cons(loc1,t2tb2('#skF_19'),t2tb('#skF_9'('#skF_19','#skF_17','#skF_15',null))) = nil(loc1),
inference(demodulation,[status(thm),theory(equality)],[c_12118,c_23061]) ).
tff(c_23066,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_28,c_23064]) ).
tff(c_23067,plain,
'#skF_4'('#skF_19','#skF_17','#skF_15',null) = null,
inference(splitRight,[status(thm)],[c_21367]) ).
tff(c_23140,plain,
! [Z_2336: loc,Z1_2337: map_loc_loc,Z2_2338: list_loc,Z3_2339: loc] :
( ( '#skF_4'(Z_2336,Z1_2337,Z2_2338,Z3_2339) = Z_2336 )
| ( tb2t(cons(loc1,t2tb2('#skF_6'(Z_2336,Z1_2337,Z2_2338,Z3_2339)),t2tb('#skF_9'(Z_2336,Z1_2337,Z2_2338,Z3_2339)))) = Z2_2338 )
| ~ list_seg(Z_2336,Z1_2337,Z2_2338,Z3_2339) ),
inference(cnfTransformation,[status(thm)],[f_277]) ).
tff(c_23152,plain,
( ( '#skF_4'('#skF_19','#skF_17','#skF_15',null) = '#skF_19' )
| ( tb2t(cons(loc1,t2tb2('#skF_6'('#skF_19','#skF_17','#skF_15',null)),t2tb('#skF_9'('#skF_19','#skF_17','#skF_15',null)))) = '#skF_15' ) ),
inference(resolution,[status(thm)],[c_294,c_23140]) ).
tff(c_23166,plain,
( ( null = '#skF_19' )
| ( tb2t(cons(loc1,t2tb2('#skF_19'),t2tb('#skF_9'('#skF_19','#skF_17','#skF_15',null)))) = '#skF_15' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_18208,c_23067,c_23152]) ).
tff(c_23167,plain,
tb2t(cons(loc1,t2tb2('#skF_19'),t2tb('#skF_9'('#skF_19','#skF_17','#skF_15',null)))) = '#skF_15',
inference(negUnitSimplification,[status(thm)],[c_293,c_23166]) ).
tff(c_23242,plain,
cons(loc1,t2tb2('#skF_19'),t2tb('#skF_9'('#skF_19','#skF_17','#skF_15',null))) = t2tb('#skF_15'),
inference(superposition,[status(thm),theory(equality)],[c_23167,c_141]) ).
tff(c_23245,plain,
cons(loc1,t2tb2('#skF_19'),t2tb('#skF_9'('#skF_19','#skF_17','#skF_15',null))) = nil(loc1),
inference(demodulation,[status(thm),theory(equality)],[c_12118,c_23242]) ).
tff(c_23247,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_28,c_23245]) ).
tff(c_23249,plain,
'#skF_6'('#skF_19','#skF_17','#skF_15',null) != '#skF_19',
inference(splitRight,[status(thm)],[c_18144]) ).
tff(c_23248,plain,
'#skF_4'('#skF_19','#skF_17','#skF_15',null) = '#skF_19',
inference(splitRight,[status(thm)],[c_18144]) ).
tff(c_23365,plain,
! [Z_2347: loc,Z1_2348: map_loc_loc,Z2_2349: list_loc,Z3_2350: loc] :
( ( '#skF_4'(Z_2347,Z1_2348,Z2_2349,Z3_2350) = Z3_2350 )
| ( '#skF_6'(Z_2347,Z1_2348,Z2_2349,Z3_2350) = Z_2347 )
| ~ list_seg(Z_2347,Z1_2348,Z2_2349,Z3_2350) ),
inference(cnfTransformation,[status(thm)],[f_277]) ).
tff(c_23371,plain,
( ( '#skF_4'('#skF_19','#skF_17','#skF_15',null) = null )
| ( '#skF_6'('#skF_19','#skF_17','#skF_15',null) = '#skF_19' ) ),
inference(resolution,[status(thm)],[c_294,c_23365]) ).
tff(c_23383,plain,
( ( null = '#skF_19' )
| ( '#skF_6'('#skF_19','#skF_17','#skF_15',null) = '#skF_19' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_23248,c_23371]) ).
tff(c_23385,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_23249,c_293,c_23383]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : SWW615_2 : TPTP v9.0.0. Released v6.1.0.
% 0.08/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.34 % Computer : n003.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Apr 9 06:17:33 EDT 2025
% 0.12/0.34 % CPUTime :
% 20.89/6.95 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.89/6.96
% 20.89/6.96 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------