%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWW650_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 : n017.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:08 PM UTC 2025
% Result : Theorem 15.43s 4.63s
% Output : CNFRefutation 15.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 9
% Syntax : Number of formulae : 119 ( 49 unt; 0 typ; 0 def)
% Number of atoms : 273 ( 86 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 252 ( 98 ~; 137 |; 9 &)
% ( 2 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 6 ( 1 avg)
% Number arithmetic : 563 ( 166 atm; 123 fun; 237 num; 37 var)
% Number of types : 7 ( 5 usr; 1 ari)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 6 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 34 ( 27 usr; 20 con; 0-4 aty)
% Number of variables : 62 ( 60 !; 2 ?; 62 :)
% Comments :
%------------------------------------------------------------------------------
%$ sort1 > rel1 > match_bool1 > mk_ref > iter1 > dist1 > contents > #nlpp > witness1 > ref > f1 > x01 > tuple03 > tuple0 > true1 > t > real > qtmark > int > false1 > bool > #skF_1 > #skF_2
%Foreground sorts:
tff(tuple02,type,
tuple02: $tType ).
tff(t1,type,
t1: $tType ).
tff(bool1,type,
bool1: $tType ).
tff(ty,type,
ty: $tType ).
tff(uni,type,
uni: $tType ).
%Background operators:
tff(mu1,type,
mu1: $int ).
tff('#skE_2',type,
'#skE_2': $int ).
tff('#skE_1',type,
'#skE_1': $int ).
tff('#skE_5',type,
'#skE_5': $int ).
tff('#skE_4',type,
'#skE_4': $int ).
tff('#skE_3',type,
'#skE_3': $int ).
tff(lambda1,type,
lambda1: $int ).
%Foreground operators:
tff(true1,type,
true1: bool1 ).
tff('#skF_1',type,
'#skF_1': ( t1 * t1 ) > $int ).
tff(int,type,
int: ty ).
tff(false1,type,
false1: bool1 ).
tff(sort1,type,
sort1: ( ty * uni ) > $o ).
tff(contents,type,
contents: ( ty * uni ) > uni ).
tff(witness1,type,
witness1: ty > uni ).
tff(real,type,
real: ty ).
tff(x01,type,
x01: t1 ).
tff(match_bool1,type,
match_bool1: ( ty * bool1 * uni * uni ) > uni ).
tff(f1,type,
f1: t1 > t1 ).
tff('#skF_2',type,
'#skF_2': $int > $int ).
tff(tuple0,type,
tuple0: ty ).
tff(qtmark,type,
qtmark: ty ).
tff(bool,type,
bool: ty ).
tff(iter1,type,
iter1: ( $int * t1 ) > t1 ).
tff(tuple03,type,
tuple03: tuple02 ).
tff(t,type,
t: ty ).
tff(ref,type,
ref: ty > ty ).
tff(dist1,type,
dist1: ( $int * $int ) > $int ).
tff(rel1,type,
rel1: ( t1 * t1 ) > $o ).
tff(mk_ref,type,
mk_ref: ( ty * uni ) > uni ).
tff(f_62,axiom,
! [X: t1] : ( iter1(1,X) = f1(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',iter_1) ).
tff(f_66,axiom,
! [Ka: $int,X: t1] :
( $less(0,Ka)
=> ( iter1(Ka,X) = f1(iter1($difference(Ka,1),X)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',iter_s2) ).
tff(f_1711,axiom,
! [C: $int,B: $int] :
( ( $product(C,B) = C )
<=> ( ( C = 0 )
| ( B = 1 ) ) ),
file('/export/starexec/sandbox/solver/bin/lemmas/mult_lemmas.p',mult_cancel_right1) ).
tff(f_93,axiom,
! [Na: $int] :
( $lesseq(mu1,Na)
=> ! [Ka: $int] :
( $lesseq(0,Ka)
=> ( iter1($sum(Na,$product(lambda1,Ka)),x01) = iter1(Na,x01) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cycle_induction) ).
tff(f_86,axiom,
! [Na: $int] :
( $lesseq(mu1,Na)
=> ( iter1($sum(Na,lambda1),x01) = iter1(Na,x01) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cycle) ).
tff(f_135,axiom,
! [T2: t1,T1: t1] :
( rel1(T2,T1)
<=> ? [Ia: $int] :
( ( T1 = iter1(Ia,x01) )
& ( T2 = iter1($sum(Ia,1),x01) )
& $lesseq(1,Ia)
& $lesseq(Ia,$sum(mu1,lambda1))
& ( $lesseq(mu1,Ia)
=> $less(dist1($sum($product(2,Ia),2),$sum(Ia,1)),dist1($product(2,Ia),Ia)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rel_def) ).
tff(f_68,axiom,
$lesseq(1,lambda1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lambda_range) ).
tff(f_152,negated_conjecture,
~ ? [Ta: $int] :
( $lesseq(1,Ta)
& $lesseq(Ta,$sum(mu1,lambda1))
& ( f1(x01) = iter1(Ta,x01) )
& ( f1(f1(x01)) = iter1($product(2,Ta),x01) )
& ! [Ia: $int] :
( ( $lesseq(1,Ia)
& $less(Ia,Ta) )
=> ( iter1(Ia,x01) != iter1($product(2,Ia),x01) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_tortoise_hare) ).
tff(f_67,axiom,
$lesseq(0,mu1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mu_range) ).
tff(c_148,plain,
! [X_20: t1] : ( iter1(1,X_20) = f1(X_20) ),
inference(cnfTransformation,[status(thm)],[f_62]) ).
tff(c_11869,plain,
! [K_1494a: $int,X_1495: t1] :
( ( f1(iter1($sum($uminus(1),K_1494a),X_1495)) = iter1(K_1494a,X_1495) )
| ~ $less(0,K_1494a) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_11947,plain,
! [K_1494a: $int,X_20: t1] :
( ( iter1(K_1494a,X_20) = f1(f1(X_20)) )
| ( $sum($uminus(1),K_1494a) != 1 )
| ~ $less(0,K_1494a) ),
inference(superposition,[status(thm),theory(equality)],[c_148,c_11869]) ).
tff(c_12033,plain,
! [X_20: t1] :
( ( iter1(2,X_20) = f1(f1(X_20)) )
| ~ $less(0,2) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_11947]) ).
tff(c_12035,plain,
! [X_20: t1] : ( iter1(2,X_20) = f1(f1(X_20)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_12033]) ).
tff(c_157,plain,
! [C_70: $int] : ( $product(C_70,1) = C_70 ),
inference(cnfTransformation,[status(thm)],[f_1711]) ).
tff(c_31,plain,
! [N_26a: $int,K_28a: $int] :
( ( iter1($sum(N_26a,$product(lambda1,K_28a)),x01) = iter1(N_26a,x01) )
| ~ $lesseq(mu1,N_26a)
| ~ $lesseq(0,K_28a) ),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_12552,plain,
! [N_1548a: $int,K_1550a: $int] :
( ( iter1($sum(N_1548a,$product(lambda1,K_1550a)),x01) = iter1(N_1548a,x01) )
| $less(N_1548a,mu1)
| $less(K_1550a,0) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_31]) ).
tff(c_12613,plain,
! [N_1548a: $int] :
( ( iter1($sum(N_1548a,lambda1),x01) = iter1(N_1548a,x01) )
| $less(N_1548a,mu1)
| $less(1,0) ),
inference(superposition,[status(thm),theory(equality)],[c_157,c_12552]) ).
tff(c_12614,plain,
! [N_1548a: $int] :
( ( iter1($sum(lambda1,N_1548a),x01) = iter1(N_1548a,x01) )
| $less(N_1548a,mu1) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_12613]) ).
tff(c_15042,plain,
! [N_1771a: $int] :
( ( iter1($sum(N_1771a,lambda1),x01) = iter1(N_1771a,x01) )
| $less(N_1771a,mu1) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_12614]) ).
tff(c_15684,plain,
( ( iter1($sum(2,lambda1),x01) = f1(f1(x01)) )
| $less(2,mu1) ),
inference(superposition,[status(thm),theory(equality)],[c_12035,c_15042]) ).
tff(c_17125,plain,
$less(2,mu1),
inference(splitLeft,[status(thm)],[c_15684]) ).
tff(c_1135,plain,
! [K_234a: $int,X_235: t1] :
( ( f1(iter1($sum($uminus(1),K_234a),X_235)) = iter1(K_234a,X_235) )
| ~ $less(0,K_234a) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_1213,plain,
! [K_234a: $int,X_20: t1] :
( ( iter1(K_234a,X_20) = f1(f1(X_20)) )
| ( $sum($uminus(1),K_234a) != 1 )
| ~ $less(0,K_234a) ),
inference(superposition,[status(thm),theory(equality)],[c_148,c_1135]) ).
tff(c_1297,plain,
! [X_20: t1] :
( ( iter1(2,X_20) = f1(f1(X_20)) )
| ~ $less(0,2) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_1213]) ).
tff(c_1299,plain,
! [X_20: t1] : ( iter1(2,X_20) = f1(f1(X_20)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_1297]) ).
tff(c_29,plain,
! [N_25a: $int] :
( ( iter1($sum(lambda1,N_25a),x01) = iter1(N_25a,x01) )
| ~ $lesseq(mu1,N_25a) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_639,plain,
! [N_202a: $int] :
( ( iter1($sum(lambda1,N_202a),x01) = iter1(N_202a,x01) )
| $less(N_202a,mu1) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_29]) ).
tff(c_762,plain,
( ( iter1($sum(lambda1,1),x01) = f1(x01) )
| $less(1,mu1) ),
inference(superposition,[status(thm),theory(equality)],[c_148,c_639]) ).
tff(c_765,plain,
( ( iter1($sum(1,lambda1),x01) = f1(x01) )
| $less(1,mu1) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_762]) ).
tff(c_1046,plain,
$less(1,mu1),
inference(splitLeft,[status(thm)],[c_765]) ).
tff(c_64,plain,
! [I_45a: $int] :
( rel1(iter1($sum(1,I_45a),x01),iter1(I_45a,x01))
| ~ $lesseq(1,I_45a)
| ~ $lesseq(I_45a,$sum(mu1,lambda1))
| $lesseq(mu1,I_45a) ),
inference(cnfTransformation,[status(thm)],[f_135]) ).
tff(c_2015,plain,
! [I_304a: $int] :
( rel1(iter1($sum(1,I_304a),x01),iter1(I_304a,x01))
| $less(I_304a,1)
| $less($sum(mu1,lambda1),I_304a)
| ~ $less(I_304a,mu1) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_64]) ).
tff(c_2099,plain,
( rel1(iter1($sum(1,1),x01),f1(x01))
| $less(1,1)
| $less($sum(mu1,lambda1),1)
| ~ $less(1,mu1) ),
inference(superposition,[status(thm),theory(equality)],[c_148,c_2015]) ).
tff(c_2199,plain,
( rel1(iter1($sum(1,1),x01),f1(x01))
| $less(1,1)
| $less($sum(mu1,lambda1),1) ),
inference(demodulation,[status(thm),theory(equality)],[c_1046,c_2099]) ).
tff(c_2200,plain,
( rel1(iter1(2,x01),f1(x01))
| $less($sum(lambda1,mu1),1) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_2199]) ).
tff(c_2202,plain,
( rel1(iter1(2,x01),f1(x01))
| $less($sum(mu1,lambda1),1) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_2200]) ).
tff(c_3023,plain,
( rel1(f1(f1(x01)),f1(x01))
| $less($sum(mu1,lambda1),1) ),
inference(demodulation,[status(thm),theory(equality)],[c_1299,c_2202]) ).
tff(c_3025,plain,
( rel1(f1(f1(x01)),f1(x01))
| $less($sum(lambda1,mu1),1) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_3023]) ).
tff(c_3026,plain,
$less($sum(lambda1,mu1),1),
inference(splitLeft,[status(thm)],[c_3025]) ).
tff(c_3028,plain,
$less($sum(mu1,lambda1),1),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_3026]) ).
tff(c_25,plain,
$lesseq(1,lambda1),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_142,plain,
~ $less(lambda1,1),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_25]) ).
tff(c_3029,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_3028,c_1046,c_142]) ).
tff(c_3030,plain,
rel1(f1(f1(x01)),f1(x01)),
inference(splitRight,[status(thm)],[c_3025]) ).
tff(c_54,plain,
! [T2_41: t1,T1_42: t1] :
( $lesseq(1,'#skF_1'(T2_41,T1_42))
| ~ rel1(T2_41,T1_42) ),
inference(cnfTransformation,[status(thm)],[f_135]) ).
tff(c_117,plain,
! [T2_41: t1,T1_42: t1] :
( ~ $less('#skF_1'(T2_41,T1_42),1)
| ~ rel1(T2_41,T1_42) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_54]) ).
tff(c_3117,plain,
~ $less('#skF_1'(f1(f1(x01)),f1(x01)),1),
inference(resolution,[status(thm)],[c_3030,c_117]) ).
tff(c_3121,plain,
'#skF_1'(f1(f1(x01)),f1(x01)) = '#skE_1',
inference(define,[status(thm),theory(equality)],[c_3117]) ).
tff(c_116,plain,
! [T2_41: t1,T1_42: t1] :
( ( iter1($sum(1,'#skF_1'(T2_41,T1_42)),x01) = T2_41 )
| ~ rel1(T2_41,T1_42) ),
inference(cnfTransformation,[status(thm)],[f_135]) ).
tff(c_3113,plain,
iter1($sum(1,'#skF_1'(f1(f1(x01)),f1(x01))),x01) = f1(f1(x01)),
inference(resolution,[status(thm)],[c_3030,c_116]) ).
tff(c_6299,plain,
iter1($sum(1,'#skE_1'),x01) = f1(f1(x01)),
inference(demodulation,[status(thm),theory(equality)],[c_3121,c_3113]) ).
tff(c_68,plain,
! [T_46a: $int] :
( $less('#skF_2'(T_46a),T_46a)
| ( iter1($product(2,T_46a),x01) != f1(f1(x01)) )
| ( iter1(T_46a,x01) != f1(x01) )
| ~ $lesseq(1,T_46a)
| ~ $lesseq(T_46a,$sum(mu1,lambda1)) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_102,plain,
! [T_46a: $int] :
( $less('#skF_2'(T_46a),T_46a)
| ( iter1($product(2,T_46a),x01) != f1(f1(x01)) )
| ( iter1(T_46a,x01) != f1(x01) )
| $less(T_46a,1)
| $less($sum(mu1,lambda1),T_46a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_68]) ).
tff(c_6595,plain,
! [T_46a: $int] :
( $less('#skF_2'(T_46a),T_46a)
| ( iter1(T_46a,x01) != f1(x01) )
| $less(T_46a,1)
| $less($sum(mu1,lambda1),T_46a)
| ( $product(2,T_46a) != $sum(1,'#skE_1') ) ),
inference(superposition,[status(thm),theory(equality)],[c_6299,c_102]) ).
tff(c_6723,plain,
! [T_772a: $int] :
( $less('#skF_2'(T_772a),T_772a)
| ( iter1(T_772a,x01) != f1(x01) )
| $less(T_772a,1)
| $less($sum(lambda1,mu1),T_772a)
| ( $product(2,T_772a) != $sum(1,'#skE_1') ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_6595]) ).
tff(c_6844,plain,
( $less('#skF_2'(1),1)
| $less(1,1)
| $less($sum(lambda1,mu1),1)
| ( $sum(1,'#skE_1') != $product(2,1) ) ),
inference(superposition,[status(thm),theory(equality)],[c_148,c_6723]) ).
tff(c_6845,plain,
( $less('#skF_2'(1),1)
| $less($sum(mu1,lambda1),1)
| ( '#skE_1' != 1 ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_6844]) ).
tff(c_6847,plain,
( $less('#skF_2'(1),1)
| $less($sum(lambda1,mu1),1)
| ( '#skE_1' != 1 ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_6845]) ).
tff(c_7114,plain,
'#skF_2'(1) = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_6847]) ).
tff(c_1311,plain,
! [X_252: t1] : ( iter1(2,X_252) = f1(f1(X_252)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_1297]) ).
tff(c_70,plain,
! [T_46a: $int] :
( $lesseq(1,'#skF_2'(T_46a))
| ( iter1($product(2,T_46a),x01) != f1(f1(x01)) )
| ( iter1(T_46a,x01) != f1(x01) )
| ~ $lesseq(1,T_46a)
| ~ $lesseq(T_46a,$sum(mu1,lambda1)) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_98,plain,
! [T_46a: $int] :
( ~ $less('#skF_2'(T_46a),1)
| ( iter1($product(2,T_46a),x01) != f1(f1(x01)) )
| ( iter1(T_46a,x01) != f1(x01) )
| $less(T_46a,1)
| $less($sum(mu1,lambda1),T_46a) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_70]) ).
tff(c_1392,plain,
! [T_46a: $int] :
( ~ $less('#skF_2'(T_46a),1)
| ( $product(2,T_46a) != 2 )
| ( iter1(T_46a,x01) != f1(x01) )
| $less(T_46a,1)
| $less($sum(mu1,lambda1),T_46a) ),
inference(superposition,[status(thm),theory(equality)],[c_1311,c_98]) ).
tff(c_1394,plain,
( ~ $less('#skF_2'(1),1)
| ( iter1(1,x01) != f1(x01) )
| $less(1,1)
| $less($sum(lambda1,mu1),1) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_1392]) ).
tff(c_1395,plain,
( ~ $less('#skF_2'(1),1)
| ( iter1(1,x01) != f1(x01) )
| $less($sum(mu1,lambda1),1) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_1394]) ).
tff(c_1397,plain,
( ~ $less('#skF_2'(1),1)
| ( iter1(1,x01) != f1(x01) )
| $less($sum(lambda1,mu1),1) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_1395]) ).
tff(c_11741,plain,
( ~ $less('#skE_2',1)
| $less($sum(lambda1,mu1),1) ),
inference(demodulation,[status(thm),theory(equality)],[c_148,c_7114,c_1397]) ).
tff(c_11743,plain,
( ~ $less('#skE_2',1)
| $less($sum(mu1,lambda1),1) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_11741]) ).
tff(c_11745,plain,
~ $less('#skE_2',1),
inference(splitLeft,[status(thm)],[c_11743]) ).
tff(c_1386,plain,
! [T_46a: $int] :
( $less('#skF_2'(T_46a),T_46a)
| ( $product(2,T_46a) != 2 )
| ( iter1(T_46a,x01) != f1(x01) )
| $less(T_46a,1)
| $less($sum(mu1,lambda1),T_46a) ),
inference(superposition,[status(thm),theory(equality)],[c_1311,c_102]) ).
tff(c_1388,plain,
( $less('#skF_2'(1),1)
| ( iter1(1,x01) != f1(x01) )
| $less(1,1)
| $less($sum(lambda1,mu1),1) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_1386]) ).
tff(c_1389,plain,
( $less('#skF_2'(1),1)
| ( iter1(1,x01) != f1(x01) )
| $less($sum(mu1,lambda1),1) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_1388]) ).
tff(c_1391,plain,
( $less('#skF_2'(1),1)
| ( iter1(1,x01) != f1(x01) )
| $less($sum(lambda1,mu1),1) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_1389]) ).
tff(c_11766,plain,
( $less('#skE_2',1)
| $less($sum(lambda1,mu1),1) ),
inference(demodulation,[status(thm),theory(equality)],[c_148,c_7114,c_1391]) ).
tff(c_11767,plain,
$less($sum(lambda1,mu1),1),
inference(negUnitSimplification,[status(thm)],[c_11745,c_11766]) ).
tff(c_11769,plain,
$less($sum(mu1,lambda1),1),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_11767]) ).
tff(c_51,plain,
! [T2_41: t1,T1_42: t1] :
( $lesseq('#skF_1'(T2_41,T1_42),$sum(mu1,lambda1))
| ~ rel1(T2_41,T1_42) ),
inference(cnfTransformation,[status(thm)],[f_135]) ).
tff(c_121,plain,
! [T2_41: t1,T1_42: t1] :
( ~ $less($sum(mu1,lambda1),'#skF_1'(T2_41,T1_42))
| ~ rel1(T2_41,T1_42) ),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_51]) ).
tff(c_3108,plain,
~ $less($sum(mu1,lambda1),'#skF_1'(f1(f1(x01)),f1(x01))),
inference(resolution,[status(thm)],[c_3030,c_121]) ).
tff(c_3111,plain,
~ $less($sum(lambda1,mu1),'#skF_1'(f1(f1(x01)),f1(x01))),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_3108]) ).
tff(c_4626,plain,
~ $less($sum(lambda1,mu1),'#skE_1'),
inference(demodulation,[status(thm),theory(equality)],[c_3121,c_3111]) ).
tff(c_4628,plain,
~ $less($sum(mu1,lambda1),'#skE_1'),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_4626]) ).
tff(c_3118,plain,
'#skF_1'(f1(f1(x01)),f1(x01)) = '#skE_1',
inference(define,[status(thm),theory(equality)],[c_3117]) ).
tff(c_3122,plain,
~ $less('#skE_1',1),
inference(demodulation,[status(thm),theory(equality)],[c_3118,c_3117]) ).
tff(c_11770,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_11769,c_4628,c_3122]) ).
tff(c_11771,plain,
$less($sum(mu1,lambda1),1),
inference(splitRight,[status(thm)],[c_11743]) ).
tff(c_11774,plain,
$less($sum(lambda1,mu1),1),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_11771]) ).
tff(c_11776,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_11774,c_4628,c_3122]) ).
tff(c_11782,plain,
~ $less(1,mu1),
inference(splitRight,[status(thm)],[c_765]) ).
tff(c_17126,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_17125,c_11782]) ).
tff(c_17193,plain,
iter1($sum(2,lambda1),x01) = f1(f1(x01)),
inference(splitRight,[status(thm)],[c_15684]) ).
tff(c_17499,plain,
! [T_46a: $int] :
( ~ $less('#skF_2'(T_46a),1)
| ( iter1(T_46a,x01) != f1(x01) )
| $less(T_46a,1)
| $less($sum(mu1,lambda1),T_46a)
| ( $product(2,T_46a) != $sum(2,lambda1) ) ),
inference(superposition,[status(thm),theory(equality)],[c_17193,c_98]) ).
tff(c_17573,plain,
! [T_1986a: $int] :
( ~ $less('#skF_2'(T_1986a),1)
| ( iter1(T_1986a,x01) != f1(x01) )
| $less(T_1986a,1)
| $less($sum(lambda1,mu1),T_1986a)
| ( $product(2,T_1986a) != $sum(2,lambda1) ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_17499]) ).
tff(c_17694,plain,
( ~ $less('#skF_2'(1),1)
| $less(1,1)
| $less($sum(lambda1,mu1),1)
| ( $sum(2,lambda1) != $product(2,1) ) ),
inference(superposition,[status(thm),theory(equality)],[c_148,c_17573]) ).
tff(c_17695,plain,
( ~ $less('#skF_2'(1),1)
| $less($sum(mu1,lambda1),1)
| ( lambda1 != 0 ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_17694]) ).
tff(c_17697,plain,
( ~ $less('#skF_2'(1),1)
| $less($sum(lambda1,mu1),1)
| ( lambda1 != 0 ) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_17695]) ).
tff(c_18048,plain,
'#skF_2'(1) = '#skE_2',
inference(define,[status(thm),theory(equality)],[c_17697]) ).
tff(c_12047,plain,
! [X_1512: t1] : ( iter1(2,X_1512) = f1(f1(X_1512)) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_12033]) ).
tff(c_12122,plain,
! [T_46a: $int] :
( $less('#skF_2'(T_46a),T_46a)
| ( $product(2,T_46a) != 2 )
| ( iter1(T_46a,x01) != f1(x01) )
| $less(T_46a,1)
| $less($sum(mu1,lambda1),T_46a) ),
inference(superposition,[status(thm),theory(equality)],[c_12047,c_102]) ).
tff(c_12124,plain,
( $less('#skF_2'(1),1)
| ( iter1(1,x01) != f1(x01) )
| $less(1,1)
| $less($sum(lambda1,mu1),1) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_12122]) ).
tff(c_12125,plain,
( $less('#skF_2'(1),1)
| ( iter1(1,x01) != f1(x01) )
| $less($sum(mu1,lambda1),1) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_12124]) ).
tff(c_12127,plain,
( $less('#skF_2'(1),1)
| ( iter1(1,x01) != f1(x01) )
| $less($sum(lambda1,mu1),1) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_12125]) ).
tff(c_19106,plain,
( $less('#skE_2',1)
| $less($sum(lambda1,mu1),1) ),
inference(demodulation,[status(thm),theory(equality)],[c_148,c_18048,c_12127]) ).
tff(c_19108,plain,
( $less('#skE_2',1)
| $less($sum(mu1,lambda1),1) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_19106]) ).
tff(c_19109,plain,
$less($sum(mu1,lambda1),1),
inference(splitLeft,[status(thm)],[c_19108]) ).
tff(c_19111,plain,
$less($sum(lambda1,mu1),1),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_19109]) ).
tff(c_23,plain,
$lesseq(0,mu1),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_143,plain,
~ $less(mu1,0),
inference(backgroundSimplification,[status(thm),theory('LRFIA')],[c_23]) ).
tff(c_19112,plain,
$false,
inference(close,[status(thm),theory('LIA')],[c_19111,c_142,c_143]) ).
tff(c_19114,plain,
~ $less($sum(mu1,lambda1),1),
inference(splitRight,[status(thm)],[c_19108]) ).
tff(c_19117,plain,
~ $less($sum(lambda1,mu1),1),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_19114]) ).
tff(c_19115,plain,
$less('#skE_2',1),
inference(splitRight,[status(thm)],[c_19108]) ).
tff(c_12128,plain,
! [T_46a: $int] :
( ~ $less('#skF_2'(T_46a),1)
| ( $product(2,T_46a) != 2 )
| ( iter1(T_46a,x01) != f1(x01) )
| $less(T_46a,1)
| $less($sum(mu1,lambda1),T_46a) ),
inference(superposition,[status(thm),theory(equality)],[c_12047,c_98]) ).
tff(c_12130,plain,
( ~ $less('#skF_2'(1),1)
| ( iter1(1,x01) != f1(x01) )
| $less(1,1)
| $less($sum(lambda1,mu1),1) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_12128]) ).
tff(c_12131,plain,
( ~ $less('#skF_2'(1),1)
| ( iter1(1,x01) != f1(x01) )
| $less($sum(mu1,lambda1),1) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_12130]) ).
tff(c_12133,plain,
( ~ $less('#skF_2'(1),1)
| ( iter1(1,x01) != f1(x01) )
| $less($sum(lambda1,mu1),1) ),
inference(backgroundSimplification,[status(thm),theory('LIA')],[c_12131]) ).
tff(c_19174,plain,
$less($sum(lambda1,mu1),1),
inference(demodulation,[status(thm),theory(equality)],[c_148,c_19115,c_18048,c_12133]) ).
tff(c_19175,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_19117,c_19174]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SWW650_2 : TPTP v9.0.0. Released v6.1.0.
% 0.11/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.14/0.34 % Computer : n017.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 : Wed Apr 9 06:20:55 EDT 2025
% 0.14/0.34 % CPUTime :
% 15.43/4.63 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.58/4.64
% 15.58/4.64 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------