%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : DAT101_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 : n021.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:07 PM UTC 2025
% Result : Theorem 225.18s 201.64s
% Output : CNFRefutation 225.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 5
% Syntax : Number of formulae : 29 ( 7 unt; 0 typ; 0 def)
% Number of atoms : 66 ( 26 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 48 ( 11 ~; 32 |; 3 &)
% ( 1 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number arithmetic : 156 ( 24 atm; 0 fun; 103 num; 29 var)
% Number of types : 3 ( 1 usr; 1 ari)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 6 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 6 usr; 6 con; 0-2 aty)
% Number of variables : 41 ( 39 !; 2 ?; 41 :)
% Comments :
%------------------------------------------------------------------------------
%$ inRange > cons > #nlpp > tail > head > nil > #skF_1 > #skF_2
%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(cons,type,
cons: ( $int * list ) > list ).
tff('#skF_1',type,
'#skF_1': ( $int * list ) > $int ).
tff('#skF_2',type,
'#skF_2': ( $int * list ) > list ).
tff(f_31,axiom,
! [Ka: $int,L: list] : ( head(cons(Ka,L)) = Ka ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l1) ).
tff(f_41,axiom,
! [Ka: $int,L: list] : ( cons(Ka,L) != nil ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l4) ).
tff(f_61,negated_conjecture,
~ ~ ! [Na: $int] :
( $greatereq(Na,4)
=> inRange(Na,cons(1,cons(5,cons(2,nil)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c) ).
tff(f_33,axiom,
! [Ka: $int,L: list] : ( tail(cons(Ka,L)) = L ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l2) ).
tff(f_55,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_85721,plain,
! [K_35095: $int,L_35096: list] : ( head(cons(K_35095,L_35096)) = K_35095 ),
inference(cnfTransformation,[status(thm)],[f_31]) ).
tff(c_85718,plain,
! [K_35090: $int,L_35091: list] : ( cons(K_35090,L_35091) != nil ),
inference(cnfTransformation,[status(thm)],[f_41]) ).
tff(c_23,plain,
! [N_16a: $int] :
( inRange(N_16a,cons(1,cons(5,cons(2,nil))))
| ~ $greatereq(N_16a,4) ),
inference(cnfTransformation,[status(thm)],[f_61]) ).
tff(c_85711,plain,
! [N_35077: $int] :
( inRange(N_35077,cons(1,cons(5,cons(2,nil))))
| $less(N_35077,4) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_23]) ).
tff(c_85720,plain,
! [K_35093: $int,L_35094: list] : ( tail(cons(K_35093,L_35094)) = L_35094 ),
inference(cnfTransformation,[status(thm)],[f_33]) ).
tff(c_85816,plain,
! [N_35113: $int,L_35114: list] :
( ( cons('#skF_1'(N_35113,L_35114),'#skF_2'(N_35113,L_35114)) = L_35114 )
| ( nil = L_35114 )
| ~ inRange(N_35113,L_35114) ),
inference(cnfTransformation,[status(thm)],[f_55]) ).
tff(c_85819,plain,
! [N_35077: $int] :
( ( cons('#skF_1'(N_35077,cons(1,cons(5,cons(2,nil)))),'#skF_2'(N_35077,cons(1,cons(5,cons(2,nil))))) = cons(1,cons(5,cons(2,nil))) )
| ( cons(1,cons(5,cons(2,nil))) = nil )
| $less(N_35077,4) ),
inference(resolution,[status(thm)],[c_85711,c_85816]) ).
tff(c_86352,plain,
! [N_35170: $int] :
( ( cons('#skF_1'(N_35170,cons(1,cons(5,cons(2,nil)))),'#skF_2'(N_35170,cons(1,cons(5,cons(2,nil))))) = cons(1,cons(5,cons(2,nil))) )
| $less(N_35170,4) ),
inference(negUnitSimplification,[status(thm)],[c_85718,c_85819]) ).
tff(c_86365,plain,
! [N_35170: $int] :
( ( tail(cons(1,cons(5,cons(2,nil)))) = '#skF_2'(N_35170,cons(1,cons(5,cons(2,nil)))) )
| $less(N_35170,4) ),
inference(superposition,[status(thm),theory(equality)],[c_86352,c_85720]) ).
tff(c_86434,plain,
! [N_35177: $int] :
( ( '#skF_2'(N_35177,cons(1,cons(5,cons(2,nil)))) = cons(5,cons(2,nil)) )
| $less(N_35177,4) ),
inference(demodulation,[status(thm),theory(equality)],[c_85720,c_86365]) ).
tff(c_85717,plain,
! [N_35088: $int,L_35089: list] :
( inRange(N_35088,'#skF_2'(N_35088,L_35089))
| ( nil = L_35089 )
| ~ inRange(N_35088,L_35089) ),
inference(cnfTransformation,[status(thm)],[f_55]) ).
tff(c_86445,plain,
! [N_35177: $int] :
( inRange(N_35177,cons(5,cons(2,nil)))
| ( cons(1,cons(5,cons(2,nil))) = nil )
| ~ inRange(N_35177,cons(1,cons(5,cons(2,nil))))
| $less(N_35177,4) ),
inference(superposition,[status(thm),theory(equality)],[c_86434,c_85717]) ).
tff(c_86456,plain,
! [N_35178: $int] :
( inRange(N_35178,cons(5,cons(2,nil)))
| ~ inRange(N_35178,cons(1,cons(5,cons(2,nil))))
| $less(N_35178,4) ),
inference(negUnitSimplification,[status(thm)],[c_85718,c_86445]) ).
tff(c_86469,plain,
! [N_35179: $int] :
( inRange(N_35179,cons(5,cons(2,nil)))
| $less(N_35179,4) ),
inference(resolution,[status(thm)],[c_85711,c_86456]) ).
tff(c_85714,plain,
! [N_35082: $int,L_35083: list] :
( ( cons('#skF_1'(N_35082,L_35083),'#skF_2'(N_35082,L_35083)) = L_35083 )
| ( nil = L_35083 )
| ~ inRange(N_35082,L_35083) ),
inference(cnfTransformation,[status(thm)],[f_55]) ).
tff(c_86495,plain,
! [N_35179: $int] :
( ( cons('#skF_1'(N_35179,cons(5,cons(2,nil))),'#skF_2'(N_35179,cons(5,cons(2,nil)))) = cons(5,cons(2,nil)) )
| ( cons(5,cons(2,nil)) = nil )
| $less(N_35179,4) ),
inference(resolution,[status(thm)],[c_86469,c_85714]) ).
tff(c_86640,plain,
! [N_35196: $int] :
( ( cons('#skF_1'(N_35196,cons(5,cons(2,nil))),'#skF_2'(N_35196,cons(5,cons(2,nil)))) = cons(5,cons(2,nil)) )
| $less(N_35196,4) ),
inference(negUnitSimplification,[status(thm)],[c_85718,c_86495]) ).
tff(c_86659,plain,
! [N_35196: $int] :
( ( head(cons(5,cons(2,nil))) = '#skF_1'(N_35196,cons(5,cons(2,nil))) )
| $less(N_35196,4) ),
inference(superposition,[status(thm),theory(equality)],[c_86640,c_85721]) ).
tff(c_86674,plain,
! [N_35197: $int] :
( ( '#skF_1'(N_35197,cons(5,cons(2,nil))) = 5 )
| $less(N_35197,4) ),
inference(demodulation,[status(thm),theory(equality)],[c_85721,c_86659]) ).
tff(c_85716,plain,
! [N_35086: $int,L_35087: list] :
( $less('#skF_1'(N_35086,L_35087),N_35086)
| ( nil = L_35087 )
| ~ inRange(N_35086,L_35087) ),
inference(cnfTransformation,[status(thm)],[f_55]) ).
tff(c_86501,plain,
! [N_35179: $int] :
( $less('#skF_1'(N_35179,cons(5,cons(2,nil))),N_35179)
| ( cons(5,cons(2,nil)) = nil )
| $less(N_35179,4) ),
inference(resolution,[status(thm)],[c_86469,c_85716]) ).
tff(c_86543,plain,
! [N_35179: $int] :
( $less('#skF_1'(N_35179,cons(5,cons(2,nil))),N_35179)
| $less(N_35179,4) ),
inference(negUnitSimplification,[status(thm)],[c_85718,c_86501]) ).
tff(c_86700,plain,
! [N_35197: $int] :
( $less(5,N_35197)
| $less(N_35197,4)
| $less(N_35197,4) ),
inference(superposition,[status(thm),theory(equality)],[c_86674,c_86543]) ).
tff(c_86712,plain,
$false,
inference(quantifierElimination,[status(thm),theory('LIA')],[c_86700]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : DAT101_1 : TPTP v9.0.0. Released v6.1.0.
% 0.03/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 : n021.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:18:28 EDT 2025
% 0.14/0.34 % CPUTime :
% 116.84/101.54 ***********************************************************************
% 116.84/101.55 After 99.9 sec it's time to try something different, got 99.8 sec left
% 116.84/101.55 ***********************************************************************
% 224.38/201.46 ***********************************************************************
% 224.38/201.46 After 199.8 sec it's time to try something different, got 99.6 sec left
% 224.38/201.46 ***********************************************************************
% 225.18/201.64 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 225.18/201.65
% 225.18/201.65 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------