%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYN632-1 : TPTP v9.0.0. Released v2.5.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 : n019.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:04:04 PM UTC 2025
% Result : Unsatisfiable 16.77s 6.13s
% Output : CNFRefutation 16.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 11
% Syntax : Number of formulae : 39 ( 9 unt; 0 typ; 0 def)
% Number of atoms : 93 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 112 ( 58 ~; 54 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 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 : 13 ( 12 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 8 con; 0-2 aty)
% Number of variables : 114 ( 114 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ p9 > p8 > p6 > p4 > p3 > p21 > p2 > p19 > p17 > p15 > p13 > p11 > f7 > f5 > f20 > f18 > f16 > f14 > f12 > f10 > #nlpp > c29 > c28 > c27 > c26 > c25 > c24 > c23 > c22
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(f5,type,
f5: ( $i * $i ) > $i ).
tff(p15,type,
p15: ( $i * $i ) > $o ).
tff(p4,type,
p4: ( $i * $i ) > $o ).
tff(f12,type,
f12: ( $i * $i ) > $i ).
tff(p13,type,
p13: ( $i * $i ) > $o ).
tff(p2,type,
p2: ( $i * $i ) > $o ).
tff(f14,type,
f14: ( $i * $i ) > $i ).
tff(c26,type,
c26: $i ).
tff(p21,type,
p21: ( $i * $i ) > $o ).
tff(c23,type,
c23: $i ).
tff(p11,type,
p11: ( $i * $i ) > $o ).
tff(p17,type,
p17: ( $i * $i ) > $o ).
tff(p8,type,
p8: ( $i * $i ) > $o ).
tff(c22,type,
c22: $i ).
tff(c27,type,
c27: $i ).
tff(f7,type,
f7: ( $i * $i ) > $i ).
tff(f18,type,
f18: ( $i * $i ) > $i ).
tff(p3,type,
p3: ( $i * $i ) > $o ).
tff(p19,type,
p19: ( $i * $i ) > $o ).
tff(c25,type,
c25: $i ).
tff(c29,type,
c29: $i ).
tff(f16,type,
f16: ( $i * $i ) > $i ).
tff(p6,type,
p6: ( $i * $i ) > $o ).
tff(f10,type,
f10: ( $i * $i ) > $i ).
tff(c28,type,
c28: $i ).
tff(p9,type,
p9: ( $i * $i ) > $o ).
tff(f20,type,
f20: ( $i * $i ) > $i ).
tff(c24,type,
c24: $i ).
tff(f_33,axiom,
! [X46] : p3(X46,X46),
file(unknown,unknown) ).
tff(f_143,axiom,
p21(f5(f7(f10(c24,f12(c28,f12(c25,c26))),c22),c23),c27),
file(unknown,unknown) ).
tff(f_35,axiom,
! [X27] : p2(X27,X27),
file(unknown,unknown) ).
tff(f_241,axiom,
! [X39,X38,X40,X41] :
( p21(f5(f7(f10(c24,X39),X38),X40),f14(f16(f18(f20(c29,X39),X40),X38),X41))
| ~ p21(f5(f7(f10(c24,f12(c28,X39)),X38),X40),X41) ),
file(unknown,unknown) ).
tff(f_212,axiom,
! [X43,X44,X42] :
( p3(X43,X44)
| ~ p21(f5(f7(f10(c24,f12(c25,c26)),X42),X43),X44) ),
file(unknown,unknown) ).
tff(f_91,axiom,
! [X47,X48,X46] :
( p3(X47,X48)
| ~ p3(X46,X47)
| ~ p3(X46,X48) ),
file(unknown,unknown) ).
tff(f_199,axiom,
! [X56,X57,X58,X59] :
( p4(f5(X56,X57),f5(X58,X59))
| ~ p2(X56,X58)
| ~ p3(X57,X59) ),
file(unknown,unknown) ).
tff(f_228,axiom,
! [X38,X39,X40,X41] :
( p21(f5(X38,f14(f16(f18(f20(c29,X39),X40),X38),X41)),X41)
| ~ p21(f5(f7(f10(c24,f12(c28,X39)),X38),X40),X41) ),
file(unknown,unknown) ).
tff(f_142,axiom,
! [X34,X35,X37,X36] :
( p21(X34,X35)
| ~ p3(X37,X35)
| ~ p4(X36,X34)
| ~ p21(X36,X37) ),
file(unknown,unknown) ).
tff(f_217,axiom,
! [X42,X43,X44] :
( p21(f5(f7(f10(c24,f12(c25,c26)),X42),X43),X44)
| ~ p3(X43,X44) ),
file(unknown,unknown) ).
tff(f_223,axiom,
! [X77] :
( ~ p21(f5(c22,c23),X77)
| ~ p21(f5(f7(f10(c24,f12(c25,c26)),c22),X77),c27) ),
file(unknown,unknown) ).
tff(c_12,plain,
! [X46_6] : p3(X46_6,X46_6),
inference(cnfTransformation,[status(thm)],[f_33]) ).
tff(c_48,plain,
p21(f5(f7(f10(c24,f12(c28,f12(c25,c26))),c22),c23),c27),
inference(cnfTransformation,[status(thm)],[f_143]) ).
tff(c_14,plain,
! [X27_7] : p2(X27_7,X27_7),
inference(cnfTransformation,[status(thm)],[f_35]) ).
tff(c_432,plain,
! [X39_292,X38_293,X40_294,X41_295] :
( ~ p21(f5(f7(f10(c24,f12(c28,X39_292)),X38_293),X40_294),X41_295)
| p21(f5(f7(f10(c24,X39_292),X38_293),X40_294),f14(f16(f18(f20(c29,X39_292),X40_294),X38_293),X41_295)) ),
inference(cnfTransformation,[status(thm)],[f_241]) ).
tff(c_66,plain,
! [X42_83,X43_81,X44_82] :
( ~ p21(f5(f7(f10(c24,f12(c25,c26)),X42_83),X43_81),X44_82)
| p3(X43_81,X44_82) ),
inference(cnfTransformation,[status(thm)],[f_212]) ).
tff(c_833,plain,
! [X40_491,X38_492,X41_493] :
( p3(X40_491,f14(f16(f18(f20(c29,f12(c25,c26)),X40_491),X38_492),X41_493))
| ~ p21(f5(f7(f10(c24,f12(c28,f12(c25,c26))),X38_492),X40_491),X41_493) ),
inference(resolution,[status(thm)],[c_432,c_66]) ).
tff(c_142,plain,
! [X46_142,X48_143,X47_144] :
( ~ p3(X46_142,X48_143)
| ~ p3(X46_142,X47_144)
| p3(X47_144,X48_143) ),
inference(cnfTransformation,[status(thm)],[f_91]) ).
tff(c_145,plain,
! [X46_6,X47_144] :
( ~ p3(X46_6,X47_144)
| p3(X47_144,X46_6) ),
inference(resolution,[status(thm)],[c_12,c_142]) ).
tff(c_864,plain,
! [X40_491,X38_492,X41_493] :
( p3(f14(f16(f18(f20(c29,f12(c25,c26)),X40_491),X38_492),X41_493),X40_491)
| ~ p21(f5(f7(f10(c24,f12(c28,f12(c25,c26))),X38_492),X40_491),X41_493) ),
inference(resolution,[status(thm)],[c_833,c_145]) ).
tff(c_62,plain,
! [X57_74,X59_76,X56_73,X58_75] :
( ~ p3(X57_74,X59_76)
| ~ p2(X56_73,X58_75)
| p4(f5(X56_73,X57_74),f5(X58_75,X59_76)) ),
inference(cnfTransformation,[status(thm)],[f_199]) ).
tff(c_319,plain,
! [X39_243,X38_244,X40_245,X41_246] :
( ~ p21(f5(f7(f10(c24,f12(c28,X39_243)),X38_244),X40_245),X41_246)
| p21(f5(X38_244,f14(f16(f18(f20(c29,X39_243),X40_245),X38_244),X41_246)),X41_246) ),
inference(cnfTransformation,[status(thm)],[f_228]) ).
tff(c_46,plain,
! [X36_48,X37_47,X34_45,X35_46] :
( ~ p21(X36_48,X37_47)
| ~ p4(X36_48,X34_45)
| ~ p3(X37_47,X35_46)
| p21(X34_45,X35_46) ),
inference(cnfTransformation,[status(thm)],[f_142]) ).
tff(c_944,plain,
! [X38_545,X41_543,X39_548,X34_547,X35_544,X40_546] :
( ~ p4(f5(X38_545,f14(f16(f18(f20(c29,X39_548),X40_546),X38_545),X41_543)),X34_547)
| ~ p3(X41_543,X35_544)
| p21(X34_547,X35_544)
| ~ p21(f5(f7(f10(c24,f12(c28,X39_548)),X38_545),X40_546),X41_543) ),
inference(resolution,[status(thm)],[c_319,c_46]) ).
tff(c_3831,plain,
! [X40_1240,X35_1238,X41_1242,X59_1236,X56_1239,X39_1237,X58_1241] :
( ~ p3(X41_1242,X35_1238)
| p21(f5(X58_1241,X59_1236),X35_1238)
| ~ p21(f5(f7(f10(c24,f12(c28,X39_1237)),X56_1239),X40_1240),X41_1242)
| ~ p3(f14(f16(f18(f20(c29,X39_1237),X40_1240),X56_1239),X41_1242),X59_1236)
| ~ p2(X56_1239,X58_1241) ),
inference(resolution,[status(thm)],[c_62,c_944]) ).
tff(c_16057,plain,
! [X40_3022,X39_3026,X58_3024,X46_3021,X56_3025,X59_3023] :
( p21(f5(X58_3024,X59_3023),X46_3021)
| ~ p21(f5(f7(f10(c24,f12(c28,X39_3026)),X56_3025),X40_3022),X46_3021)
| ~ p3(f14(f16(f18(f20(c29,X39_3026),X40_3022),X56_3025),X46_3021),X59_3023)
| ~ p2(X56_3025,X58_3024) ),
inference(resolution,[status(thm)],[c_12,c_3831]) ).
tff(c_16126,plain,
! [X58_3027,X40_3028,X41_3029,X38_3030] :
( p21(f5(X58_3027,X40_3028),X41_3029)
| ~ p2(X38_3030,X58_3027)
| ~ p21(f5(f7(f10(c24,f12(c28,f12(c25,c26))),X38_3030),X40_3028),X41_3029) ),
inference(resolution,[status(thm)],[c_864,c_16057]) ).
tff(c_16160,plain,
! [X27_3031,X40_3032,X41_3033] :
( p21(f5(X27_3031,X40_3032),X41_3033)
| ~ p21(f5(f7(f10(c24,f12(c28,f12(c25,c26))),X27_3031),X40_3032),X41_3033) ),
inference(resolution,[status(thm)],[c_14,c_16126]) ).
tff(c_16349,plain,
p21(f5(c22,c23),c27),
inference(resolution,[status(thm)],[c_48,c_16160]) ).
tff(c_261,plain,
! [X43_211,X44_212,X42_213] :
( ~ p3(X43_211,X44_212)
| p21(f5(f7(f10(c24,f12(c25,c26)),X42_213),X43_211),X44_212) ),
inference(cnfTransformation,[status(thm)],[f_217]) ).
tff(c_627,plain,
! [X44_386,X42_384,X34_388,X35_387,X43_385] :
( ~ p4(f5(f7(f10(c24,f12(c25,c26)),X42_384),X43_385),X34_388)
| ~ p3(X44_386,X35_387)
| p21(X34_388,X35_387)
| ~ p3(X43_385,X44_386) ),
inference(resolution,[status(thm)],[c_261,c_46]) ).
tff(c_1402,plain,
! [X35_747,X44_749,X58_750,X59_746,X42_748,X57_751] :
( ~ p3(X44_749,X35_747)
| p21(f5(X58_750,X59_746),X35_747)
| ~ p3(X57_751,X44_749)
| ~ p3(X57_751,X59_746)
| ~ p2(f7(f10(c24,f12(c25,c26)),X42_748),X58_750) ),
inference(resolution,[status(thm)],[c_62,c_627]) ).
tff(c_1418,plain,
! [X57_754,X46_752,X59_756,X58_753,X42_755] :
( p21(f5(X58_753,X59_756),X46_752)
| ~ p3(X57_754,X46_752)
| ~ p3(X57_754,X59_756)
| ~ p2(f7(f10(c24,f12(c25,c26)),X42_755),X58_753) ),
inference(resolution,[status(thm)],[c_12,c_1402]) ).
tff(c_1434,plain,
! [X58_757,X59_758,X46_759,X42_760] :
( p21(f5(X58_757,X59_758),X46_759)
| ~ p3(X46_759,X59_758)
| ~ p2(f7(f10(c24,f12(c25,c26)),X42_760),X58_757) ),
inference(resolution,[status(thm)],[c_12,c_1418]) ).
tff(c_1447,plain,
! [X42_761,X59_762,X46_763] :
( p21(f5(f7(f10(c24,f12(c25,c26)),X42_761),X59_762),X46_763)
| ~ p3(X46_763,X59_762) ),
inference(resolution,[status(thm)],[c_14,c_1434]) ).
tff(c_70,plain,
! [X77_87] :
( ~ p21(f5(f7(f10(c24,f12(c25,c26)),c22),X77_87),c27)
| ~ p21(f5(c22,c23),X77_87) ),
inference(cnfTransformation,[status(thm)],[f_223]) ).
tff(c_1468,plain,
! [X59_762] :
( ~ p21(f5(c22,c23),X59_762)
| ~ p3(c27,X59_762) ),
inference(resolution,[status(thm)],[c_1447,c_70]) ).
tff(c_16372,plain,
~ p3(c27,c27),
inference(resolution,[status(thm)],[c_16349,c_1468]) ).
tff(c_16393,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_12,c_16372]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.15 % Problem : SYN632-1 : TPTP v9.0.0. Released v2.5.0.
% 0.09/0.16 % 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.37 % Computer : n019.cluster.edu
% 0.15/0.37 % Model : x86_64 x86_64
% 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.37 % Memory : 8042.1875MB
% 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.37 % CPULimit : 300
% 0.15/0.37 % WCLimit : 300
% 0.15/0.37 % DateTime : Wed Apr 9 08:06:02 EDT 2025
% 0.15/0.37 % CPUTime :
% 16.77/6.13 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 16.77/6.13
% 16.77/6.13 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------