%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYN704-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 : n016.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:14 PM UTC 2025
% Result : Unsatisfiable 65.75s 49.58s
% Output : CNFRefutation 65.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 11
% Syntax : Number of formulae : 35 ( 18 unt; 0 typ; 0 def)
% Number of atoms : 69 ( 0 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 70 ( 36 ~; 34 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 27 ( 26 usr; 1 prp; 0-2 aty)
% Number of functors : 31 ( 31 usr; 11 con; 0-2 aty)
% Number of variables : 76 ( 76 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ p9 > p7 > p6 > p47 > p45 > p43 > p41 > p4 > p39 > p37 > p35 > p33 > p31 > p3 > p29 > p27 > p25 > p23 > p21 > p2 > p19 > p17 > p15 > p14 > p12 > p11 > f8 > f5 > f46 > f44 > f42 > f40 > f38 > f36 > f34 > f32 > f30 > f28 > f26 > f24 > f22 > f20 > f18 > f16 > f13 > f10 > #nlpp > c58 > c57 > c56 > c55 > c54 > c53 > c52 > c51 > c50 > c49 > c48
%Foreground sorts:
%Background operators:
%Foreground operators:
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(f32,type,
f32: ( $i * $i ) > $i ).
tff(p43,type,
p43: ( $i * $i ) > $o ).
tff(f26,type,
f26: ( $i * $i ) > $i ).
tff(f22,type,
f22: ( $i * $i ) > $i ).
tff(p23,type,
p23: ( $i * $i ) > $o ).
tff(c55,type,
c55: $i ).
tff(f36,type,
f36: ( $i * $i ) > $i ).
tff(c58,type,
c58: $i ).
tff(p47,type,
p47: ( $i * $i ) > $o ).
tff(f13,type,
f13: ( $i * $i ) > $i ).
tff(p2,type,
p2: ( $i * $i ) > $o ).
tff(c52,type,
c52: $i ).
tff(f24,type,
f24: ( $i * $i ) > $i ).
tff(f44,type,
f44: ( $i * $i ) > $i ).
tff(f38,type,
f38: ( $i * $i ) > $i ).
tff(p21,type,
p21: ( $i * $i ) > $o ).
tff(p29,type,
p29: ( $i * $i ) > $o ).
tff(c48,type,
c48: $i ).
tff(p11,type,
p11: ( $i * $i ) > $o ).
tff(p31,type,
p31: ( $i * $i ) > $o ).
tff(p17,type,
p17: ( $i * $i ) > $o ).
tff(f30,type,
f30: ( $i * $i ) > $i ).
tff(p35,type,
p35: ( $i * $i ) > $o ).
tff(c53,type,
c53: $i ).
tff(p33,type,
p33: ( $i * $i ) > $o ).
tff(f18,type,
f18: ( $i * $i ) > $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(f46,type,
f46: ( $i * $i ) > $i ).
tff(f42,type,
f42: ( $i * $i ) > $i ).
tff(p37,type,
p37: ( $i * $i ) > $o ).
tff(f8,type,
f8: ( $i * $i ) > $i ).
tff(p39,type,
p39: ( $i * $i ) > $o ).
tff(p19,type,
p19: ( $i * $i ) > $o ).
tff(p25,type,
p25: ( $i * $i ) > $o ).
tff(p14,type,
p14: ( $i * $i ) > $o ).
tff(c50,type,
c50: $i ).
tff(p41,type,
p41: ( $i * $i ) > $o ).
tff(f40,type,
f40: ( $i * $i ) > $i ).
tff(f16,type,
f16: ( $i * $i ) > $i ).
tff(p6,type,
p6: ( $i * $i ) > $o ).
tff(f10,type,
f10: ( $i * $i ) > $i ).
tff(c51,type,
c51: $i ).
tff(c56,type,
c56: $i ).
tff(p7,type,
p7: ( $i * $i ) > $o ).
tff(c49,type,
c49: $i ).
tff(f34,type,
f34: ( $i * $i ) > $i ).
tff(p12,type,
p12: ( $i * $i ) > $o ).
tff(p9,type,
p9: ( $i * $i ) > $o ).
tff(f20,type,
f20: ( $i * $i ) > $i ).
tff(f_275,axiom,
! [X65,X66,X67,X68] : ~ p47(f20(f22(f24(f26(c56,X65),X66),X67),X68),X68),
file(unknown,unknown) ).
tff(f_61,axiom,
! [X38] : p2(X38,X38),
file(unknown,unknown) ).
tff(f_474,axiom,
! [X65,X66,X67,X68] : p3(f8(f10(c49,f13(f16(f18(c50,X65),X66),X67)),X68),f13(f16(f18(c50,f20(f22(f24(f26(c56,X65),X66),X67),X68)),f30(f32(f34(f36(c57,X65),X66),X67),X68)),f40(f42(f44(f46(c58,X65),X66),X67),X68))),
file(unknown,unknown) ).
tff(f_462,axiom,
p47(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c54)),c55),
file(unknown,unknown) ).
tff(f_27,axiom,
! [X162] : p7(X162,X162),
file(unknown,unknown) ).
tff(f_326,axiom,
! [X126,X127,X128,X129] :
( p4(f5(X126,X127),f5(X128,X129))
| ~ p2(X126,X128)
| ~ p3(X127,X129) ),
file(unknown,unknown) ).
tff(f_286,axiom,
! [X151,X152,X153,X154] :
( p47(X151,X152)
| ~ p47(X153,X154)
| ~ p7(X154,X152)
| ~ p4(X153,X151) ),
file(unknown,unknown) ).
tff(f_451,axiom,
! [X147,X148,X149,X150] :
( p47(X147,X148)
| ~ p47(f5(c48,f13(f16(f18(c50,X147),X149),X150)),X148) ),
file(unknown,unknown) ).
tff(f_72,axiom,
p7(c54,c55),
file(unknown,unknown) ).
tff(f_96,axiom,
! [X163,X164,X162] :
( p7(X163,X164)
| ~ p7(X162,X163)
| ~ p7(X162,X164) ),
file(unknown,unknown) ).
tff(f_37,axiom,
! [X119] : p4(X119,X119),
file(unknown,unknown) ).
tff(c_104,plain,
! [X65_101,X66_102,X67_103,X68_104] : ~ p47(f20(f22(f24(f26(c56,X65_101),X66_102),X67_103),X68_104),X68_104),
inference(cnfTransformation,[status(thm)],[f_275]) ).
tff(c_40,plain,
! [X38_20] : p2(X38_20,X38_20),
inference(cnfTransformation,[status(thm)],[f_61]) ).
tff(c_160,plain,
! [X65_212,X66_213,X67_214,X68_215] : p3(f8(f10(c49,f13(f16(f18(c50,X65_212),X66_213),X67_214)),X68_215),f13(f16(f18(c50,f20(f22(f24(f26(c56,X65_212),X66_213),X67_214),X68_215)),f30(f32(f34(f36(c57,X65_212),X66_213),X67_214),X68_215)),f40(f42(f44(f46(c58,X65_212),X66_213),X67_214),X68_215))),
inference(cnfTransformation,[status(thm)],[f_474]) ).
tff(c_154,plain,
p47(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c54)),c55),
inference(cnfTransformation,[status(thm)],[f_462]) ).
tff(c_6,plain,
! [X162_3] : p7(X162_3,X162_3),
inference(cnfTransformation,[status(thm)],[f_27]) ).
tff(c_548,plain,
! [X127_428,X129_429,X126_430,X128_431] :
( ~ p3(X127_428,X129_429)
| ~ p2(X126_430,X128_431)
| p4(f5(X126_430,X127_428),f5(X128_431,X129_429)) ),
inference(cnfTransformation,[status(thm)],[f_326]) ).
tff(c_106,plain,
! [X153_107,X151_105,X154_108,X152_106] :
( ~ p4(X153_107,X151_105)
| ~ p7(X154_108,X152_106)
| ~ p47(X153_107,X154_108)
| p47(X151_105,X152_106) ),
inference(cnfTransformation,[status(thm)],[f_286]) ).
tff(c_1163,plain,
! [X129_726,X152_729,X154_730,X127_731,X126_728,X128_727] :
( ~ p7(X154_730,X152_729)
| ~ p47(f5(X126_728,X127_731),X154_730)
| p47(f5(X128_727,X129_726),X152_729)
| ~ p3(X127_731,X129_726)
| ~ p2(X126_728,X128_727) ),
inference(resolution,[status(thm)],[c_548,c_106]) ).
tff(c_1173,plain,
! [X127_734,X162_736,X126_733,X129_732,X128_735] :
( ~ p47(f5(X126_733,X127_734),X162_736)
| p47(f5(X128_735,X129_732),X162_736)
| ~ p3(X127_734,X129_732)
| ~ p2(X126_733,X128_735) ),
inference(resolution,[status(thm)],[c_6,c_1163]) ).
tff(c_15306,plain,
! [X128_2426,X129_2427] :
( p47(f5(X128_2426,X129_2427),c55)
| ~ p3(f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c54),X129_2427)
| ~ p2(c48,X128_2426) ),
inference(resolution,[status(thm)],[c_154,c_1173]) ).
tff(c_152362,plain,
! [X128_8961] :
( p47(f5(X128_8961,f13(f16(f18(c50,f20(f22(f24(f26(c56,c51),c52),c53),c54)),f30(f32(f34(f36(c57,c51),c52),c53),c54)),f40(f42(f44(f46(c58,c51),c52),c53),c54))),c55)
| ~ p2(c48,X128_8961) ),
inference(resolution,[status(thm)],[c_160,c_15306]) ).
tff(c_148,plain,
! [X147_189,X149_191,X150_192,X148_190] :
( ~ p47(f5(c48,f13(f16(f18(c50,X147_189),X149_191),X150_192)),X148_190)
| p47(X147_189,X148_190) ),
inference(cnfTransformation,[status(thm)],[f_451]) ).
tff(c_152378,plain,
( p47(f20(f22(f24(f26(c56,c51),c52),c53),c54),c55)
| ~ p2(c48,c48) ),
inference(resolution,[status(thm)],[c_152362,c_148]) ).
tff(c_152390,plain,
p47(f20(f22(f24(f26(c56,c51),c52),c53),c54),c55),
inference(demodulation,[status(thm),theory(equality)],[c_40,c_152378]) ).
tff(c_52,plain,
p7(c54,c55),
inference(cnfTransformation,[status(thm)],[f_72]) ).
tff(c_402,plain,
! [X162_361,X164_362,X163_363] :
( ~ p7(X162_361,X164_362)
| ~ p7(X162_361,X163_363)
| p7(X163_363,X164_362) ),
inference(cnfTransformation,[status(thm)],[f_96]) ).
tff(c_410,plain,
! [X162_368,X163_369] :
( ~ p7(X162_368,X163_369)
| p7(X163_369,X162_368) ),
inference(resolution,[status(thm)],[c_6,c_402]) ).
tff(c_417,plain,
p7(c55,c54),
inference(resolution,[status(thm)],[c_52,c_410]) ).
tff(c_16,plain,
! [X119_8] : p4(X119_8,X119_8),
inference(cnfTransformation,[status(thm)],[f_37]) ).
tff(c_435,plain,
! [X153_371,X151_372,X154_373,X152_374] :
( ~ p4(X153_371,X151_372)
| ~ p7(X154_373,X152_374)
| ~ p47(X153_371,X154_373)
| p47(X151_372,X152_374) ),
inference(cnfTransformation,[status(thm)],[f_286]) ).
tff(c_449,plain,
! [X154_376,X152_377,X119_378] :
( ~ p7(X154_376,X152_377)
| ~ p47(X119_378,X154_376)
| p47(X119_378,X152_377) ),
inference(resolution,[status(thm)],[c_16,c_435]) ).
tff(c_456,plain,
! [X119_378] :
( ~ p47(X119_378,c55)
| p47(X119_378,c54) ),
inference(resolution,[status(thm)],[c_417,c_449]) ).
tff(c_152505,plain,
p47(f20(f22(f24(f26(c56,c51),c52),c53),c54),c54),
inference(resolution,[status(thm)],[c_152390,c_456]) ).
tff(c_152600,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_104,c_152505]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYN704-1 : TPTP v9.0.0. Released v2.5.0.
% 0.03/0.13 % 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.34 % Computer : n016.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Apr 9 08:11:23 EDT 2025
% 0.13/0.34 % CPUTime :
% 65.75/49.58 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 65.78/49.58
% 65.78/49.58 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------