%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYN709-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 : n005.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 164.43s 135.48s
% Output : CNFRefutation 164.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 9
% Syntax : Number of formulae : 25 ( 11 unt; 0 typ; 0 def)
% Number of atoms : 52 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 57 ( 30 ~; 27 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 31 ( 30 usr; 1 prp; 0-2 aty)
% Number of functors : 37 ( 37 usr; 21 con; 0-2 aty)
% Number of variables : 49 ( 49 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ p9 > p7 > p6 > p47 > p46 > p45 > p44 > p42 > p40 > p4 > p38 > p36 > p35 > p32 > p30 > p3 > p29 > p27 > p26 > p24 > p22 > p21 > p2 > p19 > p18 > p16 > p15 > p13 > p11 > p10 > f8 > f5 > f43 > f41 > f39 > f37 > f34 > f33 > f31 > f28 > f25 > f23 > f20 > f17 > f14 > f12 > #nlpp > c68 > c67 > c66 > c65 > c64 > c63 > c62 > c61 > c60 > c59 > c58 > c57 > c56 > c55 > c54 > c53 > c52 > c51 > c50 > c49 > c48
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(c61,type,
c61: $i ).
tff(p32,type,
p32: ( $i * $i ) > $o ).
tff(f5,type,
f5: ( $i * $i ) > $i ).
tff(p15,type,
p15: ( $i * $i ) > $o ).
tff(c57,type,
c57: $i ).
tff(p4,type,
p4: ( $i * $i ) > $o ).
tff(p38,type,
p38: ( $i * $i ) > $o ).
tff(c64,type,
c64: $i ).
tff(p46,type,
p46: ( $i * $i ) > $o ).
tff(c55,type,
c55: $i ).
tff(p22,type,
p22: ( $i * $i ) > $o ).
tff(f39,type,
f39: ( $i * $i ) > $i ).
tff(f12,type,
f12: ( $i * $i ) > $i ).
tff(c66,type,
c66: $i ).
tff(c58,type,
c58: $i ).
tff(p47,type,
p47: ( $i * $i ) > $o ).
tff(p16,type,
p16: ( $i * $i ) > $o ).
tff(p13,type,
p13: ( $i * $i ) > $o ).
tff(p2,type,
p2: ( $i * $i ) > $o ).
tff(c52,type,
c52: $i ).
tff(f14,type,
f14: ( $i * $i ) > $i ).
tff(p21,type,
p21: ( $i * $i ) > $o ).
tff(p29,type,
p29: ( $i * $i ) > $o ).
tff(c48,type,
c48: $i ).
tff(f17,type,
f17: ( $i * $i ) > $i ).
tff(p11,type,
p11: ( $i * $i ) > $o ).
tff(p42,type,
p42: ( $i * $i ) > $o ).
tff(p35,type,
p35: ( $i * $i ) > $o ).
tff(c53,type,
c53: $i ).
tff(c63,type,
c63: $i ).
tff(p27,type,
p27: ( $i * $i ) > $o ).
tff(p45,type,
p45: ( $i * $i ) > $o ).
tff(f28,type,
f28: ( $i * $i ) > $i ).
tff(p3,type,
p3: ( $i * $i ) > $o ).
tff(c54,type,
c54: $i ).
tff(f31,type,
f31: ( $i * $i ) > $i ).
tff(p44,type,
p44: ( $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(c50,type,
c50: $i ).
tff(f23,type,
f23: ( $i * $i ) > $i ).
tff(p40,type,
p40: ( $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(p6,type,
p6: ( $i * $i ) > $o ).
tff(p36,type,
p36: ( $i * $i ) > $o ).
tff(c51,type,
c51: $i ).
tff(p26,type,
p26: ( $i * $i ) > $o ).
tff(c56,type,
c56: $i ).
tff(p7,type,
p7: ( $i * $i ) > $o ).
tff(f37,type,
f37: ( $i * $i ) > $i ).
tff(c65,type,
c65: $i ).
tff(c60,type,
c60: $i ).
tff(f41,type,
f41: ( $i * $i ) > $i ).
tff(c49,type,
c49: $i ).
tff(f34,type,
f34: ( $i * $i ) > $i ).
tff(p9,type,
p9: ( $i * $i ) > $o ).
tff(p18,type,
p18: ( $i * $i ) > $o ).
tff(f20,type,
f20: ( $i * $i ) > $i ).
tff(c62,type,
c62: $i ).
tff(c59,type,
c59: $i ).
tff(f25,type,
f25: ( $i * $i ) > $i ).
tff(f_76,axiom,
p46(f23(c58,c56),f20(c59,c60)),
file(unknown,unknown) ).
tff(f_49,axiom,
! [X72] : p29(X72,X72),
file(unknown,unknown) ).
tff(f_290,axiom,
! [X33,X34] : p19(f25(f28(c64,X33),f34(c66,X34)),f34(X33,X34)),
file(unknown,unknown) ).
tff(f_469,axiom,
! [X148,X149] :
( p47(f31(f33(c62,c63),f34(c66,X148)),X149)
| ~ p46(f23(c58,X148),f20(c59,X149)) ),
file(unknown,unknown) ).
tff(f_400,axiom,
! [X89,X90,X91,X92] :
( p30(f31(X89,X90),f31(X91,X92))
| ~ p19(X90,X92)
| ~ p29(X89,X91) ),
file(unknown,unknown) ).
tff(f_476,axiom,
! [X146,X147] :
( p47(f31(f33(c62,c63),f25(f28(c64,c65),X146)),f25(f28(c64,c65),X147))
| ~ p47(f31(f33(c62,c63),X146),X147) ),
file(unknown,unknown) ).
tff(f_63,axiom,
! [X26] : p19(X26,X26),
file(unknown,unknown) ).
tff(f_301,axiom,
! [X142,X143,X145,X144] :
( p47(X142,X143)
| ~ p30(X145,X142)
| ~ p47(X145,X144)
| ~ p19(X144,X143) ),
file(unknown,unknown) ).
tff(f_336,axiom,
~ p47(f31(f33(c62,c63),f34(c65,c56)),f25(f28(c64,c65),c60)),
file(unknown,unknown) ).
tff(c_58,plain,
p46(f23(c58,c56),f20(c59,c60)),
inference(cnfTransformation,[status(thm)],[f_76]) ).
tff(c_28,plain,
! [X72_14] : p29(X72_14,X72_14),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_118,plain,
! [X33_105,X34_106] : p19(f25(f28(c64,X33_105),f34(c66,X34_106)),f34(X33_105,X34_106)),
inference(cnfTransformation,[status(thm)],[f_290]) ).
tff(c_162,plain,
! [X148_187,X149_188] :
( ~ p46(f23(c58,X148_187),f20(c59,X149_188))
| p47(f31(f33(c62,c63),f34(c66,X148_187)),X149_188) ),
inference(cnfTransformation,[status(thm)],[f_469]) ).
tff(c_144,plain,
! [X89_151,X91_153,X90_152,X92_154] :
( ~ p29(X89_151,X91_153)
| ~ p19(X90_152,X92_154)
| p30(f31(X89_151,X90_152),f31(X91_153,X92_154)) ),
inference(cnfTransformation,[status(thm)],[f_400]) ).
tff(c_753,plain,
! [X146_498,X147_499] :
( ~ p47(f31(f33(c62,c63),X146_498),X147_499)
| p47(f31(f33(c62,c63),f25(f28(c64,c65),X146_498)),f25(f28(c64,c65),X147_499)) ),
inference(cnfTransformation,[status(thm)],[f_476]) ).
tff(c_42,plain,
! [X26_21] : p19(X26_21,X26_21),
inference(cnfTransformation,[status(thm)],[f_63]) ).
tff(c_437,plain,
! [X144_352,X143_353,X145_354,X142_355] :
( ~ p19(X144_352,X143_353)
| ~ p47(X145_354,X144_352)
| ~ p30(X145_354,X142_355)
| p47(X142_355,X143_353) ),
inference(cnfTransformation,[status(thm)],[f_301]) ).
tff(c_446,plain,
! [X145_354,X26_21,X142_355] :
( ~ p47(X145_354,X26_21)
| ~ p30(X145_354,X142_355)
| p47(X142_355,X26_21) ),
inference(resolution,[status(thm)],[c_42,c_437]) ).
tff(c_2703,plain,
! [X146_1235,X142_1236,X147_1237] :
( ~ p30(f31(f33(c62,c63),f25(f28(c64,c65),X146_1235)),X142_1236)
| p47(X142_1236,f25(f28(c64,c65),X147_1237))
| ~ p47(f31(f33(c62,c63),X146_1235),X147_1237) ),
inference(resolution,[status(thm)],[c_753,c_446]) ).
tff(c_24765,plain,
! [X91_3491,X92_3492,X147_3493,X146_3494] :
( p47(f31(X91_3491,X92_3492),f25(f28(c64,c65),X147_3493))
| ~ p47(f31(f33(c62,c63),X146_3494),X147_3493)
| ~ p29(f33(c62,c63),X91_3491)
| ~ p19(f25(f28(c64,c65),X146_3494),X92_3492) ),
inference(resolution,[status(thm)],[c_144,c_2703]) ).
tff(c_170818,plain,
! [X91_9823,X92_9824,X149_9825,X148_9826] :
( p47(f31(X91_9823,X92_9824),f25(f28(c64,c65),X149_9825))
| ~ p29(f33(c62,c63),X91_9823)
| ~ p19(f25(f28(c64,c65),f34(c66,X148_9826)),X92_9824)
| ~ p46(f23(c58,X148_9826),f20(c59,X149_9825)) ),
inference(resolution,[status(thm)],[c_162,c_24765]) ).
tff(c_282857,plain,
! [X91_12811,X34_12812,X149_12813] :
( p47(f31(X91_12811,f34(c65,X34_12812)),f25(f28(c64,c65),X149_12813))
| ~ p29(f33(c62,c63),X91_12811)
| ~ p46(f23(c58,X34_12812),f20(c59,X149_12813)) ),
inference(resolution,[status(thm)],[c_118,c_170818]) ).
tff(c_128,plain,
~ p47(f31(f33(c62,c63),f34(c65,c56)),f25(f28(c64,c65),c60)),
inference(cnfTransformation,[status(thm)],[f_336]) ).
tff(c_282931,plain,
( ~ p29(f33(c62,c63),f33(c62,c63))
| ~ p46(f23(c58,c56),f20(c59,c60)) ),
inference(resolution,[status(thm)],[c_282857,c_128]) ).
tff(c_282973,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_58,c_28,c_282931]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SYN709-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.36 % Computer : n005.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed Apr 9 08:11:57 EDT 2025
% 0.14/0.36 % CPUTime :
% 164.43/135.48 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 164.43/135.49
% 164.43/135.49 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------