%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : DAT072_1 : 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 : n029.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 06:08:03 PM UTC 2025
% Result : Theorem 273.28s 204.15s
% Output : CNFRefutation 273.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 2
% Syntax : Number of formulae : 70 ( 27 unt; 0 typ; 0 def)
% Number of atoms : 142 ( 86 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 112 ( 40 ~; 63 |; 7 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number arithmetic : 206 ( 54 atm; 76 fun; 51 num; 25 var)
% Number of types : 3 ( 1 usr; 1 ari)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 8 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 48 ( 43 usr; 32 con; 0-3 aty)
% Number of variables : 37 ( 37 !; 0 ?; 37 :)
% Comments :
%------------------------------------------------------------------------------
%$ inRange > sorted > distinct > write > rev > read > max > #nlpp > init > #skF_11 > #skF_5 > #skF_4 > #skF_8 > #skF_1 > #skF_9 > #skF_6 > #skF_3 > #skF_10 > #skF_7 > #skF_2
%Foreground sorts:
tff(array,type,
array: $tType ).
%Background operators:
tff('#skE_7',type,
'#skE_7': $int ).
tff('#skE_21',type,
'#skE_21': $int ).
tff('#skE_11',type,
'#skE_11': $int ).
tff('#skE_25',type,
'#skE_25': $int ).
tff('#skE_23',type,
'#skE_23': $int ).
tff('#skE_12',type,
'#skE_12': $int ).
tff('#skE_2',type,
'#skE_2': $int ).
tff('#skE_1',type,
'#skE_1': $int ).
tff('#skE_20',type,
'#skE_20': $int ).
tff('#skE_6',type,
'#skE_6': $int ).
tff('#skE_13',type,
'#skE_13': $int ).
tff('#skE_26',type,
'#skE_26': $int ).
tff('#skE_10',type,
'#skE_10': $int ).
tff('#skE_24',type,
'#skE_24': $int ).
tff('#skE_5',type,
'#skE_5': $int ).
tff('#skE_15',type,
'#skE_15': $int ).
tff('#skE_8',type,
'#skE_8': $int ).
tff('#skE_4',type,
'#skE_4': $int ).
tff('#skF_12',type,
'#skF_12': $int ).
tff('#skE_22',type,
'#skE_22': $int ).
tff('#skE_16',type,
'#skE_16': $int ).
tff('#skE_17',type,
'#skE_17': $int ).
tff('#skE_3',type,
'#skE_3': $int ).
tff('#skE_9',type,
'#skE_9': $int ).
tff('#skE_18',type,
'#skE_18': $int ).
tff('#skE_19',type,
'#skE_19': $int ).
tff('#skE_14',type,
'#skE_14': $int ).
%Foreground operators:
tff(sorted,type,
sorted: ( array * $int ) > $o ).
tff('#skF_11',type,
'#skF_11': array ).
tff(rev,type,
rev: ( array * $int ) > array ).
tff('#skF_5',type,
'#skF_5': ( array * $int * $int ) > $int ).
tff(write,type,
write: ( array * $int * $int ) > array ).
tff(init,type,
init: $int > array ).
tff('#skF_4',type,
'#skF_4': ( array * $int ) > $int ).
tff('#skF_8',type,
'#skF_8': ( array * array * $int ) > $int ).
tff('#skF_1',type,
'#skF_1': ( array * array ) > $int ).
tff('#skF_9',type,
'#skF_9': array ).
tff('#skF_6',type,
'#skF_6': ( array * $int ) > $int ).
tff('#skF_3',type,
'#skF_3': ( array * $int ) > $int ).
tff('#skF_10',type,
'#skF_10': array ).
tff(max,type,
max: ( array * $int ) > $int ).
tff(inRange,type,
inRange: ( array * $int * $int ) > $o ).
tff('#skF_7',type,
'#skF_7': ( array * $int ) > $int ).
tff(read,type,
read: ( array * $int ) > $int ).
tff(distinct,type,
distinct: ( array * $int ) > $o ).
tff('#skF_2',type,
'#skF_2': ( array * $int * $int ) > $int ).
tff(f_147,negated_conjecture,
~ ! [A: array,B1: array,B2: array,Na: $int] :
( ( ! [Ia: $int] :
( ( $greatereq(Ia,0)
& $greater(Na,Ia)
& ( read(B1,Ia) = read(A,$difference(Na,$sum(Ia,1))) ) )
| ( ( $greater(0,Ia)
| $greatereq(Ia,Na) )
& ( read(B1,Ia) = read(A,Ia) ) ) )
& ! [Ia: $int] :
( ( $greatereq(Ia,0)
& $greater(Na,Ia)
& ( read(B2,Ia) = read(A,$difference(Na,$sum(Ia,1))) ) )
| ( ( $greater(0,Ia)
| $greatereq(Ia,Na) )
& ( read(B2,Ia) = read(A,Ia) ) ) ) )
=> ( B1 = B2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c) ).
tff(f_40,axiom,
! [A: array,B: array] :
( ! [Ia: $int] : ( read(A,Ia) = read(B,Ia) )
=> ( A = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ext) ).
tff(c_72,plain,
'#skF_11' != '#skF_10',
inference(cnfTransformation,[status(thm)],[f_147]) ).
tff(c_87,plain,
! [I_47a: $int] :
( ( read('#skF_9',I_47a) = read('#skF_10',I_47a) )
| $greater('#skF_12',I_47a) ),
inference(cnfTransformation,[status(thm)],[f_147]) ).
tff(c_640006,plain,
! [I_54931: $int] :
( ( read('#skF_9',I_54931) = read('#skF_10',I_54931) )
| $less(I_54931,'#skF_12') ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_87]) ).
tff(c_76,plain,
! [I_48a: $int] :
( ( read('#skF_11',I_48a) = read('#skF_9',I_48a) )
| $greater('#skF_12',I_48a) ),
inference(cnfTransformation,[status(thm)],[f_147]) ).
tff(c_640010,plain,
! [I_54937: $int] :
( ( read('#skF_11',I_54937) = read('#skF_9',I_54937) )
| $less(I_54937,'#skF_12') ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_76]) ).
tff(c_640271,plain,
! [B_55135: array,A_55136: array] :
( ( B_55135 = A_55136 )
| ( read(B_55135,'#skF_1'(A_55136,B_55135)) != read(A_55136,'#skF_1'(A_55136,B_55135)) ) ),
inference(cnfTransformation,[status(thm)],[f_40]) ).
tff(c_647772,plain,
! [A_57418: array] :
( ( A_57418 = '#skF_11' )
| ( read(A_57418,'#skF_1'(A_57418,'#skF_11')) != read('#skF_9','#skF_1'(A_57418,'#skF_11')) )
| $less('#skF_1'(A_57418,'#skF_11'),'#skF_12') ),
inference(superposition,[status(thm),theory(equality)],[c_640010,c_640271]) ).
tff(c_647892,plain,
! [A_57418: array] :
( ( A_57418 = '#skF_11' )
| ( read(A_57418,'#skF_1'(A_57418,'#skF_11')) != read('#skF_10','#skF_1'(A_57418,'#skF_11')) )
| $less('#skF_1'(A_57418,'#skF_11'),'#skF_12') ),
inference(superposition,[status(thm),theory(equality)],[c_640006,c_647772]) ).
tff(c_648409,plain,
( ( '#skF_11' = '#skF_10' )
| $less('#skF_1'('#skF_10','#skF_11'),'#skF_12') ),
inference(reflexivity,[status(thm),theory(equality)],[c_647892]) ).
tff(c_648414,plain,
$less('#skF_1'('#skF_10','#skF_11'),'#skF_12'),
inference(negUnitSimplification,[status(thm)],[c_72,c_648409]) ).
tff(c_648559,plain,
'#skF_1'('#skF_10','#skF_11') = '#skE_16',
inference(define,[status(thm),theory(equality)],[c_648414]) ).
tff(c_640037,plain,
! [B_55007: array,A_55008: array] :
( ( B_55007 = A_55008 )
| ( read(B_55007,'#skF_1'(A_55008,B_55007)) != read(A_55008,'#skF_1'(A_55008,B_55007)) ) ),
inference(cnfTransformation,[status(thm)],[f_40]) ).
tff(c_648573,plain,
( ( '#skF_11' = '#skF_10' )
| ( read('#skF_11','#skE_16') != read('#skF_10','#skF_1'('#skF_10','#skF_11')) ) ),
inference(superposition,[status(thm),theory(equality)],[c_648559,c_640037]) ).
tff(c_648592,plain,
( ( '#skF_11' = '#skF_10' )
| ( read('#skF_11','#skE_16') != read('#skF_10','#skE_16') ) ),
inference(demodulation,[status(thm),theory(equality)],[c_648559,c_648573]) ).
tff(c_648596,plain,
read('#skF_11','#skE_16') != read('#skF_10','#skE_16'),
inference(negUnitSimplification,[status(thm)],[c_72,c_648592]) ).
tff(c_648602,plain,
read('#skF_10','#skE_16') = '#skE_18',
inference(define,[status(thm),theory(equality)],[c_648596]) ).
tff(c_648601,plain,
read('#skF_11','#skE_16') = '#skE_17',
inference(define,[status(thm),theory(equality)],[c_648596]) ).
tff(c_648600,plain,
read('#skF_11','#skE_16') != read('#skF_10','#skE_16'),
inference(negUnitSimplification,[status(thm)],[c_72,c_648592]) ).
tff(c_648613,plain,
'#skE_18' != '#skE_17',
inference(demodulation,[status(thm),theory(equality)],[c_648602,c_648601,c_648600]) ).
tff(c_78,plain,
! [I_48a: $int] :
( ( read('#skF_11',I_48a) = read('#skF_9',I_48a) )
| $greatereq(I_48a,0) ),
inference(cnfTransformation,[status(thm)],[f_147]) ).
tff(c_640009,plain,
! [I_54936: $int] :
( ( read('#skF_11',I_54936) = read('#skF_9',I_54936) )
| ~ $less(I_54936,0) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_78]) ).
tff(c_640364,plain,
! [A_55136: array] :
( ( A_55136 = '#skF_11' )
| ( read(A_55136,'#skF_1'(A_55136,'#skF_11')) != read('#skF_9','#skF_1'(A_55136,'#skF_11')) )
| ~ $less('#skF_1'(A_55136,'#skF_11'),0) ),
inference(superposition,[status(thm),theory(equality)],[c_640009,c_640271]) ).
tff(c_648569,plain,
( ( '#skF_11' = '#skF_10' )
| ( read('#skF_9','#skE_16') != read('#skF_10','#skF_1'('#skF_10','#skF_11')) )
| ~ $less('#skF_1'('#skF_10','#skF_11'),0) ),
inference(superposition,[status(thm),theory(equality)],[c_648559,c_640364]) ).
tff(c_648585,plain,
( ( '#skF_11' = '#skF_10' )
| ( read('#skF_9','#skE_16') != read('#skF_10','#skE_16') )
| ~ $less('#skE_16',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_648559,c_648559,c_648569]) ).
tff(c_648589,plain,
( ( read('#skF_9','#skE_16') != read('#skF_10','#skE_16') )
| ~ $less('#skE_16',0) ),
inference(negUnitSimplification,[status(thm)],[c_72,c_648585]) ).
tff(c_648830,plain,
read('#skF_10','#skE_16') = '#skE_18',
inference(define,[status(thm),theory(equality)],[c_648589]) ).
tff(c_648829,plain,
read('#skF_9','#skE_16') = '#skE_19',
inference(define,[status(thm),theory(equality)],[c_648589]) ).
tff(c_648828,plain,
( ( read('#skF_9','#skE_16') != read('#skF_10','#skE_16') )
| ~ $less('#skE_16',0) ),
inference(negUnitSimplification,[status(thm)],[c_72,c_648585]) ).
tff(c_648841,plain,
( ( '#skE_19' != '#skE_18' )
| ~ $less('#skE_16',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_648830,c_648829,c_648828]) ).
tff(c_649247,plain,
~ $less('#skE_16',0),
inference(splitLeft,[status(thm)],[c_648841]) ).
tff(c_648556,plain,
'#skF_1'('#skF_10','#skF_11') = '#skE_16',
inference(define,[status(thm),theory(equality)],[c_648414]) ).
tff(c_648555,plain,
$less('#skF_1'('#skF_10','#skF_11'),'#skF_12'),
inference(negUnitSimplification,[status(thm)],[c_72,c_648409]) ).
tff(c_648560,plain,
$less('#skE_16','#skF_12'),
inference(demodulation,[status(thm),theory(equality)],[c_648556,c_648555]) ).
tff(c_648843,plain,
read('#skF_10','#skE_16') = '#skE_18',
inference(define,[status(thm),theory(equality)],[c_648596]) ).
tff(c_91,plain,
! [I_47a: $int] :
( ( read('#skF_9',$sum($uminus(1),$sum($uminus(I_47a),'#skF_12'))) = read('#skF_10',I_47a) )
| $greater(0,I_47a)
| $greatereq(I_47a,'#skF_12') ),
inference(cnfTransformation,[status(thm)],[f_147]) ).
tff(c_96,plain,
! [I_47a: $int] :
( ( read('#skF_9',$sum($uminus(1),$sum('#skF_12',$uminus(I_47a)))) = read('#skF_10',I_47a) )
| $less(I_47a,0)
| ~ $less(I_47a,'#skF_12') ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_91]) ).
tff(c_640004,plain,
! [X_54928: $int,I_54929: $int] :
( ( read('#skF_9',X_54928) = read('#skF_10',I_54929) )
| ( X_54928 != $sum($uminus(1),$sum($uminus(I_54929),'#skF_12')) )
| $less(I_54929,0)
| ~ $less(I_54929,'#skF_12') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_96]) ).
tff(c_649001,plain,
read('#skF_9','#skE_16') = '#skE_19',
inference(define,[status(thm),theory(equality)],[c_648589]) ).
tff(c_85,plain,
! [I_47a: $int] :
( ( read('#skF_9',$sum($uminus(1),$sum($uminus(I_47a),'#skF_12'))) = read('#skF_10',I_47a) )
| ( read('#skF_9',I_47a) = read('#skF_10',I_47a) ) ),
inference(cnfTransformation,[status(thm)],[f_147]) ).
tff(c_103,plain,
! [I_47a: $int] :
( ( read('#skF_9',$sum($uminus(1),$sum('#skF_12',$uminus(I_47a)))) = read('#skF_10',I_47a) )
| ( read('#skF_9',I_47a) = read('#skF_10',I_47a) ) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_85]) ).
tff(c_640007,plain,
! [X_54932: $int,I_54933: $int] :
( ( read('#skF_9',X_54932) = read('#skF_10',I_54933) )
| ( X_54932 != $sum($uminus(1),$sum($uminus(I_54933),'#skF_12')) )
| ( read('#skF_9',I_54933) = read('#skF_10',I_54933) ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_103]) ).
tff(c_649044,plain,
( ( read('#skF_9',$sum($uminus(1),$sum($uminus('#skE_16'),'#skF_12'))) = read('#skF_10','#skE_16') )
| ( read('#skF_10','#skE_16') = '#skE_19' ) ),
inference(superposition,[status(thm),theory(equality)],[c_649001,c_640007]) ).
tff(c_649166,plain,
( ( read('#skF_9',$sum($uminus(1),$sum($uminus('#skE_16'),'#skF_12'))) = '#skE_18' )
| ( '#skE_19' = '#skE_18' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_648843,c_648843,c_649044]) ).
tff(c_654278,plain,
read('#skF_9',$sum($uminus(1),$sum($uminus('#skE_16'),'#skF_12'))) = '#skE_24',
inference(define,[status(thm),theory(equality)],[c_649166]) ).
tff(c_654602,plain,
! [I_54929: $int] :
( ( read('#skF_10',I_54929) = '#skE_24' )
| ( $sum($uminus(1),$sum($uminus(I_54929),'#skF_12')) != $sum($uminus(1),$sum($uminus('#skE_16'),'#skF_12')) )
| $less(I_54929,0)
| ~ $less(I_54929,'#skF_12') ),
inference(superposition,[status(thm),theory(equality)],[c_640004,c_654278]) ).
tff(c_654606,plain,
( ( read('#skF_10','#skE_16') = '#skE_24' )
| $less('#skE_16',0)
| ~ $less('#skE_16','#skF_12') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_654602]) ).
tff(c_659791,plain,
( ( '#skE_24' = '#skE_18' )
| $less('#skE_16',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_648560,c_648843,c_654606]) ).
tff(c_659793,plain,
'#skE_24' = '#skE_18',
inference(negUnitSimplification,[status(thm)],[c_649247,c_659791]) ).
tff(c_653963,plain,
read('#skF_9',$sum($uminus(1),$sum($uminus('#skE_16'),'#skF_12'))) = '#skE_24',
inference(define,[status(thm),theory(equality)],[c_649166]) ).
tff(c_659803,plain,
read('#skF_9',$sum($uminus(1),$sum($uminus('#skE_16'),'#skF_12'))) = '#skE_18',
inference(demodulation,[status(thm),theory(equality)],[c_659793,c_653963]) ).
tff(c_80,plain,
! [I_48a: $int] :
( ( read('#skF_11',I_48a) = read('#skF_9',$sum($uminus(1),$sum($uminus(I_48a),'#skF_12'))) )
| $greater(0,I_48a)
| $greatereq(I_48a,'#skF_12') ),
inference(cnfTransformation,[status(thm)],[f_147]) ).
tff(c_108,plain,
! [I_48a: $int] :
( ( read('#skF_11',I_48a) = read('#skF_9',$sum($uminus(1),$sum('#skF_12',$uminus(I_48a)))) )
| $less(I_48a,0)
| ~ $less(I_48a,'#skF_12') ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_80]) ).
tff(c_640008,plain,
! [X_54935: $int,I_54934: $int] :
( ( read('#skF_9',X_54935) = read('#skF_11',I_54934) )
| ( X_54935 != $sum($uminus(1),$sum($uminus(I_54934),'#skF_12')) )
| $less(I_54934,0)
| ~ $less(I_54934,'#skF_12') ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_108]) ).
tff(c_648616,plain,
read('#skF_11','#skE_16') = '#skE_17',
inference(define,[status(thm),theory(equality)],[c_648596]) ).
tff(c_648694,plain,
( ( read('#skF_9',$sum($uminus(1),$sum($uminus('#skE_16'),'#skF_12'))) = '#skE_17' )
| $less('#skE_16',0)
| ~ $less('#skE_16','#skF_12') ),
inference(superposition,[status(thm),theory(equality)],[c_640008,c_648616]) ).
tff(c_648814,plain,
( ( read('#skF_9',$sum($uminus(1),$sum($uminus('#skE_16'),'#skF_12'))) = '#skE_17' )
| $less('#skE_16',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_648560,c_648694]) ).
tff(c_669435,plain,
( ( '#skE_18' = '#skE_17' )
| $less('#skE_16',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_659803,c_648814]) ).
tff(c_669436,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_649247,c_648613,c_669435]) ).
tff(c_669440,plain,
$less('#skE_16',0),
inference(splitRight,[status(thm)],[c_648841]) ).
tff(c_649000,plain,
read('#skF_9','#skE_16') = '#skE_19',
inference(define,[status(thm),theory(equality)],[c_648589]) ).
tff(c_648817,plain,
( ( read('#skF_9','#skE_16') = '#skE_17' )
| ~ $less('#skE_16',0) ),
inference(superposition,[status(thm),theory(equality)],[c_640009,c_648616]) ).
tff(c_669445,plain,
'#skE_19' = '#skE_17',
inference(demodulation,[status(thm),theory(equality)],[c_669440,c_649000,c_648817]) ).
tff(c_89,plain,
! [I_47a: $int] :
( ( read('#skF_9',I_47a) = read('#skF_10',I_47a) )
| $greatereq(I_47a,0) ),
inference(cnfTransformation,[status(thm)],[f_147]) ).
tff(c_640005,plain,
! [I_54930: $int] :
( ( read('#skF_9',I_54930) = read('#skF_10',I_54930) )
| ~ $less(I_54930,0) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_89]) ).
tff(c_649069,plain,
( ( read('#skF_10','#skE_16') = '#skE_19' )
| ~ $less('#skE_16',0) ),
inference(superposition,[status(thm),theory(equality)],[c_649001,c_640005]) ).
tff(c_649195,plain,
( ( '#skE_19' = '#skE_18' )
| ~ $less('#skE_16',0) ),
inference(demodulation,[status(thm),theory(equality)],[c_648843,c_649069]) ).
tff(c_669457,plain,
'#skE_18' = '#skE_17',
inference(demodulation,[status(thm),theory(equality)],[c_669440,c_669445,c_649195]) ).
tff(c_669458,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_648613,c_669457]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : DAT072_1 : TPTP v9.0.0. Released v6.1.0.
% 0.10/0.12 % 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.33 % Computer : n029.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Mon Apr 7 18:17:04 EDT 2025
% 0.12/0.33 % CPUTime :
% 144.78/101.57 ***********************************************************************
% 144.78/101.57 After 99.8 sec it's time to try something different, got 99.7 sec left
% 144.78/101.57 ***********************************************************************
% 264.37/201.41 ***********************************************************************
% 264.40/201.41 After 199.6 sec it's time to try something different, got 99.6 sec left
% 264.40/201.41 ***********************************************************************
% 273.28/204.15 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 273.50/204.17
% 273.50/204.17 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------