%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYN714-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 : n009.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 21.71s 9.22s
% Output : CNFRefutation 21.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 8
% Syntax : Number of formulae : 23 ( 12 unt; 0 typ; 0 def)
% Number of atoms : 46 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 50 ( 27 ~; 23 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 33 ( 32 usr; 1 prp; 0-3 aty)
% Number of functors : 35 ( 35 usr; 11 con; 0-3 aty)
% Number of variables : 17 ( 17 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ p50 > p7 > p57 > p56 > p55 > p54 > p53 > p52 > p51 > p5 > p49 > p46 > p45 > p42 > p40 > p36 > p33 > p32 > p30 > p3 > p28 > p26 > p24 > p23 > p2 > p19 > p18 > p16 > p15 > p10 > p48 > p47 > f44 > f43 > f22 > f9 > f8 > f6 > f35 > f34 > f29 > f27 > f25 > f21 > f13 > #nlpp > f41 > f4 > f39 > f38 > f37 > f31 > f20 > f17 > f14 > f12 > f11 > c68 > c67 > c66 > c65 > c64 > c63 > c62 > c61 > c60 > c59 > c58
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(f43,type,
f43: ( $i * $i * $i ) > $i ).
tff(c61,type,
c61: $i ).
tff(f12,type,
f12: $i > $i ).
tff(p32,type,
p32: ( $i * $i ) > $o ).
tff(p15,type,
p15: ( $i * $i ) > $o ).
tff(c64,type,
c64: $i ).
tff(p46,type,
p46: ( $i * $i ) > $o ).
tff(p23,type,
p23: ( $i * $i ) > $o ).
tff(p51,type,
p51: ( $i * $i ) > $o ).
tff(p57,type,
p57: ( $i * $i ) > $o ).
tff(p50,type,
p50: ( $i * $i * $i ) > $o ).
tff(c66,type,
c66: $i ).
tff(c58,type,
c58: $i ).
tff(p16,type,
p16: ( $i * $i ) > $o ).
tff(f13,type,
f13: ( $i * $i ) > $i ).
tff(f9,type,
f9: ( $i * $i ) > $i ).
tff(f17,type,
f17: $i > $i ).
tff(p2,type,
p2: ( $i * $i ) > $o ).
tff(f14,type,
f14: $i > $i ).
tff(f20,type,
f20: $i > $i ).
tff(p47,type,
p47: $i > $o ).
tff(p53,type,
p53: ( $i * $i ) > $o ).
tff(f44,type,
f44: ( $i * $i * $i ) > $i ).
tff(f38,type,
f38: $i > $i ).
tff(p42,type,
p42: ( $i * $i ) > $o ).
tff(p56,type,
p56: ( $i * $i ) > $o ).
tff(p33,type,
p33: ( $i * $i ) > $o ).
tff(f31,type,
f31: $i > $i ).
tff(f22,type,
f22: ( $i * $i * $i ) > $i ).
tff(p5,type,
p5: ( $i * $i ) > $o ).
tff(c63,type,
c63: $i ).
tff(p52,type,
p52: ( $i * $i ) > $o ).
tff(p54,type,
p54: ( $i * $i ) > $o ).
tff(f35,type,
f35: ( $i * $i ) > $i ).
tff(p45,type,
p45: ( $i * $i ) > $o ).
tff(p3,type,
p3: ( $i * $i ) > $o ).
tff(f8,type,
f8: ( $i * $i ) > $i ).
tff(p30,type,
p30: ( $i * $i ) > $o ).
tff(p19,type,
p19: ( $i * $i ) > $o ).
tff(c67,type,
c67: $i ).
tff(p24,type,
p24: ( $i * $i ) > $o ).
tff(c68,type,
c68: $i ).
tff(p48,type,
p48: $i > $o ).
tff(p40,type,
p40: ( $i * $i ) > $o ).
tff(p10,type,
p10: ( $i * $i ) > $o ).
tff(f4,type,
f4: $i > $i ).
tff(p36,type,
p36: ( $i * $i ) > $o ).
tff(f27,type,
f27: ( $i * $i ) > $i ).
tff(f39,type,
f39: $i > $i ).
tff(f41,type,
f41: $i > $i ).
tff(p28,type,
p28: ( $i * $i ) > $o ).
tff(f29,type,
f29: ( $i * $i ) > $i ).
tff(p26,type,
p26: ( $i * $i ) > $o ).
tff(f21,type,
f21: ( $i * $i ) > $i ).
tff(p7,type,
p7: ( $i * $i ) > $o ).
tff(c65,type,
c65: $i ).
tff(c60,type,
c60: $i ).
tff(f11,type,
f11: $i > $i ).
tff(f34,type,
f34: ( $i * $i ) > $i ).
tff(p55,type,
p55: ( $i * $i ) > $o ).
tff(p18,type,
p18: ( $i * $i ) > $o ).
tff(f6,type,
f6: ( $i * $i ) > $i ).
tff(c62,type,
c62: $i ).
tff(c59,type,
c59: $i ).
tff(f37,type,
f37: $i > $i ).
tff(p49,type,
p49: ( $i * $i ) > $o ).
tff(f25,type,
f25: ( $i * $i ) > $i ).
tff(f_62,axiom,
p51(c66,c67),
file(unknown,unknown) ).
tff(f_63,axiom,
p53(c68,f17(c66)),
file(unknown,unknown) ).
tff(f_512,axiom,
! [X165,X166,X167,X168] :
( p51(X165,f25(f27(X166,X167),X168))
| ~ p51(X165,X168)
| ~ p53(X167,f17(X165)) ),
file(unknown,unknown) ).
tff(f_301,axiom,
! [X160] :
( p50(c66,f25(f27(c59,X160),c67),c62)
| ~ p53(X160,f17(c66)) ),
file(unknown,unknown) ).
tff(f_65,axiom,
~ p16(f17(c66),c65),
file(unknown,unknown) ).
tff(f_69,axiom,
p52(f20(f21(c62,c64)),c66),
file(unknown,unknown) ).
tff(f_627,axiom,
! [X15,X16] :
( p16(f17(X15),c65)
| p50(X15,X16,c60)
| ~ p51(X15,X16)
| ~ p50(X15,X16,c62)
| ~ p52(f20(f21(c62,c64)),X15) ),
file(unknown,unknown) ).
tff(f_89,axiom,
~ p50(c66,f25(f27(c59,c68),c67),c60),
file(unknown,unknown) ).
tff(c_44,plain,
p51(c66,c67),
inference(cnfTransformation,[status(thm)],[f_62]) ).
tff(c_46,plain,
p53(c68,f17(c66)),
inference(cnfTransformation,[status(thm)],[f_63]) ).
tff(c_174,plain,
! [X167_192,X165_190,X168_193,X166_191] :
( ~ p53(X167_192,f17(X165_190))
| ~ p51(X165_190,X168_193)
| p51(X165_190,f25(f27(X166_191,X167_192),X168_193)) ),
inference(cnfTransformation,[status(thm)],[f_512]) ).
tff(c_128,plain,
! [X160_103] :
( ~ p53(X160_103,f17(c66))
| p50(c66,f25(f27(c59,X160_103),c67),c62) ),
inference(cnfTransformation,[status(thm)],[f_301]) ).
tff(c_48,plain,
~ p16(f17(c66),c65),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_56,plain,
p52(f20(f21(c62,c64)),c66),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_3760,plain,
! [X15_806,X16_807] :
( ~ p52(f20(f21(c62,c64)),X15_806)
| ~ p50(X15_806,X16_807,c62)
| ~ p51(X15_806,X16_807)
| p50(X15_806,X16_807,c60)
| p16(f17(X15_806),c65) ),
inference(cnfTransformation,[status(thm)],[f_627]) ).
tff(c_3768,plain,
! [X16_807] :
( ~ p50(c66,X16_807,c62)
| ~ p51(c66,X16_807)
| p50(c66,X16_807,c60)
| p16(f17(c66),c65) ),
inference(resolution,[status(thm)],[c_56,c_3760]) ).
tff(c_3780,plain,
! [X16_808] :
( ~ p50(c66,X16_808,c62)
| ~ p51(c66,X16_808)
| p50(c66,X16_808,c60) ),
inference(negUnitSimplification,[status(thm)],[c_48,c_3768]) ).
tff(c_37675,plain,
! [X160_2040] :
( ~ p51(c66,f25(f27(c59,X160_2040),c67))
| p50(c66,f25(f27(c59,X160_2040),c67),c60)
| ~ p53(X160_2040,f17(c66)) ),
inference(resolution,[status(thm)],[c_128,c_3780]) ).
tff(c_66,plain,
~ p50(c66,f25(f27(c59,c68),c67),c60),
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_37680,plain,
( ~ p51(c66,f25(f27(c59,c68),c67))
| ~ p53(c68,f17(c66)) ),
inference(resolution,[status(thm)],[c_37675,c_66]) ).
tff(c_37684,plain,
~ p51(c66,f25(f27(c59,c68),c67)),
inference(demodulation,[status(thm),theory(equality)],[c_46,c_37680]) ).
tff(c_37687,plain,
( ~ p53(c68,f17(c66))
| ~ p51(c66,c67) ),
inference(resolution,[status(thm)],[c_174,c_37684]) ).
tff(c_37694,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_44,c_46,c_37687]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.13 % Problem : SYN714-1 : TPTP v9.0.0. Released v2.5.0.
% 0.13/0.14 % 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.14/0.35 % Computer : n009.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed Apr 9 08:11:41 EDT 2025
% 0.14/0.35 % CPUTime :
% 21.71/9.22 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 21.71/9.22
% 21.71/9.22 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------