%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWX217+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 : n014.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:37 PM UTC 2026
% Result : Theorem 147.61s 103.68s
% Output : CNFRefutation 147.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 18
% Syntax : Number of formulae : 113 ( 83 unt; 0 typ; 0 def)
% Number of atoms : 143 ( 85 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 64 ( 34 ~; 27 |; 0 &)
% ( 1 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 7 ( 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-2 aty)
% Number of functors : 16 ( 16 usr; 4 con; 0-2 aty)
% Number of variables : 83 ( 81 !; 2 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ evenNat > x > cons > append > addNat > #nlpp > tail > suc > shw > rd > proj1Suc > head > half > double > zero > o > nil > i
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(evenNat,type,
evenNat: $i > $o ).
tff(i,type,
i: $i ).
tff(half,type,
half: $i > $i ).
tff(proj1Suc,type,
proj1Suc: $i > $i ).
tff(shw,type,
shw: $i > $i ).
tff(x,type,
x: ( $i * $i ) > $i ).
tff(double,type,
double: $i > $i ).
tff(append,type,
append: ( $i * $i ) > $i ).
tff(suc,type,
suc: $i > $i ).
tff(cons,type,
cons: ( $i * $i ) > $i ).
tff(tail,type,
tail: $i > $i ).
tff(head,type,
head: $i > $i ).
tff(nil,type,
nil: $i ).
tff(addNat,type,
addNat: ( $i * $i ) > $i ).
tff(o,type,
o: $i ).
tff(rd,type,
rd: $i > $i ).
tff(zero,type,
zero: $i ).
tff(f_43,axiom,
evenNat(zero),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_010) ).
tff(f_64,axiom,
! [Y] : ( addNat(zero,Y) = Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_017) ).
tff(f_68,axiom,
! [X] : ( double(X) = addNat(X,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_019) ).
tff(f_66,axiom,
! [Y,Z] : ( addNat(suc(Z),Y) = suc(addNat(Z,Y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_018) ).
tff(f_48,axiom,
! [N] :
( evenNat(suc(N))
<=> ~ evenNat(N) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_011) ).
tff(f_69,axiom,
rd(nil) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_020) ).
tff(f_71,axiom,
! [Xs] : ( rd(cons(i,Xs)) = suc(double(rd(Xs))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_021) ).
tff(f_73,axiom,
! [Xs] : ( rd(cons(o,Xs)) = double(rd(Xs)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_022) ).
tff(f_79,negated_conjecture,
~ ? [X,Y] : ( x(X,Y) != x(Y,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal_024) ).
tff(f_60,axiom,
! [Y] : ( append(nil,Y) = Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_015) ).
tff(f_62,axiom,
! [Y,Z,Xs] : ( append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_016) ).
tff(f_49,axiom,
shw(zero) = nil,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_012) ).
tff(f_40,axiom,
half(suc(zero)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_008) ).
tff(f_58,axiom,
! [Y] :
( ~ evenNat(suc(Y))
=> ( shw(suc(Y)) = cons(i,shw(half(suc(Y)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_014) ).
tff(f_75,axiom,
! [X,Y] : ( x(X,Y) = rd(append(shw(X),shw(Y))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_023) ).
tff(f_39,axiom,
half(zero) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_007) ).
tff(f_42,axiom,
! [N] : ( half(suc(suc(N))) = suc(half(N)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_009) ).
tff(f_53,axiom,
! [Y] :
( evenNat(suc(Y))
=> ( shw(suc(Y)) = cons(o,shw(half(suc(Y)))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_013) ).
tff(c_20,plain,
evenNat(zero),
inference(cnfTransformation,[status(thm)],[f_43]) ).
tff(c_36,plain,
! [Y_17] : ( addNat(zero,Y_17) = Y_17 ),
inference(cnfTransformation,[status(thm)],[f_64]) ).
tff(c_40,plain,
! [X_20] : ( addNat(X_20,X_20) = double(X_20) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_233,plain,
! [Z_46,Y_47] : ( addNat(suc(Z_46),Y_47) = suc(addNat(Z_46,Y_47)) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_378,plain,
! [Z_65] : ( suc(addNat(Z_65,suc(Z_65))) = double(suc(Z_65)) ),
inference(superposition,[status(thm),theory(equality)],[c_40,c_233]) ).
tff(c_418,plain,
suc(suc(zero)) = double(suc(zero)),
inference(superposition,[status(thm),theory(equality)],[c_36,c_378]) ).
tff(c_24,plain,
! [N_10] :
( evenNat(suc(N_10))
| evenNat(N_10) ),
inference(cnfTransformation,[status(thm)],[f_48]) ).
tff(c_498,plain,
( evenNat(double(suc(zero)))
| evenNat(suc(zero)) ),
inference(superposition,[status(thm),theory(equality)],[c_418,c_24]) ).
tff(c_665,plain,
evenNat(suc(zero)),
inference(splitLeft,[status(thm)],[c_498]) ).
tff(c_22,plain,
! [N_10] :
( ~ evenNat(N_10)
| ~ evenNat(suc(N_10)) ),
inference(cnfTransformation,[status(thm)],[f_48]) ).
tff(c_668,plain,
~ evenNat(zero),
inference(resolution,[status(thm)],[c_665,c_22]) ).
tff(c_672,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_20,c_668]) ).
tff(c_673,plain,
evenNat(double(suc(zero))),
inference(splitRight,[status(thm)],[c_498]) ).
tff(c_139,plain,
! [X_38] : ( addNat(X_38,X_38) = double(X_38) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_146,plain,
double(zero) = zero,
inference(superposition,[status(thm),theory(equality)],[c_139,c_36]) ).
tff(c_42,plain,
rd(nil) = zero,
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_193,plain,
! [Xs_44] : ( suc(double(rd(Xs_44))) = rd(cons(i,Xs_44)) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_219,plain,
suc(double(zero)) = rd(cons(i,nil)),
inference(superposition,[status(thm),theory(equality)],[c_42,c_193]) ).
tff(c_222,plain,
rd(cons(i,nil)) = suc(zero),
inference(demodulation,[status(thm),theory(equality)],[c_146,c_219]) ).
tff(c_44,plain,
! [Xs_21] : ( suc(double(rd(Xs_21))) = rd(cons(i,Xs_21)) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_229,plain,
suc(double(suc(zero))) = rd(cons(i,cons(i,nil))),
inference(superposition,[status(thm),theory(equality)],[c_222,c_44]) ).
tff(c_4664,plain,
( ~ evenNat(double(suc(zero)))
| ~ evenNat(rd(cons(i,cons(i,nil)))) ),
inference(superposition,[status(thm),theory(equality)],[c_229,c_22]) ).
tff(c_4699,plain,
~ evenNat(rd(cons(i,cons(i,nil)))),
inference(demodulation,[status(thm),theory(equality)],[c_673,c_4664]) ).
tff(c_38,plain,
! [Z_19,Y_18] : ( addNat(suc(Z_19),Y_18) = suc(addNat(Z_19,Y_18)) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_1469,plain,
! [Z_127] :
( evenNat(double(suc(Z_127)))
| evenNat(addNat(Z_127,suc(Z_127))) ),
inference(superposition,[status(thm),theory(equality)],[c_378,c_24]) ).
tff(c_1485,plain,
( evenNat(double(suc(suc(zero))))
| evenNat(addNat(suc(zero),double(suc(zero)))) ),
inference(superposition,[status(thm),theory(equality)],[c_418,c_1469]) ).
tff(c_1502,plain,
( evenNat(double(double(suc(zero))))
| evenNat(suc(double(suc(zero)))) ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_38,c_418,c_1485]) ).
tff(c_6526,plain,
( evenNat(double(double(suc(zero))))
| evenNat(rd(cons(i,cons(i,nil)))) ),
inference(demodulation,[status(thm),theory(equality)],[c_229,c_1502]) ).
tff(c_6527,plain,
evenNat(double(double(suc(zero)))),
inference(negUnitSimplification,[status(thm)],[c_4699,c_6526]) ).
tff(c_46,plain,
! [Xs_22] : ( rd(cons(o,Xs_22)) = double(rd(Xs_22)) ),
inference(cnfTransformation,[status(thm)],[f_73]) ).
tff(c_1750,plain,
! [Xs_138] : ( suc(double(double(rd(Xs_138)))) = rd(cons(i,cons(o,Xs_138))) ),
inference(superposition,[status(thm),theory(equality)],[c_46,c_193]) ).
tff(c_1856,plain,
suc(double(double(suc(zero)))) = rd(cons(i,cons(o,cons(i,nil)))),
inference(superposition,[status(thm),theory(equality)],[c_222,c_1750]) ).
tff(c_10592,plain,
( ~ evenNat(double(double(suc(zero))))
| ~ evenNat(rd(cons(i,cons(o,cons(i,nil))))) ),
inference(superposition,[status(thm),theory(equality)],[c_1856,c_22]) ).
tff(c_10663,plain,
~ evenNat(rd(cons(i,cons(o,cons(i,nil))))),
inference(demodulation,[status(thm),theory(equality)],[c_6527,c_10592]) ).
tff(c_50,plain,
! [Y_26,X_25] : ( x(Y_26,X_25) = x(X_25,Y_26) ),
inference(cnfTransformation,[status(thm)],[f_79]) ).
tff(c_32,plain,
! [Y_13] : ( append(nil,Y_13) = Y_13 ),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_308,plain,
! [Z_52,Xs_53,Y_54] : ( cons(Z_52,append(Xs_53,Y_54)) = append(cons(Z_52,Xs_53),Y_54) ),
inference(cnfTransformation,[status(thm)],[f_62]) ).
tff(c_333,plain,
! [Z_52,Y_13] : ( append(cons(Z_52,nil),Y_13) = cons(Z_52,Y_13) ),
inference(superposition,[status(thm),theory(equality)],[c_32,c_308]) ).
tff(c_674,plain,
~ evenNat(suc(zero)),
inference(splitRight,[status(thm)],[c_498]) ).
tff(c_26,plain,
shw(zero) = nil,
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_16,plain,
half(suc(zero)) = zero,
inference(cnfTransformation,[status(thm)],[f_40]) ).
tff(c_424,plain,
! [Y_66] :
( ( cons(i,shw(half(suc(Y_66)))) = shw(suc(Y_66)) )
| evenNat(suc(Y_66)) ),
inference(cnfTransformation,[status(thm)],[f_58]) ).
tff(c_459,plain,
( ( cons(i,shw(zero)) = shw(suc(zero)) )
| evenNat(suc(zero)) ),
inference(superposition,[status(thm),theory(equality)],[c_16,c_424]) ).
tff(c_465,plain,
( ( shw(suc(zero)) = cons(i,nil) )
| evenNat(suc(zero)) ),
inference(demodulation,[status(thm),theory(equality)],[c_26,c_459]) ).
tff(c_1075,plain,
shw(suc(zero)) = cons(i,nil),
inference(negUnitSimplification,[status(thm)],[c_674,c_465]) ).
tff(c_253,plain,
! [X_48,Y_49] : ( rd(append(shw(X_48),shw(Y_49))) = x(X_48,Y_49) ),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_268,plain,
! [X_48] : ( rd(append(shw(X_48),nil)) = x(X_48,zero) ),
inference(superposition,[status(thm),theory(equality)],[c_26,c_253]) ).
tff(c_1087,plain,
rd(append(cons(i,nil),nil)) = x(suc(zero),zero),
inference(superposition,[status(thm),theory(equality)],[c_1075,c_268]) ).
tff(c_1103,plain,
x(zero,suc(zero)) = suc(zero),
inference(demodulation,[status(thm),theory(equality)],[c_50,c_222,c_333,c_1087]) ).
tff(c_48,plain,
! [X_23,Y_24] : ( rd(append(shw(X_23),shw(Y_24))) = x(X_23,Y_24) ),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_1093,plain,
! [Y_24] : ( rd(append(cons(i,nil),shw(Y_24))) = x(suc(zero),Y_24) ),
inference(superposition,[status(thm),theory(equality)],[c_1075,c_48]) ).
tff(c_1105,plain,
! [Y_24] : ( rd(cons(i,shw(Y_24))) = x(suc(zero),Y_24) ),
inference(demodulation,[status(thm),theory(equality)],[c_333,c_1093]) ).
tff(c_34,plain,
! [Z_15,Xs_16,Y_14] : ( cons(Z_15,append(Xs_16,Y_14)) = append(cons(Z_15,Xs_16),Y_14) ),
inference(cnfTransformation,[status(thm)],[f_62]) ).
tff(c_259,plain,
! [X_48,Y_49] : ( rd(cons(i,append(shw(X_48),shw(Y_49)))) = suc(double(x(X_48,Y_49))) ),
inference(superposition,[status(thm),theory(equality)],[c_253,c_44]) ).
tff(c_2758,plain,
! [X_177,Y_178] : ( rd(append(cons(i,shw(X_177)),shw(Y_178))) = suc(double(x(X_177,Y_178))) ),
inference(demodulation,[status(thm),theory(equality)],[c_34,c_259]) ).
tff(c_2794,plain,
! [Y_178] : ( rd(append(cons(i,nil),shw(Y_178))) = suc(double(x(zero,Y_178))) ),
inference(superposition,[status(thm),theory(equality)],[c_26,c_2758]) ).
tff(c_2838,plain,
! [Y_182] : ( suc(double(x(zero,Y_182))) = x(suc(zero),Y_182) ),
inference(demodulation,[status(thm),theory(equality)],[c_1105,c_333,c_2794]) ).
tff(c_2947,plain,
x(suc(zero),suc(zero)) = suc(double(suc(zero))),
inference(superposition,[status(thm),theory(equality)],[c_1103,c_2838]) ).
tff(c_4561,plain,
x(suc(zero),suc(zero)) = rd(cons(i,cons(i,nil))),
inference(demodulation,[status(thm),theory(equality)],[c_229,c_2947]) ).
tff(c_14,plain,
half(zero) = zero,
inference(cnfTransformation,[status(thm)],[f_39]) ).
tff(c_18,plain,
! [N_9] : ( half(suc(suc(N_9))) = suc(half(N_9)) ),
inference(cnfTransformation,[status(thm)],[f_42]) ).
tff(c_495,plain,
half(double(suc(zero))) = suc(half(zero)),
inference(superposition,[status(thm),theory(equality)],[c_418,c_18]) ).
tff(c_513,plain,
half(double(suc(zero))) = suc(zero),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_495]) ).
tff(c_265,plain,
! [Y_49] : ( rd(append(nil,shw(Y_49))) = x(zero,Y_49) ),
inference(superposition,[status(thm),theory(equality)],[c_26,c_253]) ).
tff(c_271,plain,
! [Y_49] : ( rd(shw(Y_49)) = x(zero,Y_49) ),
inference(demodulation,[status(thm),theory(equality)],[c_32,c_265]) ).
tff(c_515,plain,
! [Y_69] :
( ( cons(o,shw(half(suc(Y_69)))) = shw(suc(Y_69)) )
| ~ evenNat(suc(Y_69)) ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_526,plain,
! [Y_69] :
( ( double(rd(shw(half(suc(Y_69))))) = rd(shw(suc(Y_69))) )
| ~ evenNat(suc(Y_69)) ),
inference(superposition,[status(thm),theory(equality)],[c_515,c_46]) ).
tff(c_2615,plain,
! [Y_168] :
( ( double(x(zero,half(suc(Y_168)))) = x(zero,suc(Y_168)) )
| ~ evenNat(suc(Y_168)) ),
inference(demodulation,[status(thm),theory(equality)],[c_271,c_271,c_526]) ).
tff(c_2642,plain,
( ( double(x(zero,half(double(suc(zero))))) = x(zero,suc(suc(zero))) )
| ~ evenNat(suc(suc(zero))) ),
inference(superposition,[status(thm),theory(equality)],[c_418,c_2615]) ).
tff(c_2664,plain,
x(zero,double(suc(zero))) = double(suc(zero)),
inference(demodulation,[status(thm),theory(equality)],[c_673,c_418,c_1103,c_418,c_513,c_2642]) ).
tff(c_28,plain,
! [Y_11] :
( ( cons(o,shw(half(suc(Y_11)))) = shw(suc(Y_11)) )
| ~ evenNat(suc(Y_11)) ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_1324,plain,
! [Xs_116,Y_117] : ( rd(append(cons(o,Xs_116),Y_117)) = double(rd(append(Xs_116,Y_117))) ),
inference(superposition,[status(thm),theory(equality)],[c_308,c_46]) ).
tff(c_39778,plain,
! [Y_923,Y_924] :
( ( double(rd(append(shw(half(suc(Y_923))),Y_924))) = rd(append(shw(suc(Y_923)),Y_924)) )
| ~ evenNat(suc(Y_923)) ),
inference(superposition,[status(thm),theory(equality)],[c_28,c_1324]) ).
tff(c_39952,plain,
! [Y_923,Y_24] :
( ( rd(append(shw(suc(Y_923)),shw(Y_24))) = double(x(half(suc(Y_923)),Y_24)) )
| ~ evenNat(suc(Y_923)) ),
inference(superposition,[status(thm),theory(equality)],[c_48,c_39778]) ).
tff(c_105040,plain,
! [Y_1852,Y_1853] :
( ( double(x(half(suc(Y_1852)),Y_1853)) = x(suc(Y_1852),Y_1853) )
| ~ evenNat(suc(Y_1852)) ),
inference(demodulation,[status(thm),theory(equality)],[c_48,c_39952]) ).
tff(c_105394,plain,
! [Y_1853] :
( ( double(x(half(double(suc(zero))),Y_1853)) = x(suc(suc(zero)),Y_1853) )
| ~ evenNat(suc(suc(zero))) ),
inference(superposition,[status(thm),theory(equality)],[c_418,c_105040]) ).
tff(c_105473,plain,
! [Y_1854] : ( x(double(suc(zero)),Y_1854) = double(x(suc(zero),Y_1854)) ),
inference(demodulation,[status(thm),theory(equality)],[c_673,c_418,c_418,c_513,c_105394]) ).
tff(c_1233,plain,
! [Y_113] : ( rd(cons(i,shw(Y_113))) = x(suc(zero),Y_113) ),
inference(demodulation,[status(thm),theory(equality)],[c_333,c_1093]) ).
tff(c_205,plain,
! [Xs_44] :
( ~ evenNat(double(rd(Xs_44)))
| ~ evenNat(rd(cons(i,Xs_44))) ),
inference(superposition,[status(thm),theory(equality)],[c_193,c_22]) ).
tff(c_1239,plain,
! [Y_113] :
( ~ evenNat(double(rd(shw(Y_113))))
| ~ evenNat(x(suc(zero),Y_113)) ),
inference(superposition,[status(thm),theory(equality)],[c_1233,c_205]) ).
tff(c_5133,plain,
! [Y_251] :
( ~ evenNat(double(x(zero,Y_251)))
| ~ evenNat(x(suc(zero),Y_251)) ),
inference(demodulation,[status(thm),theory(equality)],[c_271,c_1239]) ).
tff(c_5144,plain,
! [X_25] :
( ~ evenNat(double(x(zero,X_25)))
| ~ evenNat(x(X_25,suc(zero))) ),
inference(superposition,[status(thm),theory(equality)],[c_50,c_5133]) ).
tff(c_105990,plain,
( ~ evenNat(double(x(zero,double(suc(zero)))))
| ~ evenNat(double(x(suc(zero),suc(zero)))) ),
inference(superposition,[status(thm),theory(equality)],[c_105473,c_5144]) ).
tff(c_106239,plain,
~ evenNat(double(rd(cons(i,cons(i,nil))))),
inference(demodulation,[status(thm),theory(equality)],[c_4561,c_6527,c_2664,c_105990]) ).
tff(c_250,plain,
! [Z_46] : ( suc(addNat(Z_46,suc(Z_46))) = double(suc(Z_46)) ),
inference(superposition,[status(thm),theory(equality)],[c_40,c_233]) ).
tff(c_486,plain,
suc(addNat(suc(zero),double(suc(zero)))) = double(suc(suc(zero))),
inference(superposition,[status(thm),theory(equality)],[c_418,c_250]) ).
tff(c_510,plain,
suc(suc(double(suc(zero)))) = double(double(suc(zero))),
inference(demodulation,[status(thm),theory(equality)],[c_418,c_36,c_38,c_486]) ).
tff(c_4562,plain,
suc(rd(cons(i,cons(i,nil)))) = double(double(suc(zero))),
inference(demodulation,[status(thm),theory(equality)],[c_229,c_510]) ).
tff(c_489,plain,
! [Y_18] : ( addNat(double(suc(zero)),Y_18) = suc(addNat(suc(zero),Y_18)) ),
inference(superposition,[status(thm),theory(equality)],[c_418,c_38]) ).
tff(c_511,plain,
! [Y_18] : ( addNat(double(suc(zero)),Y_18) = suc(suc(Y_18)) ),
inference(demodulation,[status(thm),theory(equality)],[c_36,c_38,c_489]) ).
tff(c_4652,plain,
suc(addNat(double(suc(zero)),rd(cons(i,cons(i,nil))))) = double(suc(double(suc(zero)))),
inference(superposition,[status(thm),theory(equality)],[c_229,c_250]) ).
tff(c_4694,plain,
suc(suc(suc(rd(cons(i,cons(i,nil)))))) = double(rd(cons(i,cons(i,nil)))),
inference(demodulation,[status(thm),theory(equality)],[c_229,c_511,c_4652]) ).
tff(c_198414,plain,
suc(rd(cons(i,cons(o,cons(i,nil))))) = double(rd(cons(i,cons(i,nil)))),
inference(demodulation,[status(thm),theory(equality)],[c_1856,c_4562,c_4694]) ).
tff(c_200550,plain,
( evenNat(double(rd(cons(i,cons(i,nil)))))
| evenNat(rd(cons(i,cons(o,cons(i,nil))))) ),
inference(superposition,[status(thm),theory(equality)],[c_198414,c_24]) ).
tff(c_201366,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_10663,c_106239,c_200550]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX217+1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/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.15/0.34 % Computer : n014.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Tue May 5 12:15:21 EDT 2026
% 0.15/0.34 % CPUTime :
% 147.61/103.68 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 147.61/103.70
% 147.61/103.70 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------