%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWX222-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/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 : n005.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:38 PM UTC 2026
% Result : Unsatisfiable 5.78s 2.38s
% Output : CNFRefutation 6.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 12
% Syntax : Number of formulae : 34 ( 34 unt; 0 typ; 0 def)
% Number of atoms : 34 ( 33 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 26 ( 26 usr; 8 con; 0-4 aty)
% Number of variables : 50 ( 50 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ aux > tc > app > index > eq4 > eq3 > eq2 > eq > cons > arr > andb > #nlpp > var > suc > sat_synth_nf_k > notb > nf > lam > just > zero > nothing > nil > c > btrue > bfalse > b > a
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(eq,type,
eq: ( $i * $i ) > $i ).
tff(app,type,
app: ( $i * $i * $i ) > $i ).
tff(eq3,type,
eq3: ( $i * $i ) > $i ).
tff(arr,type,
arr: ( $i * $i ) > $i ).
tff(a,type,
a: $i ).
tff(tc,type,
tc: ( $i * $i * $i ) > $i ).
tff(b,type,
b: $i ).
tff(aux,type,
aux: ( $i * $i * $i * $i ) > $i ).
tff(notb,type,
notb: $i > $i ).
tff(eq4,type,
eq4: ( $i * $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(lam,type,
lam: $i > $i ).
tff(suc,type,
suc: $i > $i ).
tff(cons,type,
cons: ( $i * $i ) > $i ).
tff(bfalse,type,
bfalse: $i ).
tff(eq2,type,
eq2: ( $i * $i ) > $i ).
tff(andb,type,
andb: ( $i * $i ) > $i ).
tff(nf,type,
nf: $i > $i ).
tff(nil,type,
nil: $i ).
tff(btrue,type,
btrue: $i ).
tff(sat_synth_nf_k,type,
sat_synth_nf_k: $i > $i ).
tff(zero,type,
zero: $i ).
tff(c,type,
c: $i ).
tff(f_142,axiom,
! [X] : ( eq4(X,X) = btrue ),
file(unknown,unknown) ).
tff(f_26,axiom,
notb(btrue) = bfalse,
file(unknown,unknown) ).
tff(f_35,axiom,
! [Q] : ( andb(btrue,Q) = Q ),
file(unknown,unknown) ).
tff(f_47,axiom,
! [X4] : ( nf(var(X4)) = btrue ),
file(unknown,unknown) ).
tff(f_136,axiom,
! [X] : ( eq(X,X) = btrue ),
file(unknown,unknown) ).
tff(f_25,axiom,
! [X,Z,X3,Tx3] : ( aux(X,Z,X3,just(Tx3)) = eq(Tx3,Z) ),
file(unknown,unknown) ).
tff(f_31,axiom,
! [Z,Xs] : ( index(cons(Z,Xs),zero) = just(Z) ),
file(unknown,unknown) ).
tff(f_59,axiom,
! [X,X3,Z] : ( tc(X,var(X3),Z) = aux(X,Z,X3,index(X,X3)) ),
file(unknown,unknown) ).
tff(f_51,axiom,
! [X,E,Tx2,T1] : ( tc(X,lam(E),arr(Tx2,T1)) = tc(cons(Tx2,X),E,T1) ),
file(unknown,unknown) ).
tff(f_45,axiom,
! [E] : ( nf(lam(E)) = nf(E) ),
file(unknown,unknown) ).
tff(f_61,axiom,
! [X] : ( sat_synth_nf_k(X) = notb(andb(nf(X),tc(nil,X,arr(a,arr(b,b))))) ),
file(unknown,unknown) ).
tff(f_145,axiom,
! [X] : ( eq4(sat_synth_nf_k(X),bfalse) != btrue ),
file(unknown,unknown) ).
tff(c_110,plain,
! [X_117] : ( eq4(X_117,X_117) = btrue ),
inference(cnfTransformation,[status(thm)],[f_142]) ).
tff(c_6,plain,
notb(btrue) = bfalse,
inference(cnfTransformation,[status(thm)],[f_26]) ).
tff(c_16,plain,
! [Q_14] : ( andb(btrue,Q_14) = Q_14 ),
inference(cnfTransformation,[status(thm)],[f_35]) ).
tff(c_28,plain,
! [X4_28] : ( nf(var(X4_28)) = btrue ),
inference(cnfTransformation,[status(thm)],[f_47]) ).
tff(c_104,plain,
! [X_114] : ( eq(X_114,X_114) = btrue ),
inference(cnfTransformation,[status(thm)],[f_136]) ).
tff(c_4,plain,
! [X_4,Z_5,X3_6,Tx3_7] : ( aux(X_4,Z_5,X3_6,just(Tx3_7)) = eq(Tx3_7,Z_5) ),
inference(cnfTransformation,[status(thm)],[f_25]) ).
tff(c_12,plain,
! [Z_9,Xs_10] : ( index(cons(Z_9,Xs_10),zero) = just(Z_9) ),
inference(cnfTransformation,[status(thm)],[f_31]) ).
tff(c_449,plain,
! [X_193,Z_194,X3_195] : ( aux(X_193,Z_194,X3_195,index(X_193,X3_195)) = tc(X_193,var(X3_195),Z_194) ),
inference(cnfTransformation,[status(thm)],[f_59]) ).
tff(c_461,plain,
! [Z_9,Xs_10,Z_194] : ( aux(cons(Z_9,Xs_10),Z_194,zero,just(Z_9)) = tc(cons(Z_9,Xs_10),var(zero),Z_194) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_449]) ).
tff(c_467,plain,
! [Z_9,Xs_10,Z_194] : ( tc(cons(Z_9,Xs_10),var(zero),Z_194) = eq(Z_9,Z_194) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_461]) ).
tff(c_32,plain,
! [X_34,E_35,Tx2_36,T1_37] : ( tc(X_34,lam(E_35),arr(Tx2_36,T1_37)) = tc(cons(Tx2_36,X_34),E_35,T1_37) ),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_26,plain,
! [E_27] : ( nf(lam(E_27)) = nf(E_27) ),
inference(cnfTransformation,[status(thm)],[f_45]) ).
tff(c_634,plain,
! [X_221] : ( notb(andb(nf(X_221),tc(nil,X_221,arr(a,arr(b,b))))) = sat_synth_nf_k(X_221) ),
inference(cnfTransformation,[status(thm)],[f_61]) ).
tff(c_657,plain,
! [E_27] : ( notb(andb(nf(E_27),tc(nil,lam(E_27),arr(a,arr(b,b))))) = sat_synth_nf_k(lam(E_27)) ),
inference(superposition,[status(thm),theory(equality)],[c_26,c_634]) ).
tff(c_1155,plain,
! [E_298] : ( notb(andb(nf(E_298),tc(cons(a,nil),E_298,arr(b,b)))) = sat_synth_nf_k(lam(E_298)) ),
inference(demodulation,[status(thm),theory(equality)],[c_32,c_657]) ).
tff(c_1190,plain,
! [E_27] : ( notb(andb(nf(E_27),tc(cons(a,nil),lam(E_27),arr(b,b)))) = sat_synth_nf_k(lam(lam(E_27))) ),
inference(superposition,[status(thm),theory(equality)],[c_26,c_1155]) ).
tff(c_2657,plain,
! [E_385] : ( notb(andb(nf(E_385),tc(cons(b,cons(a,nil)),E_385,b))) = sat_synth_nf_k(lam(lam(E_385))) ),
inference(demodulation,[status(thm),theory(equality)],[c_32,c_1190]) ).
tff(c_2700,plain,
notb(andb(nf(var(zero)),eq(b,b))) = sat_synth_nf_k(lam(lam(var(zero)))),
inference(superposition,[status(thm),theory(equality)],[c_467,c_2657]) ).
tff(c_2721,plain,
sat_synth_nf_k(lam(lam(var(zero)))) = bfalse,
inference(demodulation,[status(thm),theory(equality)],[c_6,c_16,c_28,c_104,c_2700]) ).
tff(c_112,plain,
! [X_118] : ( eq4(sat_synth_nf_k(X_118),bfalse) != btrue ),
inference(cnfTransformation,[status(thm)],[f_145]) ).
tff(c_2728,plain,
eq4(bfalse,bfalse) != btrue,
inference(superposition,[status(thm),theory(equality)],[c_2721,c_112]) ).
tff(c_2733,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_110,c_2728]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX222-1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/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.16/0.34 % Computer : n005.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % 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:35:00 EDT 2026
% 0.16/0.34 % CPUTime :
% 5.78/2.38 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.78/2.39
% 5.78/2.39 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------