%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : DAT086_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/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/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:05 PM UTC 2025
% Result : Theorem 272.68s 206.42s
% Output : CNFRefutation 272.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 8
% Syntax : Number of formulae : 48 ( 32 unt; 0 typ; 0 def)
% Number of atoms : 92 ( 41 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 53 ( 9 ~; 38 |; 4 &)
% ( 1 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number arithmetic : 154 ( 42 atm; 12 fun; 47 num; 53 var)
% Number of types : 3 ( 1 usr; 1 ari)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 7 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 13 usr; 6 con; 0-2 aty)
% Number of variables : 103 ( 101 !; 2 ?; 103 :)
% Comments :
%------------------------------------------------------------------------------
%$ inRange > in > count > cons > append > #nlpp > tail > length > head > nil > #skF_4 > #skF_1 > #skF_2 > #skF_6 > #skF_3 > #skF_5
%Foreground sorts:
tff(list,type,
list: $tType ).
%Background operators:
%Foreground operators:
tff(inRange,type,
inRange: ( $int * list ) > $o ).
tff(tail,type,
tail: list > list ).
tff(nil,type,
nil: list ).
tff(head,type,
head: list > $int ).
tff(length,type,
length: list > $int ).
tff('#skF_4',type,
'#skF_4': ( $int * list ) > list ).
tff(append,type,
append: ( list * list ) > list ).
tff(count,type,
count: ( $int * list ) > $int ).
tff(cons,type,
cons: ( $int * list ) > list ).
tff(in,type,
in: ( $int * list ) > $o ).
tff('#skF_1',type,
'#skF_1': ( $int * list ) > $int ).
tff('#skF_2',type,
'#skF_2': ( $int * list ) > list ).
tff('#skF_6',type,
'#skF_6': ( $int * list ) > list ).
tff('#skF_3',type,
'#skF_3': ( $int * list ) > $int ).
tff('#skF_5',type,
'#skF_5': ( $int * list ) > $int ).
tff(f_70,axiom,
length(nil) = 0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l) ).
tff(f_87,axiom,
! [L: list] : ( append(nil,L) = L ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l_6) ).
tff(f_89,axiom,
! [Ia: $int,K: list,L: list] : ( append(cons(Ia,K),L) = cons(Ia,append(K,L)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l_7) ).
tff(f_72,axiom,
! [Ha: $int,T: list] : ( length(cons(Ha,T)) = $sum(1,length(T)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l_1) ).
tff(f_41,axiom,
! [Ka: $int,L: list] : ( cons(Ka,L) != nil ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l4) ).
tff(f_31,axiom,
! [Ka: $int,L: list] : ( head(cons(Ka,L)) = Ka ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l1) ).
tff(f_101,negated_conjecture,
~ ~ ! [L: list,Na: $int] :
( ( $greatereq(Na,3)
& $greatereq(length(L),4) )
=> inRange(Na,L) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_9) ).
tff(f_68,axiom,
! [Na: $int,L: list] :
( inRange(Na,L)
<=> ( ( L = nil )
| ? [Ka: $int,T: list] :
( ( L = cons(Ka,T) )
& $lesseq(0,Ka)
& $less(Ka,Na)
& inRange(Na,T) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',inRange) ).
tff(c_65,plain,
length(nil) = 0,
inference(cnfTransformation,[status(thm)],[f_70]) ).
tff(c_363674,plain,
! [L_4580: list] : ( append(nil,L_4580) = L_4580 ),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_363943,plain,
! [I_4659: $int,K_4660: list,L_4661: list] : ( cons(I_4659,append(K_4660,L_4661)) = append(cons(I_4659,K_4660),L_4661) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_363986,plain,
! [I_4659: $int,L_4580: list] : ( cons(I_4659,L_4580) = append(cons(I_4659,nil),L_4580) ),
inference(superposition,[status(thm),theory(equality)],[c_363674,c_363943]) ).
tff(c_363673,plain,
! [I_4577: $int,K_4578: list,L_4579: list] : ( cons(I_4577,append(K_4578,L_4579)) = append(cons(I_4577,K_4578),L_4579) ),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_364079,plain,
! [I_4677: $int,L_4678: list] : ( cons(I_4677,L_4678) = append(cons(I_4677,nil),L_4678) ),
inference(superposition,[status(thm),theory(equality)],[c_363674,c_363943]) ).
tff(c_366568,plain,
! [I_4828: $int,K_4829: list,L_4830: list] : ( append(cons(I_4828,nil),append(K_4829,L_4830)) = append(cons(I_4828,K_4829),L_4830) ),
inference(superposition,[status(thm),theory(equality)],[c_363673,c_364079]) ).
tff(c_366842,plain,
! [I_4659: $int,L_4580: list,L_4830: list] : ( append(append(cons(I_4659,nil),L_4580),L_4830) = append(cons(I_4659,nil),append(L_4580,L_4830)) ),
inference(superposition,[status(thm),theory(equality)],[c_363986,c_366568]) ).
tff(c_363678,plain,
! [H_4587: $int,T_4588: list] : ( length(cons(H_4587,T_4588)) = $sum(1,length(T_4588)) ),
inference(cnfTransformation,[status(thm)],[f_72]) ).
tff(c_364107,plain,
! [I_4577: $int,I_4677: $int,L_4678: list] : ( cons(I_4577,cons(I_4677,L_4678)) = append(cons(I_4577,cons(I_4677,nil)),L_4678) ),
inference(superposition,[status(thm),theory(equality)],[c_364079,c_363673]) ).
tff(c_373188,plain,
! [I_5039: $int,I_5040: $int,L_5041: list] : ( cons(I_5039,cons(I_5040,L_5041)) = append(append(cons(I_5039,nil),cons(I_5040,nil)),L_5041) ),
inference(demodulation,[status(thm),theory(equality)],[c_363986,c_364107]) ).
tff(c_373506,plain,
! [I_5039: $int,I_5040: $int,L_5041: list] : ( length(append(append(cons(I_5039,nil),cons(I_5040,nil)),L_5041)) = $sum(1,length(cons(I_5040,L_5041))) ),
inference(superposition,[status(thm),theory(equality)],[c_373188,c_363678]) ).
tff(c_373737,plain,
! [I_5039: $int,I_5040: $int,L_5041: list] : ( length(append(append(cons(I_5039,nil),cons(I_5040,nil)),L_5041)) = $sum(1,$sum(1,length(L_5041))) ),
inference(demodulation,[status(thm),theory(equality)],[c_363678,c_373506]) ).
tff(c_373739,plain,
! [I_5039: $int,I_5040: $int,L_5041: list] : ( length(append(append(cons(I_5039,nil),cons(I_5040,nil)),L_5041)) = $sum(2,length(L_5041)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_373737]) ).
tff(c_377879,plain,
! [I_5099: $int,I_5100: $int,L_5101: list] : ( length(append(cons(I_5099,nil),append(cons(I_5100,nil),L_5101))) = $sum(2,length(L_5101)) ),
inference(demodulation,[status(thm),theory(equality)],[c_366842,c_373739]) ).
tff(c_377986,plain,
! [I_5099: $int,I_4659: $int,L_4580: list] : ( length(append(cons(I_5099,nil),cons(I_4659,L_4580))) = $sum(2,length(L_4580)) ),
inference(superposition,[status(thm),theory(equality)],[c_363986,c_377879]) ).
tff(c_363691,plain,
! [K_4614: $int,L_4615: list] : ( cons(K_4614,L_4615) != nil ),
inference(cnfTransformation,[status(thm)],[f_41]) ).
tff(c_363984,plain,
! [I_4659: $int,K_4660: list,L_4661: list] : ( append(cons(I_4659,K_4660),L_4661) != nil ),
inference(superposition,[status(thm),theory(equality)],[c_363943,c_363691]) ).
tff(c_363694,plain,
! [K_4619: $int,L_4620: list] : ( head(cons(K_4619,L_4620)) = K_4619 ),
inference(cnfTransformation,[status(thm)],[f_31]) ).
tff(c_363982,plain,
! [I_4659: $int,K_4660: list,L_4661: list] : ( head(append(cons(I_4659,K_4660),L_4661)) = I_4659 ),
inference(superposition,[status(thm),theory(equality)],[c_363943,c_363694]) ).
tff(c_55,plain,
! [N_48a: $int,L_47: list] :
( inRange(N_48a,L_47)
| ~ $greatereq(length(L_47),4)
| ~ $greatereq(N_48a,3) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_363670,plain,
! [N_4571: $int,L_4572: list] :
( inRange(N_4571,L_4572)
| $less(length(L_4572),4)
| $less(N_4571,3) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_55]) ).
tff(c_364387,plain,
! [N_4710: $int,L_4711: list] :
( ( cons('#skF_5'(N_4710,L_4711),'#skF_6'(N_4710,L_4711)) = L_4711 )
| ( nil = L_4711 )
| ~ inRange(N_4710,L_4711) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_364423,plain,
! [N_4715: $int,L_4716: list] :
( ( cons('#skF_5'(N_4715,L_4716),'#skF_6'(N_4715,L_4716)) = L_4716 )
| ( nil = L_4716 )
| $less(length(L_4716),4)
| $less(N_4715,3) ),
inference(resolution,[status(thm)],[c_363670,c_364387]) ).
tff(c_365211,plain,
! [L_4765: list,N_4766: $int] :
( ( head(L_4765) = '#skF_5'(N_4766,L_4765) )
| ( nil = L_4765 )
| $less(length(L_4765),4)
| $less(N_4766,3) ),
inference(superposition,[status(thm),theory(equality)],[c_364423,c_363694]) ).
tff(c_363987,plain,
! [N_4662: $int,L_4663: list] :
( $less('#skF_5'(N_4662,L_4663),N_4662)
| ( nil = L_4663 )
| ~ inRange(N_4662,L_4663) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_364000,plain,
! [N_4571: $int,L_4572: list] :
( $less('#skF_5'(N_4571,L_4572),N_4571)
| ( nil = L_4572 )
| $less(length(L_4572),4)
| $less(N_4571,3) ),
inference(resolution,[status(thm)],[c_363670,c_363987]) ).
tff(c_365313,plain,
! [L_4765: list,N_4766: $int] :
( $less(head(L_4765),N_4766)
| ( nil = L_4765 )
| $less(length(L_4765),4)
| $less(N_4766,3)
| ( nil = L_4765 )
| $less(length(L_4765),4)
| $less(N_4766,3) ),
inference(superposition,[status(thm),theory(equality)],[c_365211,c_364000]) ).
tff(c_397581,plain,
! [L_5387: list,N_5388: $int] :
( $less(head(L_5387),N_5388)
| ( nil = L_5387 )
| $less(length(L_5387),4)
| $less(N_5388,3) ),
inference(factorization,[status(thm),theory(equality)],[c_365313]) ).
tff(c_397599,plain,
! [I_5099: $int,I_4659: $int,L_4580: list,N_5388: $int] :
( $less(head(append(cons(I_5099,nil),cons(I_4659,L_4580))),N_5388)
| ( append(cons(I_5099,nil),cons(I_4659,L_4580)) = nil )
| $less($sum(2,length(L_4580)),4)
| $less(N_5388,3) ),
inference(superposition,[status(thm),theory(equality)],[c_377986,c_397581]) ).
tff(c_397671,plain,
! [I_5099: $int,N_5388: $int,I_4659: $int,L_4580: list] :
( $less(I_5099,N_5388)
| ( append(cons(I_5099,nil),cons(I_4659,L_4580)) = nil )
| $less($sum(2,length(L_4580)),4)
| $less(N_5388,3) ),
inference(demodulation,[status(thm),theory(equality)],[c_363982,c_397599]) ).
tff(c_397672,plain,
! [I_5099: $int,N_5388: $int,L_4580: list] :
( $less(I_5099,N_5388)
| $less($sum(2,length(L_4580)),4)
| $less(N_5388,3) ),
inference(negUnitSimplification,[status(thm)],[c_363984,c_397671]) ).
tff(c_397674,plain,
! [I_5099: $int,N_5388: $int,L_4580: list] :
( $less(I_5099,N_5388)
| $less(length(L_4580),2)
| $less(N_5388,3) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_397672]) ).
tff(c_397723,plain,
! [I_5099: $int,N_5388: $int] :
( $less(I_5099,N_5388)
| $less(N_5388,3) ),
inference(splitLeft,[status(thm)],[c_397674]) ).
tff(c_397725,plain,
$false,
inference(quantifierElimination,[status(thm),theory('LIA')],[c_397723]) ).
tff(c_397728,plain,
! [L_5389: list] : $less(length(L_5389),2),
inference(splitRight,[status(thm)],[c_397674]) ).
tff(c_397736,plain,
! [L_4580: list] : $less($sum(2,length(L_4580)),2),
inference(superposition,[status(thm),theory(equality)],[c_377986,c_397728]) ).
tff(c_397777,plain,
! [L_5390: list] : $less(length(L_5390),0),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_397736]) ).
tff(c_397801,plain,
$less(0,0),
inference(superposition,[status(thm),theory(equality)],[c_65,c_397777]) ).
tff(c_397826,plain,
$false,
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_397801]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.12 % Problem : DAT086_1 : TPTP v9.0.0. Released v6.1.0.
% 0.02/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.14/0.34 % Computer : n029.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Mon Apr 7 18:17:34 EDT 2025
% 0.14/0.34 % CPUTime :
% 142.09/101.59 ***********************************************************************
% 142.16/101.60 After 99.9 sec it's time to try something different, got 99.7 sec left
% 142.16/101.60 ***********************************************************************
% 263.93/202.11 ***********************************************************************
% 263.93/202.11 After 200.4 sec it's time to try something different, got 99.0 sec left
% 263.93/202.11 ***********************************************************************
% 272.68/206.42 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 272.68/206.43
% 272.68/206.43 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------