%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYN715-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/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 : n015.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:16 PM UTC 2025
% Result : Unsatisfiable 77.87s 62.15s
% Output : CNFRefutation 77.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 10
% Syntax : Number of formulae : 29 ( 14 unt; 0 typ; 0 def)
% Number of atoms : 52 ( 0 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 49 ( 26 ~; 23 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 36 ( 35 usr; 1 prp; 0-2 aty)
% Number of functors : 40 ( 40 usr; 13 con; 0-2 aty)
% Number of variables : 65 ( 65 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ p9 > p7 > p63 > p62 > p60 > p6 > p58 > p56 > p54 > p52 > p50 > p48 > p46 > p44 > p42 > p40 > p4 > p38 > p36 > p34 > p32 > p3 > p29 > p27 > p25 > p23 > p22 > p20 > p2 > p18 > p17 > p15 > p14 > p12 > p10 > f8 > f61 > f59 > f57 > f55 > f53 > f51 > f5 > f49 > f47 > f45 > f43 > f41 > f39 > f37 > f35 > f33 > f31 > f30 > f28 > f26 > f24 > f21 > f19 > f16 > f13 > f11 > #nlpp > c76 > c75 > c74 > c73 > c72 > c71 > c70 > c69 > c68 > c67 > c66 > c65 > c64
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(p32,type,
p32: ( $i * $i ) > $o ).
tff(f11,type,
f11: ( $i * $i ) > $i ).
tff(f5,type,
f5: ( $i * $i ) > $i ).
tff(f61,type,
f61: ( $i * $i ) > $i ).
tff(p15,type,
p15: ( $i * $i ) > $o ).
tff(p4,type,
p4: ( $i * $i ) > $o ).
tff(f45,type,
f45: ( $i * $i ) > $i ).
tff(c69,type,
c69: $i ).
tff(f26,type,
f26: ( $i * $i ) > $i ).
tff(p38,type,
p38: ( $i * $i ) > $o ).
tff(c64,type,
c64: $i ).
tff(p46,type,
p46: ( $i * $i ) > $o ).
tff(p23,type,
p23: ( $i * $i ) > $o ).
tff(f19,type,
f19: ( $i * $i ) > $i ).
tff(p58,type,
p58: ( $i * $i ) > $o ).
tff(p22,type,
p22: ( $i * $i ) > $o ).
tff(f39,type,
f39: ( $i * $i ) > $i ).
tff(c76,type,
c76: $i ).
tff(c66,type,
c66: $i ).
tff(f59,type,
f59: ( $i * $i ) > $i ).
tff(f13,type,
f13: ( $i * $i ) > $i ).
tff(p2,type,
p2: ( $i * $i ) > $o ).
tff(p48,type,
p48: ( $i * $i ) > $o ).
tff(c72,type,
c72: $i ).
tff(p60,type,
p60: ( $i * $i ) > $o ).
tff(f24,type,
f24: ( $i * $i ) > $i ).
tff(p29,type,
p29: ( $i * $i ) > $o ).
tff(p20,type,
p20: ( $i * $i ) > $o ).
tff(c71,type,
c71: $i ).
tff(p50,type,
p50: ( $i * $i ) > $o ).
tff(p17,type,
p17: ( $i * $i ) > $o ).
tff(f30,type,
f30: ( $i * $i ) > $i ).
tff(p63,type,
p63: ( $i * $i ) > $o ).
tff(p42,type,
p42: ( $i * $i ) > $o ).
tff(p56,type,
p56: ( $i * $i ) > $o ).
tff(c73,type,
c73: $i ).
tff(f55,type,
f55: ( $i * $i ) > $i ).
tff(f51,type,
f51: ( $i * $i ) > $i ).
tff(p52,type,
p52: ( $i * $i ) > $o ).
tff(p27,type,
p27: ( $i * $i ) > $o ).
tff(p54,type,
p54: ( $i * $i ) > $o ).
tff(f35,type,
f35: ( $i * $i ) > $i ).
tff(f28,type,
f28: ( $i * $i ) > $i ).
tff(p3,type,
p3: ( $i * $i ) > $o ).
tff(f31,type,
f31: ( $i * $i ) > $i ).
tff(p44,type,
p44: ( $i * $i ) > $o ).
tff(f8,type,
f8: ( $i * $i ) > $i ).
tff(f47,type,
f47: ( $i * $i ) > $i ).
tff(f57,type,
f57: ( $i * $i ) > $i ).
tff(c67,type,
c67: $i ).
tff(p25,type,
p25: ( $i * $i ) > $o ).
tff(p14,type,
p14: ( $i * $i ) > $o ).
tff(c68,type,
c68: $i ).
tff(c75,type,
c75: $i ).
tff(p40,type,
p40: ( $i * $i ) > $o ).
tff(p62,type,
p62: ( $i * $i ) > $o ).
tff(p10,type,
p10: ( $i * $i ) > $o ).
tff(f33,type,
f33: ( $i * $i ) > $i ).
tff(f43,type,
f43: ( $i * $i ) > $i ).
tff(c74,type,
c74: $i ).
tff(f16,type,
f16: ( $i * $i ) > $i ).
tff(p6,type,
p6: ( $i * $i ) > $o ).
tff(f53,type,
f53: ( $i * $i ) > $i ).
tff(p36,type,
p36: ( $i * $i ) > $o ).
tff(c70,type,
c70: $i ).
tff(f21,type,
f21: ( $i * $i ) > $i ).
tff(p7,type,
p7: ( $i * $i ) > $o ).
tff(f49,type,
f49: ( $i * $i ) > $i ).
tff(f37,type,
f37: ( $i * $i ) > $i ).
tff(c65,type,
c65: $i ).
tff(f41,type,
f41: ( $i * $i ) > $i ).
tff(p34,type,
p34: ( $i * $i ) > $o ).
tff(p12,type,
p12: ( $i * $i ) > $o ).
tff(p9,type,
p9: ( $i * $i ) > $o ).
tff(p18,type,
p18: ( $i * $i ) > $o ).
tff(f_374,axiom,
p63(f24(f26(f30(c73,f31(c68,c72)),f28(c69,c72)),c70),c71),
file(unknown,unknown) ).
tff(f_616,axiom,
! [X211,X212,X213,X214] :
( p63(f24(f26(f30(c73,X211),X212),X213),X214)
| ~ p63(f24(f26(f30(c73,X213),X214),X211),X212) ),
file(unknown,unknown) ).
tff(f_77,axiom,
! [X44] : p2(X44,X44),
file(unknown,unknown) ).
tff(f_634,axiom,
! [X9,X7,X11,X8,X10] : p3(f8(f11(f13(c65,f16(f19(f21(c66,X7),X8),X9)),X10),X11),f16(f19(f21(c66,f33(f35(f37(f39(f41(c74,X7),X8),X9),X10),X11)),f43(f45(f47(f49(f51(c75,X7),X8),X9),X10),X11)),f53(f55(f57(f59(f61(c76,X7),X8),X9),X10),X11))),
file(unknown,unknown) ).
tff(f_510,axiom,
! [X123,X124,X125,X126] :
( p4(f5(X123,X124),f5(X125,X126))
| ~ p2(X123,X125)
| ~ p3(X124,X126) ),
file(unknown,unknown) ).
tff(f_606,axiom,
p62(f5(c64,f8(f11(f13(c65,f16(f19(f21(c66,c67),c68),c69)),c70),c71)),c72),
file(unknown,unknown) ).
tff(f_67,axiom,
! [X71] : p27(X71,X71),
file(unknown,unknown) ).
tff(f_362,axiom,
! [X199,X200,X202,X201] :
( p62(X199,X200)
| ~ p4(X202,X199)
| ~ p62(X202,X201)
| ~ p27(X201,X200) ),
file(unknown,unknown) ).
tff(f_595,axiom,
! [X203,X204,X205,X206] :
( p62(X203,X204)
| ~ p62(f5(c64,f16(f19(f21(c66,X203),X205),X206)),X204) ),
file(unknown,unknown) ).
tff(f_622,axiom,
! [X9,X12,X7,X11,X8,X10] :
( ~ p63(f24(f26(f30(c73,X10),X11),f31(X8,X12)),f28(X9,X12))
| ~ p62(f33(f35(f37(f39(f41(c74,X7),X8),X9),X10),X11),X12) ),
file(unknown,unknown) ).
tff(c_138,plain,
p63(f24(f26(f30(c73,f31(c68,c72)),f28(c69,c72)),c70),c71),
inference(cnfTransformation,[status(thm)],[f_374]) ).
tff(c_907,plain,
! [X213_708,X214_709,X211_710,X212_711] :
( ~ p63(f24(f26(f30(c73,X213_708),X214_709),X211_710),X212_711)
| p63(f24(f26(f30(c73,X211_710),X212_711),X213_708),X214_709) ),
inference(cnfTransformation,[status(thm)],[f_616]) ).
tff(c_910,plain,
p63(f24(f26(f30(c73,c70),c71),f31(c68,c72)),f28(c69,c72)),
inference(resolution,[status(thm)],[c_138,c_907]) ).
tff(c_56,plain,
! [X44_28] : p2(X44_28,X44_28),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_212,plain,
! [X7_290,X9_289,X11_291,X10_293,X8_292] : p3(f8(f11(f13(c65,f16(f19(f21(c66,X7_290),X8_292),X9_289)),X10_293),X11_291),f16(f19(f21(c66,f33(f35(f37(f39(f41(c74,X7_290),X8_292),X9_289),X10_293),X11_291)),f43(f45(f47(f49(f51(c75,X7_290),X8_292),X9_289),X10_293),X11_291)),f53(f55(f57(f59(f61(c76,X7_290),X8_292),X9_289),X10_293),X11_291))),
inference(cnfTransformation,[status(thm)],[f_634]) ).
tff(c_172,plain,
! [X124_206,X126_208,X123_205,X125_207] :
( ~ p3(X124_206,X126_208)
| ~ p2(X123_205,X125_207)
| p4(f5(X123_205,X124_206),f5(X125_207,X126_208)) ),
inference(cnfTransformation,[status(thm)],[f_510]) ).
tff(c_200,plain,
p62(f5(c64,f8(f11(f13(c65,f16(f19(f21(c66,c67),c68),c69)),c70),c71)),c72),
inference(cnfTransformation,[status(thm)],[f_606]) ).
tff(c_46,plain,
! [X71_23] : p27(X71_23,X71_23),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_551,plain,
! [X201_499,X200_500,X202_501,X199_502] :
( ~ p27(X201_499,X200_500)
| ~ p62(X202_501,X201_499)
| ~ p4(X202_501,X199_502)
| p62(X199_502,X200_500) ),
inference(cnfTransformation,[status(thm)],[f_362]) ).
tff(c_554,plain,
! [X202_501,X71_23,X199_502] :
( ~ p62(X202_501,X71_23)
| ~ p4(X202_501,X199_502)
| p62(X199_502,X71_23) ),
inference(resolution,[status(thm)],[c_46,c_551]) ).
tff(c_2287,plain,
! [X199_1382] :
( ~ p4(f5(c64,f8(f11(f13(c65,f16(f19(f21(c66,c67),c68),c69)),c70),c71)),X199_1382)
| p62(X199_1382,c72) ),
inference(resolution,[status(thm)],[c_200,c_554]) ).
tff(c_4448,plain,
! [X125_2371,X126_2372] :
( p62(f5(X125_2371,X126_2372),c72)
| ~ p3(f8(f11(f13(c65,f16(f19(f21(c66,c67),c68),c69)),c70),c71),X126_2372)
| ~ p2(c64,X125_2371) ),
inference(resolution,[status(thm)],[c_172,c_2287]) ).
tff(c_104161,plain,
! [X125_21425] :
( p62(f5(X125_21425,f16(f19(f21(c66,f33(f35(f37(f39(f41(c74,c67),c68),c69),c70),c71)),f43(f45(f47(f49(f51(c75,c67),c68),c69),c70),c71)),f53(f55(f57(f59(f61(c76,c67),c68),c69),c70),c71))),c72)
| ~ p2(c64,X125_21425) ),
inference(resolution,[status(thm)],[c_212,c_4448]) ).
tff(c_194,plain,
! [X203_249,X205_251,X206_252,X204_250] :
( ~ p62(f5(c64,f16(f19(f21(c66,X203_249),X205_251),X206_252)),X204_250)
| p62(X203_249,X204_250) ),
inference(cnfTransformation,[status(thm)],[f_595]) ).
tff(c_104177,plain,
( p62(f33(f35(f37(f39(f41(c74,c67),c68),c69),c70),c71),c72)
| ~ p2(c64,c64) ),
inference(resolution,[status(thm)],[c_104161,c_194]) ).
tff(c_104188,plain,
p62(f33(f35(f37(f39(f41(c74,c67),c68),c69),c70),c71),c72),
inference(demodulation,[status(thm),theory(equality)],[c_56,c_104177]) ).
tff(c_206,plain,
! [X8_275,X11_274,X7_273,X12_272,X10_276,X9_271] :
( ~ p62(f33(f35(f37(f39(f41(c74,X7_273),X8_275),X9_271),X10_276),X11_274),X12_272)
| ~ p63(f24(f26(f30(c73,X10_276),X11_274),f31(X8_275,X12_272)),f28(X9_271,X12_272)) ),
inference(cnfTransformation,[status(thm)],[f_622]) ).
tff(c_104221,plain,
~ p63(f24(f26(f30(c73,c70),c71),f31(c68,c72)),f28(c69,c72)),
inference(resolution,[status(thm)],[c_104188,c_206]) ).
tff(c_104247,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_910,c_104221]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SYN715-1 : TPTP v9.0.0. Released v2.5.0.
% 0.04/0.14 % 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.13/0.35 % Computer : n015.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed Apr 9 08:11:50 EDT 2025
% 0.13/0.35 % CPUTime :
% 77.87/62.15 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 77.92/62.16
% 77.92/62.16 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------