%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYO691-1.001 : TPTP v9.0.0. Released v7.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 : n003.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 10:38:07 PM UTC 2025
% Result : Unsatisfiable 13.26s 5.12s
% Output : CNFRefutation 13.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 7
% Syntax : Number of formulae : 32 ( 11 unt; 0 typ; 0 def)
% Number of atoms : 62 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 66 ( 36 ~; 30 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 6 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 : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 106 ( 106 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ seq > top > step > f > #nlpp > succ > zero > a
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(top,type,
top: ( $i * $i ) > $o ).
tff(a,type,
a: $i ).
tff(step,type,
step: ( $i * $i ) > $o ).
tff(succ,type,
succ: $i > $i ).
tff(f,type,
f: ( $i * $i ) > $i ).
tff(zero,type,
zero: $i ).
tff(seq,type,
seq: ( $i * $i * $i ) > $o ).
tff(f_23,axiom,
! [Z,Y,X] : top(f(f(f(Z,a),Y),f(X,a)),f(f(X,f(f(Y,a),a)),Z)),
file(unknown,unknown) ).
tff(f_31,axiom,
! [X,Y] :
( ~ top(X,Y)
| step(X,Y) ),
file(unknown,unknown) ).
tff(f_36,axiom,
! [X,Y,Z] :
( ~ step(X,Y)
| step(f(X,Z),f(Y,Z)) ),
file(unknown,unknown) ).
tff(f_43,axiom,
! [X] : seq(zero,X,X),
file(unknown,unknown) ).
tff(f_41,axiom,
! [Y,Z,X] :
( ~ step(Y,Z)
| step(f(X,Y),f(X,Z)) ),
file(unknown,unknown) ).
tff(f_51,axiom,
! [N,X,Y,Z] :
( ~ seq(N,X,Y)
| ~ step(Y,Z)
| seq(succ(N),X,Z) ),
file(unknown,unknown) ).
tff(f_26,axiom,
! [X] : ~ seq(succ(succ(succ(succ(succ(zero))))),X,X),
file(unknown,unknown) ).
tff(c_44,plain,
! [Z_45,Y_46,X_47] : top(f(f(f(Z_45,a),Y_46),f(X_47,a)),f(f(X_47,f(f(Y_46,a),a)),Z_45)),
inference(cnfTransformation,[status(thm)],[f_23]) ).
tff(c_6,plain,
! [X_5,Y_6] :
( step(X_5,Y_6)
| ~ top(X_5,Y_6) ),
inference(cnfTransformation,[status(thm)],[f_31]) ).
tff(c_48,plain,
! [Z_45,Y_46,X_47] : step(f(f(f(Z_45,a),Y_46),f(X_47,a)),f(f(X_47,f(f(Y_46,a),a)),Z_45)),
inference(resolution,[status(thm)],[c_44,c_6]) ).
tff(c_8,plain,
! [X_7,Z_9,Y_8] :
( step(f(X_7,Z_9),f(Y_8,Z_9))
| ~ step(X_7,Y_8) ),
inference(cnfTransformation,[status(thm)],[f_36]) ).
tff(c_77,plain,
! [Z_63,Y_64,X_65] : step(f(f(f(Z_63,a),Y_64),f(X_65,a)),f(f(X_65,f(f(Y_64,a),a)),Z_63)),
inference(resolution,[status(thm)],[c_44,c_6]) ).
tff(c_12,plain,
! [X_13] : seq(zero,X_13,X_13),
inference(cnfTransformation,[status(thm)],[f_43]) ).
tff(c_10,plain,
! [X_12,Y_10,Z_11] :
( step(f(X_12,Y_10),f(X_12,Z_11))
| ~ step(Y_10,Z_11) ),
inference(cnfTransformation,[status(thm)],[f_41]) ).
tff(c_20,plain,
! [N_28,X_29,Z_30,Y_31] :
( seq(succ(N_28),X_29,Z_30)
| ~ step(Y_31,Z_30)
| ~ seq(N_28,X_29,Y_31) ),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_27,plain,
! [Z_36,X_32,Y_33,N_35,X_34] :
( seq(succ(N_35),X_32,f(X_34,Z_36))
| ~ seq(N_35,X_32,f(X_34,Y_33))
| ~ step(Y_33,Z_36) ),
inference(resolution,[status(thm)],[c_10,c_20]) ).
tff(c_32,plain,
! [X_37,Y_38,Z_39] :
( seq(succ(zero),f(X_37,Y_38),f(X_37,Z_39))
| ~ step(Y_38,Z_39) ),
inference(resolution,[status(thm)],[c_12,c_27]) ).
tff(c_25,plain,
! [X_29,Z_11,Y_10,X_12,N_28] :
( seq(succ(N_28),X_29,f(X_12,Z_11))
| ~ seq(N_28,X_29,f(X_12,Y_10))
| ~ step(Y_10,Z_11) ),
inference(resolution,[status(thm)],[c_10,c_20]) ).
tff(c_35,plain,
! [X_37,Y_38,Z_11,Z_39] :
( seq(succ(succ(zero)),f(X_37,Y_38),f(X_37,Z_11))
| ~ step(Z_39,Z_11)
| ~ step(Y_38,Z_39) ),
inference(resolution,[status(thm)],[c_32,c_25]) ).
tff(c_535,plain,
! [X_308,Y_310,Z_312,Y_311,X_309] :
( seq(succ(succ(zero)),f(X_309,Y_310),f(X_309,f(f(X_308,f(f(Y_311,a),a)),Z_312)))
| ~ step(Y_310,f(f(f(Z_312,a),Y_311),f(X_308,a))) ),
inference(resolution,[status(thm)],[c_77,c_35]) ).
tff(c_26,plain,
! [Y_8,Z_9,X_29,X_7,N_28] :
( seq(succ(N_28),X_29,f(Y_8,Z_9))
| ~ seq(N_28,X_29,f(X_7,Z_9))
| ~ step(X_7,Y_8) ),
inference(resolution,[status(thm)],[c_8,c_20]) ).
tff(c_2499,plain,
! [Z_1228,Y_1229,Y_1225,Y_1224,X_1227,X_1226] :
( seq(succ(succ(succ(zero))),f(X_1226,Y_1225),f(Y_1224,f(f(X_1227,f(f(Y_1229,a),a)),Z_1228)))
| ~ step(X_1226,Y_1224)
| ~ step(Y_1225,f(f(f(Z_1228,a),Y_1229),f(X_1227,a))) ),
inference(resolution,[status(thm)],[c_535,c_26]) ).
tff(c_14,plain,
! [N_14,X_15,Z_17,Y_16] :
( seq(succ(N_14),X_15,Z_17)
| ~ step(Y_16,Z_17)
| ~ seq(N_14,X_15,Y_16) ),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_177,plain,
! [X_111,Y_114,Z_115,N_112,X_113] :
( seq(succ(N_112),X_113,f(f(X_111,f(f(Y_114,a),a)),Z_115))
| ~ seq(N_112,X_113,f(f(f(Z_115,a),Y_114),f(X_111,a))) ),
inference(resolution,[status(thm)],[c_77,c_14]) ).
tff(c_323,plain,
! [Y_201,N_205,X_204,X_202,Y_200,Z_203] :
( seq(succ(succ(N_205)),X_204,f(Y_200,Z_203))
| ~ step(f(X_202,f(f(Y_201,a),a)),Y_200)
| ~ seq(N_205,X_204,f(f(f(Z_203,a),Y_201),f(X_202,a))) ),
inference(resolution,[status(thm)],[c_177,c_26]) ).
tff(c_1261,plain,
! [Y_655,Z_660,Z_658,Y_656,N_657,X_659] :
( seq(succ(succ(N_657)),X_659,f(f(f(f(Y_656,a),f(f(Y_655,a),a)),Z_660),Z_658))
| ~ seq(N_657,X_659,f(f(f(Z_658,a),Y_656),f(f(f(Z_660,a),Y_655),a))) ),
inference(resolution,[status(thm)],[c_48,c_323]) ).
tff(c_4,plain,
! [X_4] : ~ seq(succ(succ(succ(succ(succ(zero))))),X_4,X_4),
inference(cnfTransformation,[status(thm)],[f_26]) ).
tff(c_1272,plain,
! [Y_656,Y_655,Z_660,Z_658] : ~ seq(succ(succ(succ(zero))),f(f(f(f(Y_656,a),f(f(Y_655,a),a)),Z_660),Z_658),f(f(f(Z_658,a),Y_656),f(f(f(Z_660,a),Y_655),a))),
inference(resolution,[status(thm)],[c_1261,c_4]) ).
tff(c_6829,plain,
! [Y_3794,Y_3795,Z_3796,Y_3797] :
( ~ step(f(f(f(Y_3794,a),f(f(f(f(Y_3795,a),a),a),a)),Z_3796),f(f(Y_3797,a),Y_3794))
| ~ step(Y_3797,f(f(f(a,a),Y_3795),f(f(Z_3796,a),a))) ),
inference(resolution,[status(thm)],[c_2499,c_1272]) ).
tff(c_6835,plain,
! [Y_3798,Y_3799,Z_3800] :
( ~ step(Y_3798,f(f(f(a,a),Y_3799),f(f(Z_3800,a),a)))
| ~ step(f(f(Z_3800,a),f(f(f(f(Y_3799,a),a),a),a)),f(Y_3798,a)) ),
inference(resolution,[status(thm)],[c_8,c_6829]) ).
tff(c_6846,plain,
! [Y_3801] : ~ step(f(f(f(f(Y_3801,a),a),a),f(f(a,a),a)),f(f(f(a,a),Y_3801),f(f(f(a,a),a),a))),
inference(resolution,[status(thm)],[c_48,c_6835]) ).
tff(c_6851,plain,
$false,
inference(resolution,[status(thm)],[c_48,c_6846]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : SYO691-1.001 : TPTP v9.0.0. Released v7.3.0.
% 0.10/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.12/0.34 % Computer : n003.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Apr 9 09:44:48 EDT 2025
% 0.12/0.34 % CPUTime :
% 13.26/5.12 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.26/5.13
% 13.26/5.13 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------