%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWX224+1 : TPTP v9.3.0. Released v9.3.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 : n008.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 : Tue May 5 06:56:39 PM UTC 2026
% Result : Theorem 8.67s 3.21s
% Output : CNFRefutation 8.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 6
% Syntax : Number of formulae : 26 ( 9 unt; 0 typ; 0 def)
% Number of atoms : 54 ( 24 equ)
% Maximal formula atoms : 3 ( 2 avg)
% Number of connectives : 64 ( 36 ~; 23 |; 1 &)
% ( 3 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 6 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 25 ( 25 usr; 6 con; 0-3 aty)
% Number of variables : 79 ( 78 !; 1 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ tc > app > index > cons > arr > #nlpp > var > tail > suc > proj3App > proj2Arr > proj2App > proj1Var > proj1Suc > proj1Lam > proj1Just > proj1Arr > proj1App > lam > just > head > zero > nothing > nil > c > b > a
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(app,type,
app: ( $i * $i * $i ) > $i ).
tff(arr,type,
arr: ( $i * $i ) > $i ).
tff(proj3App,type,
proj3App: $i > $i ).
tff(a,type,
a: $i ).
tff(proj1Suc,type,
proj1Suc: $i > $i ).
tff(proj1Lam,type,
proj1Lam: $i > $i ).
tff(b,type,
b: $i ).
tff(proj2App,type,
proj2App: $i > $i ).
tff(proj1Just,type,
proj1Just: $i > $i ).
tff(proj2Arr,type,
proj2Arr: $i > $i ).
tff(nothing,type,
nothing: $i ).
tff(var,type,
var: $i > $i ).
tff(index,type,
index: ( $i * $i ) > $i ).
tff(just,type,
just: $i > $i ).
tff(proj1Var,type,
proj1Var: $i > $i ).
tff(proj1Arr,type,
proj1Arr: $i > $i ).
tff(lam,type,
lam: $i > $i ).
tff(suc,type,
suc: $i > $i ).
tff(cons,type,
cons: ( $i * $i ) > $i ).
tff(proj1App,type,
proj1App: $i > $i ).
tff(tail,type,
tail: $i > $i ).
tff(tc,type,
tc: ( $i * $i * $i ) > $o ).
tff(head,type,
head: $i > $i ).
tff(nil,type,
nil: $i ).
tff(zero,type,
zero: $i ).
tff(c,type,
c: $i ).
tff(f_83,axiom,
! [Z,Xs] : ( index(cons(Z,Xs),zero) = just(Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_025) ).
tff(f_85,axiom,
! [Z,Xs,N] : ( index(cons(Z,Xs),suc(N)) = index(Xs,N) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_026) ).
tff(f_112,axiom,
! [X,Z,X3,Tx3] :
( ( index(X,X3) = just(Tx3) )
=> ( tc(X,var(X3),Z)
<=> ( Tx3 = Z ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_031) ).
tff(f_91,axiom,
! [X,Z,F,X2,Tx] :
( tc(X,app(F,X2,Tx),Z)
<=> ( tc(X,F,arr(Tx,Z))
& tc(X,X2,Tx) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_027) ).
tff(f_101,axiom,
! [X,E,Tx2,T1] :
( tc(X,lam(E),arr(Tx2,T1))
<=> tc(cons(Tx2,X),E,T1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_029) ).
tff(f_115,negated_conjecture,
~ ? [E] : tc(nil,E,arr(arr(a,arr(a,b)),arr(a,b))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal_032) ).
tff(c_50,plain,
! [Z_43,Xs_44] : ( index(cons(Z_43,Xs_44),zero) = just(Z_43) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_52,plain,
! [Z_45,Xs_46,N_47] : ( index(cons(Z_45,Xs_46),suc(N_47)) = index(Xs_46,N_47) ),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_68,plain,
! [X_63,X3_65,Z_64] :
( tc(X_63,var(X3_65),Z_64)
| ( just(Z_64) != index(X_63,X3_65) ) ),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_54,plain,
! [Tx_52,X_48,Z_49,X2_51,F_50] :
( tc(X_48,app(F_50,X2_51,Tx_52),Z_49)
| ~ tc(X_48,X2_51,Tx_52)
| ~ tc(X_48,F_50,arr(Tx_52,Z_49)) ),
inference(cnfTransformation,[status(thm)],[f_91]) ).
tff(c_310,plain,
! [F_167,X_163,Z_164,Tx_166,X2_165] :
( tc(X_163,app(F_167,X2_165,Tx_166),Z_164)
| ~ tc(X_163,X2_165,Tx_166)
| ~ tc(X_163,F_167,arr(Tx_166,Z_164)) ),
inference(cnfTransformation,[status(thm)],[f_91]) ).
tff(c_64,plain,
! [X_56,E_57,Tx2_58,T1_59] :
( tc(X_56,lam(E_57),arr(Tx2_58,T1_59))
| ~ tc(cons(Tx2_58,X_56),E_57,T1_59) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_259,plain,
! [X_151,E_152,Tx2_153,T1_154] :
( tc(X_151,lam(E_152),arr(Tx2_153,T1_154))
| ~ tc(cons(Tx2_153,X_151),E_152,T1_154) ),
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_72,plain,
! [E_67] : ~ tc(nil,E_67,arr(arr(a,arr(a,b)),arr(a,b))),
inference(cnfTransformation,[status(thm)],[f_115]) ).
tff(c_269,plain,
! [E_155] : ~ tc(cons(arr(a,arr(a,b)),nil),E_155,arr(a,b)),
inference(resolution,[status(thm)],[c_259,c_72]) ).
tff(c_278,plain,
! [E_57] : ~ tc(cons(a,cons(arr(a,arr(a,b)),nil)),E_57,b),
inference(resolution,[status(thm)],[c_64,c_269]) ).
tff(c_561,plain,
! [X2_238,Tx_239,F_240] :
( ~ tc(cons(a,cons(arr(a,arr(a,b)),nil)),X2_238,Tx_239)
| ~ tc(cons(a,cons(arr(a,arr(a,b)),nil)),F_240,arr(Tx_239,b)) ),
inference(resolution,[status(thm)],[c_310,c_278]) ).
tff(c_732,plain,
! [F_289,Z_290,X3_291] :
( ~ tc(cons(a,cons(arr(a,arr(a,b)),nil)),F_289,arr(Z_290,b))
| ( just(Z_290) != index(cons(a,cons(arr(a,arr(a,b)),nil)),X3_291) ) ),
inference(resolution,[status(thm)],[c_68,c_561]) ).
tff(c_2616,plain,
! [F_1237,X3_1236,Tx_1235,Z_1238,X2_1234] :
( ( just(Z_1238) != index(cons(a,cons(arr(a,arr(a,b)),nil)),X3_1236) )
| ~ tc(cons(a,cons(arr(a,arr(a,b)),nil)),X2_1234,Tx_1235)
| ~ tc(cons(a,cons(arr(a,arr(a,b)),nil)),F_1237,arr(Tx_1235,arr(Z_1238,b))) ),
inference(resolution,[status(thm)],[c_54,c_732]) ).
tff(c_2624,plain,
! [Z_1243,X2_1244,Tx_1245,F_1246] :
( ( just(a) != just(Z_1243) )
| ~ tc(cons(a,cons(arr(a,arr(a,b)),nil)),X2_1244,Tx_1245)
| ~ tc(cons(a,cons(arr(a,arr(a,b)),nil)),F_1246,arr(Tx_1245,arr(Z_1243,b))) ),
inference(superposition,[status(thm),theory(equality)],[c_50,c_2616]) ).
tff(c_2891,plain,
! [Z_1386,F_1387,Z_1388,X3_1389] :
( ( just(a) != just(Z_1386) )
| ~ tc(cons(a,cons(arr(a,arr(a,b)),nil)),F_1387,arr(Z_1388,arr(Z_1386,b)))
| ( just(Z_1388) != index(cons(a,cons(arr(a,arr(a,b)),nil)),X3_1389) ) ),
inference(resolution,[status(thm)],[c_68,c_2624]) ).
tff(c_3799,plain,
! [Z_1894,Z_1895,X3_1896,X3_1897] :
( ( just(a) != just(Z_1894) )
| ( just(Z_1895) != index(cons(a,cons(arr(a,arr(a,b)),nil)),X3_1896) )
| ( just(arr(Z_1895,arr(Z_1894,b))) != index(cons(a,cons(arr(a,arr(a,b)),nil)),X3_1897) ) ),
inference(resolution,[status(thm)],[c_68,c_2891]) ).
tff(c_3806,plain,
! [Z_1898,Z_1899,X3_1900] :
( ( just(a) != just(Z_1898) )
| ( just(a) != just(Z_1899) )
| ( just(arr(Z_1899,arr(Z_1898,b))) != index(cons(a,cons(arr(a,arr(a,b)),nil)),X3_1900) ) ),
inference(superposition,[status(thm),theory(equality)],[c_50,c_3799]) ).
tff(c_3829,plain,
! [Z_1911,Z_1912,N_1913] :
( ( just(a) != just(Z_1911) )
| ( just(a) != just(Z_1912) )
| ( just(arr(Z_1912,arr(Z_1911,b))) != index(cons(arr(a,arr(a,b)),nil),N_1913) ) ),
inference(superposition,[status(thm),theory(equality)],[c_52,c_3806]) ).
tff(c_3837,plain,
! [Z_1911,Z_1912] :
( ( just(a) != just(Z_1911) )
| ( just(a) != just(Z_1912) )
| ( just(arr(a,arr(a,b))) != just(arr(Z_1912,arr(Z_1911,b))) ) ),
inference(superposition,[status(thm),theory(equality)],[c_50,c_3829]) ).
tff(c_3843,plain,
$false,
inference(reflexivity,[status(thm),theory(equality)],[c_3837]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX224+1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.12 % 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.16/0.33 % Computer : n008.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Tue May 5 12:40:28 EDT 2026
% 0.16/0.34 % CPUTime :
% 8.67/3.21 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.67/3.22
% 8.67/3.22 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------