%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYO613-1 : TPTP v9.0.0. Released v7.1.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 : n010.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:37:58 PM UTC 2025
% Result : Unsatisfiable 17.72s 9.33s
% Output : CNFRefutation 17.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 5
% Syntax : Number of formulae : 53 ( 35 unt; 0 typ; 0 def)
% Number of atoms : 158 ( 0 equ)
% Maximal formula atoms : 23 ( 2 avg)
% Number of connectives : 223 ( 118 ~; 105 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 36 ( 8 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 : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 1 con; 0-2 aty)
% Number of variables : 267 ( 267 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ le > eq > max > #nlpp > s > f > a0
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(le,type,
le: ( $i * $i ) > $o ).
tff(s,type,
s: $i > $i ).
tff(f,type,
f: $i > $i ).
tff(a0,type,
a0: $i ).
tff(max,type,
max: ( $i * $i ) > $i ).
tff(eq,type,
eq: ( $i * $i ) > $o ).
tff(f_25,axiom,
! [A] : le(A,A),
file(unknown,unknown) ).
tff(f_30,axiom,
! [A,B,C] :
( ~ le(max(A,B),C)
| le(A,C) ),
file(unknown,unknown) ).
tff(f_35,axiom,
! [A,B,C] :
( ~ le(max(A,B),C)
| le(B,C) ),
file(unknown,unknown) ).
tff(f_37,axiom,
! [A] : eq(f(A),a0),
file(unknown,unknown) ).
tff(f_106,axiom,
! [A5,A2,A4,A8,A6,A10,A9,A3,A7,A1,A0,A11] :
( ~ eq(f(A0),a0)
| ~ eq(f(A1),a0)
| ~ eq(f(A2),a0)
| ~ eq(f(A3),a0)
| ~ eq(f(A4),a0)
| ~ eq(f(A5),a0)
| ~ eq(f(A6),a0)
| ~ eq(f(A7),a0)
| ~ eq(f(A8),a0)
| ~ eq(f(A9),a0)
| ~ eq(f(A10),a0)
| ~ eq(f(A11),a0)
| ~ le(s(A0),A1)
| ~ le(s(A1),A2)
| ~ le(s(A2),A3)
| ~ le(s(A3),A4)
| ~ le(s(A4),A5)
| ~ le(s(A5),A6)
| ~ le(s(A6),A7)
| ~ le(s(A7),A8)
| ~ le(s(A8),A9)
| ~ le(s(A9),A10)
| ~ le(s(A10),A11) ),
file(unknown,unknown) ).
tff(c_2,plain,
! [A_1] : le(A_1,A_1),
inference(cnfTransformation,[status(thm)],[f_25]) ).
tff(c_15,plain,
! [A_23,C_24,B_25] :
( le(A_23,C_24)
| ~ le(max(A_23,B_25),C_24) ),
inference(cnfTransformation,[status(thm)],[f_30]) ).
tff(c_20,plain,
! [A_23,B_25] : le(A_23,max(A_23,B_25)),
inference(resolution,[status(thm)],[c_2,c_15]) ).
tff(c_33,plain,
! [B_31,C_32,A_33] :
( le(B_31,C_32)
| ~ le(max(A_33,B_31),C_32) ),
inference(cnfTransformation,[status(thm)],[f_35]) ).
tff(c_60,plain,
! [B_36,A_37,B_38] : le(B_36,max(max(A_37,B_36),B_38)),
inference(resolution,[status(thm)],[c_20,c_33]) ).
tff(c_4,plain,
! [A_2,C_4,B_3] :
( le(A_2,C_4)
| ~ le(max(A_2,B_3),C_4) ),
inference(cnfTransformation,[status(thm)],[f_30]) ).
tff(c_93,plain,
! [A_45,A_46,B_47,B_48] : le(A_45,max(max(A_46,max(A_45,B_47)),B_48)),
inference(resolution,[status(thm)],[c_60,c_4]) ).
tff(c_6,plain,
! [B_6,C_7,A_5] :
( le(B_6,C_7)
| ~ le(max(A_5,B_6),C_7) ),
inference(cnfTransformation,[status(thm)],[f_35]) ).
tff(c_417,plain,
! [A_149,B_147,A_148,B_146,B_145] : le(B_147,max(max(A_149,max(max(A_148,B_147),B_145)),B_146)),
inference(resolution,[status(thm)],[c_93,c_6]) ).
tff(c_998,plain,
! [B_361,A_358,A_363,B_360,A_362,B_359] : le(B_360,max(max(A_362,max(max(A_358,max(A_363,B_360)),B_359)),B_361)),
inference(resolution,[status(thm)],[c_417,c_6]) ).
tff(c_2078,plain,
! [B_793,A_794,A_791,B_796,A_795,B_790,A_792] : le(A_795,max(max(A_791,max(max(A_792,max(A_794,max(A_795,B_793))),B_796)),B_790)),
inference(resolution,[status(thm)],[c_998,c_4]) ).
tff(c_2610,plain,
! [B_1094,A_1088,B_1089,B_1091,A_1093,A_1087,A_1090,B_1092] : le(B_1091,max(max(A_1090,max(max(A_1087,max(A_1088,max(max(A_1093,B_1091),B_1094))),B_1089)),B_1092)),
inference(resolution,[status(thm)],[c_2078,c_6]) ).
tff(c_5635,plain,
! [A_2539,B_2545,B_2544,B_2540,A_2542,A_2541,A_2538,B_2537,A_2543] : le(B_2540,max(max(A_2542,max(max(A_2539,max(A_2541,max(max(A_2538,max(A_2543,B_2540)),B_2545))),B_2537)),B_2544)),
inference(resolution,[status(thm)],[c_2610,c_6]) ).
tff(c_5648,plain,
! [A_2539,B_2545,B_2544,A_2542,A_2541,B_3,A_2538,B_2537,A_2543,A_2] : le(A_2,max(max(A_2542,max(max(A_2539,max(A_2541,max(max(A_2538,max(A_2543,max(A_2,B_3))),B_2545))),B_2537)),B_2544)),
inference(resolution,[status(thm)],[c_5635,c_4]) ).
tff(c_49,plain,
! [B_34,A_35] : le(B_34,max(A_35,B_34)),
inference(resolution,[status(thm)],[c_2,c_33]) ).
tff(c_71,plain,
! [B_39,A_40,A_41] : le(B_39,max(A_40,max(A_41,B_39))),
inference(resolution,[status(thm)],[c_49,c_6]) ).
tff(c_213,plain,
! [B_85,A_86,A_87,A_88] : le(B_85,max(A_86,max(A_87,max(A_88,B_85)))),
inference(resolution,[status(thm)],[c_71,c_6]) ).
tff(c_375,plain,
! [A_134,A_130,A_133,A_132,B_131] : le(A_133,max(A_130,max(A_132,max(A_134,max(A_133,B_131))))),
inference(resolution,[status(thm)],[c_213,c_4]) ).
tff(c_900,plain,
! [A_319,A_317,B_318,A_321,B_320,A_316] : le(A_321,max(A_316,max(A_317,max(A_319,max(max(A_321,B_320),B_318))))),
inference(resolution,[status(thm)],[c_375,c_4]) ).
tff(c_1644,plain,
! [B_574,A_577,B_573,A_579,A_575,A_576,B_578] : le(A_575,max(A_577,max(A_576,max(A_579,max(max(max(A_575,B_574),B_578),B_573))))),
inference(resolution,[status(thm)],[c_900,c_4]) ).
tff(c_1656,plain,
! [B_574,B_6,A_577,B_573,A_5,A_579,A_576,B_578] : le(B_6,max(A_577,max(A_576,max(A_579,max(max(max(max(A_5,B_6),B_574),B_578),B_573))))),
inference(resolution,[status(thm)],[c_1644,c_6]) ).
tff(c_185,plain,
! [A_77,A_78,A_79,B_80] : le(A_77,max(A_78,max(A_79,max(A_77,B_80)))),
inference(resolution,[status(thm)],[c_71,c_4]) ).
tff(c_431,plain,
! [A_152,A_150,A_153,B_151,B_154] : le(A_153,max(A_150,max(A_152,max(max(A_153,B_151),B_154)))),
inference(resolution,[status(thm)],[c_185,c_4]) ).
tff(c_970,plain,
! [B_350,A_346,A_351,B_347,A_349,B_348] : le(B_348,max(A_351,max(A_346,max(max(max(A_349,B_348),B_347),B_350)))),
inference(resolution,[status(thm)],[c_431,c_6]) ).
tff(c_982,plain,
! [B_6,B_350,A_346,A_5,A_351,B_347,A_349] : le(B_6,max(A_351,max(A_346,max(max(max(A_349,max(A_5,B_6)),B_347),B_350)))),
inference(resolution,[status(thm)],[c_970,c_6]) ).
tff(c_21,plain,
! [A_26,B_27] : le(A_26,max(A_26,B_27)),
inference(resolution,[status(thm)],[c_2,c_15]) ).
tff(c_27,plain,
! [A_28,B_29,B_30] : le(A_28,max(max(A_28,B_29),B_30)),
inference(resolution,[status(thm)],[c_21,c_4]) ).
tff(c_115,plain,
! [A_53,B_54,B_55,B_56] : le(A_53,max(max(max(A_53,B_54),B_55),B_56)),
inference(resolution,[status(thm)],[c_27,c_4]) ).
tff(c_445,plain,
! [B_155,B_159,B_156,A_158,B_157] : le(B_156,max(max(max(max(A_158,B_156),B_159),B_157),B_155)),
inference(resolution,[status(thm)],[c_115,c_6]) ).
tff(c_458,plain,
! [B_155,B_159,A_158,B_157,B_3,A_2] : le(A_2,max(max(max(max(A_158,max(A_2,B_3)),B_159),B_157),B_155)),
inference(resolution,[status(thm)],[c_445,c_4]) ).
tff(c_32,plain,
! [A_2,B_3,B_29,B_30] : le(A_2,max(max(max(A_2,B_3),B_29),B_30)),
inference(resolution,[status(thm)],[c_27,c_4]) ).
tff(c_70,plain,
! [A_2,A_37,B_3,B_38] : le(A_2,max(max(A_37,max(A_2,B_3)),B_38)),
inference(resolution,[status(thm)],[c_60,c_4]) ).
tff(c_58,plain,
! [B_6,A_35,A_5] : le(B_6,max(A_35,max(A_5,B_6))),
inference(resolution,[status(thm)],[c_49,c_6]) ).
tff(c_48,plain,
! [B_31,A_33] : le(B_31,max(A_33,B_31)),
inference(resolution,[status(thm)],[c_2,c_33]) ).
tff(c_8,plain,
! [A_8] : eq(f(A_8),a0),
inference(cnfTransformation,[status(thm)],[f_37]) ).
tff(c_10,plain,
! [A2_10,A9_15,A7_17,A4_11,A6_13,A8_12,A1_18,A3_16,A11_20,A10_14,A0_19,A5_9] :
( ~ le(s(A10_14),A11_20)
| ~ le(s(A9_15),A10_14)
| ~ le(s(A8_12),A9_15)
| ~ le(s(A7_17),A8_12)
| ~ le(s(A6_13),A7_17)
| ~ le(s(A5_9),A6_13)
| ~ le(s(A4_11),A5_9)
| ~ le(s(A3_16),A4_11)
| ~ le(s(A2_10),A3_16)
| ~ le(s(A1_18),A2_10)
| ~ le(s(A0_19),A1_18)
| ~ eq(f(A11_20),a0)
| ~ eq(f(A10_14),a0)
| ~ eq(f(A9_15),a0)
| ~ eq(f(A8_12),a0)
| ~ eq(f(A7_17),a0)
| ~ eq(f(A6_13),a0)
| ~ eq(f(A5_9),a0)
| ~ eq(f(A4_11),a0)
| ~ eq(f(A3_16),a0)
| ~ eq(f(A2_10),a0)
| ~ eq(f(A1_18),a0)
| ~ eq(f(A0_19),a0) ),
inference(cnfTransformation,[status(thm)],[f_106]) ).
tff(c_148,plain,
! [A3_71,A10_76,A7_68,A4_65,A5_74,A8_69,A11_75,A2_70,A9_73,A1_67,A6_66,A0_72] :
( ~ le(s(A10_76),A11_75)
| ~ le(s(A9_73),A10_76)
| ~ le(s(A8_69),A9_73)
| ~ le(s(A7_68),A8_69)
| ~ le(s(A6_66),A7_68)
| ~ le(s(A5_74),A6_66)
| ~ le(s(A4_65),A5_74)
| ~ le(s(A3_71),A4_65)
| ~ le(s(A2_70),A3_71)
| ~ le(s(A1_67),A2_70)
| ~ le(s(A0_72),A1_67) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_8,c_8,c_8,c_8,c_8,c_8,c_8,c_8,c_8,c_8,c_8,c_10]) ).
tff(c_311,plain,
! [A8_119,A10_125,A1_120,A7_121,A4_122,A6_126,A0_124,A9_128,A2_129,A5_123,A3_127] :
( ~ le(s(A9_128),A10_125)
| ~ le(s(A8_119),A9_128)
| ~ le(s(A7_121),A8_119)
| ~ le(s(A6_126),A7_121)
| ~ le(s(A5_123),A6_126)
| ~ le(s(A4_122),A5_123)
| ~ le(s(A3_127),A4_122)
| ~ le(s(A2_129),A3_127)
| ~ le(s(A1_120),A2_129)
| ~ le(s(A0_124),A1_120) ),
inference(resolution,[status(thm)],[c_2,c_148]) ).
tff(c_501,plain,
! [A3_178,A7_181,A0_175,A8_176,A6_184,A1_180,A2_177,A4_182,A5_183,A9_179] :
( ~ le(s(A8_176),A9_179)
| ~ le(s(A7_181),A8_176)
| ~ le(s(A6_184),A7_181)
| ~ le(s(A5_183),A6_184)
| ~ le(s(A4_182),A5_183)
| ~ le(s(A3_178),A4_182)
| ~ le(s(A2_177),A3_178)
| ~ le(s(A1_180),A2_177)
| ~ le(s(A0_175),A1_180) ),
inference(resolution,[status(thm)],[c_48,c_311]) ).
tff(c_1222,plain,
! [A5_467,A0_469,A6_466,A3_468,A7_472,A8_473,A2_471,A4_474,A1_470] :
( ~ le(s(A7_472),A8_473)
| ~ le(s(A6_466),A7_472)
| ~ le(s(A5_467),A6_466)
| ~ le(s(A4_474),A5_467)
| ~ le(s(A3_468),A4_474)
| ~ le(s(A2_471),A3_468)
| ~ le(s(A1_470),A2_471)
| ~ le(s(A0_469),A1_470) ),
inference(resolution,[status(thm)],[c_58,c_501]) ).
tff(c_3338,plain,
! [A5_1503,A7_1506,A6_1510,A4_1508,A0_1507,A1_1505,A2_1504,A3_1509] :
( ~ le(s(A6_1510),A7_1506)
| ~ le(s(A5_1503),A6_1510)
| ~ le(s(A4_1508),A5_1503)
| ~ le(s(A3_1509),A4_1508)
| ~ le(s(A2_1504),A3_1509)
| ~ le(s(A1_1505),A2_1504)
| ~ le(s(A0_1507),A1_1505) ),
inference(resolution,[status(thm)],[c_70,c_1222]) ).
tff(c_8883,plain,
! [A2_4676,A1_4680,A0_4679,A3_4678,A5_4677,A6_4675,A4_4681] :
( ~ le(s(A5_4677),A6_4675)
| ~ le(s(A4_4681),A5_4677)
| ~ le(s(A3_4678),A4_4681)
| ~ le(s(A2_4676),A3_4678)
| ~ le(s(A1_4680),A2_4676)
| ~ le(s(A0_4679),A1_4680) ),
inference(resolution,[status(thm)],[c_32,c_3338]) ).
tff(c_10567,plain,
! [A0_4684,A3_4683,A4_4686,A1_4685,A5_4687,A2_4682] :
( ~ le(s(A4_4686),A5_4687)
| ~ le(s(A3_4683),A4_4686)
| ~ le(s(A2_4682),A3_4683)
| ~ le(s(A1_4685),A2_4682)
| ~ le(s(A0_4684),A1_4685) ),
inference(resolution,[status(thm)],[c_458,c_8883]) ).
tff(c_12251,plain,
! [A0_4691,A4_4688,A2_4692,A1_4690,A3_4689] :
( ~ le(s(A3_4689),A4_4688)
| ~ le(s(A2_4692),A3_4689)
| ~ le(s(A1_4690),A2_4692)
| ~ le(s(A0_4691),A1_4690) ),
inference(resolution,[status(thm)],[c_982,c_10567]) ).
tff(c_13935,plain,
! [A2_4693,A3_4694,A1_4695,A0_4696] :
( ~ le(s(A2_4693),A3_4694)
| ~ le(s(A1_4695),A2_4693)
| ~ le(s(A0_4696),A1_4695) ),
inference(resolution,[status(thm)],[c_1656,c_12251]) ).
tff(c_15619,plain,
! [A1_4697,A2_4698,A0_4699] :
( ~ le(s(A1_4697),A2_4698)
| ~ le(s(A0_4699),A1_4697) ),
inference(resolution,[status(thm)],[c_2,c_13935]) ).
tff(c_17303,plain,
! [A0_4700,A1_4701] : ~ le(s(A0_4700),A1_4701),
inference(resolution,[status(thm)],[c_5648,c_15619]) ).
tff(c_18988,plain,
$false,
inference(resolution,[status(thm)],[c_5648,c_17303]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SYO613-1 : TPTP v9.0.0. Released v7.1.0.
% 0.08/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.14/0.35 % Computer : n010.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 09:36:04 EDT 2025
% 0.14/0.35 % CPUTime :
% 17.72/9.33 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 17.72/9.34
% 17.72/9.34 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------