%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYN712-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 : n026.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:15 PM UTC 2025
% Result : Unsatisfiable 85.00s 64.28s
% Output : CNFRefutation 85.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 14
% Syntax : Number of formulae : 41 ( 19 unt; 0 typ; 0 def)
% Number of atoms : 76 ( 0 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 73 ( 38 ~; 35 |; 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 : 94 ( 94 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ p9 > p7 > p63 > p62 > p60 > p6 > p58 > p56 > p54 > p52 > p50 > p48 > p46 > p44 > p42 > p40 > p4 > p38 > p35 > p34 > p32 > p30 > p3 > p28 > p26 > p24 > p22 > p20 > p2 > p18 > p17 > p15 > p14 > p12 > p10 > f8 > f61 > f59 > f57 > f55 > f53 > f51 > f5 > f49 > f47 > f45 > f43 > f41 > f39 > f37 > f36 > f33 > f31 > f29 > f27 > f25 > f23 > 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(p38,type,
p38: ( $i * $i ) > $o ).
tff(c64,type,
c64: $i ).
tff(p46,type,
p46: ( $i * $i ) > $o ).
tff(f19,type,
f19: ( $i * $i ) > $i ).
tff(f36,type,
f36: ( $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(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(p63,type,
p63: ( $i * $i ) > $o ).
tff(p42,type,
p42: ( $i * $i ) > $o ).
tff(p35,type,
p35: ( $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(p54,type,
p54: ( $i * $i ) > $o ).
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(p30,type,
p30: ( $i * $i ) > $o ).
tff(c67,type,
c67: $i ).
tff(p14,type,
p14: ( $i * $i ) > $o ).
tff(p24,type,
p24: ( $i * $i ) > $o ).
tff(c68,type,
c68: $i ).
tff(c75,type,
c75: $i ).
tff(f23,type,
f23: ( $i * $i ) > $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(f27,type,
f27: ( $i * $i ) > $i ).
tff(p28,type,
p28: ( $i * $i ) > $o ).
tff(c70,type,
c70: $i ).
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(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(f25,type,
f25: ( $i * $i ) > $i ).
tff(f_601,axiom,
! [X203,X205,X206,X204] :
( p62(f5(c64,f8(f11(f13(c65,X203),X205),X206)),X204)
| ~ p62(X203,X204) ),
file(unknown,unknown) ).
tff(f_353,axiom,
~ p62(f5(c64,f8(f11(f13(c65,c66),c67),c68)),c69),
file(unknown,unknown) ).
tff(f_77,axiom,
! [X44] : p2(X44,X44),
file(unknown,unknown) ).
tff(f_625,axiom,
! [X27,X24,X28,X26,X25] : p3(f16(f19(f21(c70,f8(f11(f13(c65,X24),X25),X26)),X27),X28),f8(f11(f13(c65,f23(f25(f27(f29(f31(c74,X24),X25),X26),X27),X28)),f43(f45(f47(f49(f51(c75,X24),X25),X26),X27),X28)),f53(f55(f57(f59(f61(c76,X24),X25),X26),X27),X28))),
file(unknown,unknown) ).
tff(f_65,axiom,
! [X78] : p3(X78,X78),
file(unknown,unknown) ).
tff(f_263,axiom,
! [X79,X80,X78] :
( p3(X79,X80)
| ~ p3(X78,X79)
| ~ p3(X78,X80) ),
file(unknown,unknown) ).
tff(f_479,axiom,
! [X123,X124,X125,X126] :
( p4(f5(X123,X124),f5(X125,X126))
| ~ p2(X123,X125)
| ~ p3(X124,X126) ),
file(unknown,unknown) ).
tff(f_53,axiom,
! [X116] : p4(X116,X116),
file(unknown,unknown) ).
tff(f_215,axiom,
! [X117,X118,X116] :
( p4(X117,X118)
| ~ p4(X116,X117)
| ~ p4(X116,X118) ),
file(unknown,unknown) ).
tff(f_607,axiom,
p62(f5(c64,f16(f19(f21(c70,f8(f11(f13(c65,c66),c67),c68)),c71),c72)),c69),
file(unknown,unknown) ).
tff(f_61,axiom,
! [X92] : p32(X92,X92),
file(unknown,unknown) ).
tff(f_375,axiom,
! [X199,X200,X202,X201] :
( p62(X199,X200)
| ~ p4(X202,X199)
| ~ p62(X202,X201)
| ~ p32(X201,X200) ),
file(unknown,unknown) ).
tff(f_596,axiom,
! [X203,X204,X205,X206] :
( p62(X203,X204)
| ~ p62(f5(c64,f8(f11(f13(c65,X203),X205),X206)),X204) ),
file(unknown,unknown) ).
tff(f_606,axiom,
! [X27,X29,X24,X28,X26,X25] :
( p62(X24,X29)
| ~ p62(f23(f25(f27(f29(f31(c74,X24),X25),X26),X27),X28),X29) ),
file(unknown,unknown) ).
tff(c_791,plain,
! [X203_638,X204_639,X205_640,X206_641] :
( ~ p62(X203_638,X204_639)
| p62(f5(c64,f8(f11(f13(c65,X203_638),X205_640),X206_641)),X204_639) ),
inference(cnfTransformation,[status(thm)],[f_601]) ).
tff(c_134,plain,
~ p62(f5(c64,f8(f11(f13(c65,c66),c67),c68)),c69),
inference(cnfTransformation,[status(thm)],[f_353]) ).
tff(c_802,plain,
~ p62(c66,c69),
inference(resolution,[status(thm)],[c_791,c_134]) ).
tff(c_56,plain,
! [X44_28] : p2(X44_28,X44_28),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_1001,plain,
! [X27_762,X28_763,X26_761,X24_764,X25_765] : p3(f16(f19(f21(c70,f8(f11(f13(c65,X24_764),X25_765),X26_761)),X27_762),X28_763),f8(f11(f13(c65,f23(f25(f27(f29(f31(c74,X24_764),X25_765),X26_761),X27_762),X28_763)),f43(f45(f47(f49(f51(c75,X24_764),X25_765),X26_761),X27_762),X28_763)),f53(f55(f57(f59(f61(c76,X24_764),X25_765),X26_761),X27_762),X28_763))),
inference(cnfTransformation,[status(thm)],[f_625]) ).
tff(c_44,plain,
! [X78_22] : p3(X78_22,X78_22),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_521,plain,
! [X78_474,X80_475,X79_476] :
( ~ p3(X78_474,X80_475)
| ~ p3(X78_474,X79_476)
| p3(X79_476,X80_475) ),
inference(cnfTransformation,[status(thm)],[f_263]) ).
tff(c_524,plain,
! [X78_22,X79_476] :
( ~ p3(X78_22,X79_476)
| p3(X79_476,X78_22) ),
inference(resolution,[status(thm)],[c_44,c_521]) ).
tff(c_1006,plain,
! [X27_762,X28_763,X26_761,X24_764,X25_765] : p3(f8(f11(f13(c65,f23(f25(f27(f29(f31(c74,X24_764),X25_765),X26_761),X27_762),X28_763)),f43(f45(f47(f49(f51(c75,X24_764),X25_765),X26_761),X27_762),X28_763)),f53(f55(f57(f59(f61(c76,X24_764),X25_765),X26_761),X27_762),X28_763)),f16(f19(f21(c70,f8(f11(f13(c65,X24_764),X25_765),X26_761)),X27_762),X28_763)),
inference(resolution,[status(thm)],[c_1001,c_524]) ).
tff(c_668,plain,
! [X124_566,X126_567,X123_568,X125_569] :
( ~ p3(X124_566,X126_567)
| ~ p2(X123_568,X125_569)
| p4(f5(X123_568,X124_566),f5(X125_569,X126_567)) ),
inference(cnfTransformation,[status(thm)],[f_479]) ).
tff(c_32,plain,
! [X116_16] : p4(X116_16,X116_16),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_476,plain,
! [X116_449,X118_450,X117_451] :
( ~ p4(X116_449,X118_450)
| ~ p4(X116_449,X117_451)
| p4(X117_451,X118_450) ),
inference(cnfTransformation,[status(thm)],[f_215]) ).
tff(c_479,plain,
! [X116_16,X117_451] :
( ~ p4(X116_16,X117_451)
| p4(X117_451,X116_16) ),
inference(resolution,[status(thm)],[c_32,c_476]) ).
tff(c_673,plain,
! [X125_569,X126_567,X123_568,X124_566] :
( p4(f5(X125_569,X126_567),f5(X123_568,X124_566))
| ~ p3(X124_566,X126_567)
| ~ p2(X123_568,X125_569) ),
inference(resolution,[status(thm)],[c_668,c_479]) ).
tff(c_200,plain,
p62(f5(c64,f16(f19(f21(c70,f8(f11(f13(c65,c66),c67),c68)),c71),c72)),c69),
inference(cnfTransformation,[status(thm)],[f_607]) ).
tff(c_40,plain,
! [X92_20] : p32(X92_20,X92_20),
inference(cnfTransformation,[status(thm)],[f_61]) ).
tff(c_539,plain,
! [X201_484,X200_485,X202_486,X199_487] :
( ~ p32(X201_484,X200_485)
| ~ p62(X202_486,X201_484)
| ~ p4(X202_486,X199_487)
| p62(X199_487,X200_485) ),
inference(cnfTransformation,[status(thm)],[f_375]) ).
tff(c_542,plain,
! [X202_486,X92_20,X199_487] :
( ~ p62(X202_486,X92_20)
| ~ p4(X202_486,X199_487)
| p62(X199_487,X92_20) ),
inference(resolution,[status(thm)],[c_40,c_539]) ).
tff(c_2274,plain,
! [X199_1379] :
( ~ p4(f5(c64,f16(f19(f21(c70,f8(f11(f13(c65,c66),c67),c68)),c71),c72)),X199_1379)
| p62(X199_1379,c69) ),
inference(resolution,[status(thm)],[c_200,c_542]) ).
tff(c_4194,plain,
! [X123_2274,X124_2275] :
( p62(f5(X123_2274,X124_2275),c69)
| ~ p3(X124_2275,f16(f19(f21(c70,f8(f11(f13(c65,c66),c67),c68)),c71),c72))
| ~ p2(X123_2274,c64) ),
inference(resolution,[status(thm)],[c_673,c_2274]) ).
tff(c_93675,plain,
! [X123_20651] :
( p62(f5(X123_20651,f8(f11(f13(c65,f23(f25(f27(f29(f31(c74,c66),c67),c68),c71),c72)),f43(f45(f47(f49(f51(c75,c66),c67),c68),c71),c72)),f53(f55(f57(f59(f61(c76,c66),c67),c68),c71),c72))),c69)
| ~ p2(X123_20651,c64) ),
inference(resolution,[status(thm)],[c_1006,c_4194]) ).
tff(c_194,plain,
! [X203_249,X205_251,X206_252,X204_250] :
( ~ p62(f5(c64,f8(f11(f13(c65,X203_249),X205_251),X206_252)),X204_250)
| p62(X203_249,X204_250) ),
inference(cnfTransformation,[status(thm)],[f_596]) ).
tff(c_93691,plain,
( p62(f23(f25(f27(f29(f31(c74,c66),c67),c68),c71),c72),c69)
| ~ p2(c64,c64) ),
inference(resolution,[status(thm)],[c_93675,c_194]) ).
tff(c_93702,plain,
p62(f23(f25(f27(f29(f31(c74,c66),c67),c68),c71),c72),c69),
inference(demodulation,[status(thm),theory(equality)],[c_56,c_93691]) ).
tff(c_198,plain,
! [X29_258,X26_261,X25_262,X28_260,X24_259,X27_257] :
( ~ p62(f23(f25(f27(f29(f31(c74,X24_259),X25_262),X26_261),X27_257),X28_260),X29_258)
| p62(X24_259,X29_258) ),
inference(cnfTransformation,[status(thm)],[f_606]) ).
tff(c_93736,plain,
p62(c66,c69),
inference(resolution,[status(thm)],[c_93702,c_198]) ).
tff(c_93757,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_802,c_93736]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.09 % Problem : SYN712-1 : TPTP v9.0.0. Released v2.5.0.
% 0.04/0.10 % 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.09/0.30 % Computer : n026.cluster.edu
% 0.09/0.30 % Model : x86_64 x86_64
% 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.30 % Memory : 8042.1875MB
% 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.30 % CPULimit : 300
% 0.09/0.30 % WCLimit : 300
% 0.09/0.30 % DateTime : Wed Apr 9 08:11:53 EDT 2025
% 0.09/0.30 % CPUTime :
% 85.00/64.28 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 85.00/64.29
% 85.00/64.29 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------