%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYN702-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 : n018.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 31.28s 16.95s
% Output : CNFRefutation 31.28s
% 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 : 48 ( 25 ~; 23 |; 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 : 30 ( 30 usr; 10 con; 0-2 aty)
% Number of variables : 58 ( 58 !; 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 > 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(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_274,axiom,
! [X65,X66,X67,X68] : ~ p47(f20(f22(f24(f26(c55,X65),X66),X67),X68),X68),
file(unknown,unknown) ).
tff(f_61,axiom,
! [X38] : p2(X38,X38),
file(unknown,unknown) ).
tff(f_473,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(c55,X65),X66),X67),X68)),f30(f32(f34(f36(c56,X65),X66),X67),X68)),f40(f42(f44(f46(c57,X65),X66),X67),X68))),
file(unknown,unknown) ).
tff(f_461,axiom,
p47(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c54)),c54),
file(unknown,unknown) ).
tff(f_27,axiom,
! [X162] : p7(X162,X162),
file(unknown,unknown) ).
tff(f_325,axiom,
! [X126,X127,X128,X129] :
( p4(f5(X126,X127),f5(X128,X129))
| ~ p2(X126,X128)
| ~ p3(X127,X129) ),
file(unknown,unknown) ).
tff(f_285,axiom,
! [X151,X152,X153,X154] :
( p47(X151,X152)
| ~ p47(X153,X154)
| ~ p7(X154,X152)
| ~ p4(X153,X151) ),
file(unknown,unknown) ).
tff(f_450,axiom,
! [X147,X148,X149,X150] :
( p47(X147,X148)
| ~ p47(f5(c48,f13(f16(f18(c50,X147),X149),X150)),X148) ),
file(unknown,unknown) ).
tff(c_102,plain,
! [X65_101,X66_102,X67_103,X68_104] : ~ p47(f20(f22(f24(f26(c55,X65_101),X66_102),X67_103),X68_104),X68_104),
inference(cnfTransformation,[status(thm)],[f_274]) ).
tff(c_40,plain,
! [X38_20] : p2(X38_20,X38_20),
inference(cnfTransformation,[status(thm)],[f_61]) ).
tff(c_158,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(c55,X65_212),X66_213),X67_214),X68_215)),f30(f32(f34(f36(c56,X65_212),X66_213),X67_214),X68_215)),f40(f42(f44(f46(c57,X65_212),X66_213),X67_214),X68_215))),
inference(cnfTransformation,[status(thm)],[f_473]) ).
tff(c_152,plain,
p47(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c54)),c54),
inference(cnfTransformation,[status(thm)],[f_461]) ).
tff(c_6,plain,
! [X162_3] : p7(X162_3,X162_3),
inference(cnfTransformation,[status(thm)],[f_27]) ).
tff(c_498,plain,
! [X127_421,X129_422,X126_423,X128_424] :
( ~ p3(X127_421,X129_422)
| ~ p2(X126_423,X128_424)
| p4(f5(X126_423,X127_421),f5(X128_424,X129_422)) ),
inference(cnfTransformation,[status(thm)],[f_325]) ).
tff(c_104,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_285]) ).
tff(c_1066,plain,
! [X127_720,X128_715,X129_718,X152_716,X154_717,X126_719] :
( ~ p7(X154_717,X152_716)
| ~ p47(f5(X126_719,X127_720),X154_717)
| p47(f5(X128_715,X129_718),X152_716)
| ~ p3(X127_720,X129_718)
| ~ p2(X126_719,X128_715) ),
inference(resolution,[status(thm)],[c_498,c_104]) ).
tff(c_1070,plain,
! [X162_725,X126_724,X128_721,X129_723,X127_722] :
( ~ p47(f5(X126_724,X127_722),X162_725)
| p47(f5(X128_721,X129_723),X162_725)
| ~ p3(X127_722,X129_723)
| ~ p2(X126_724,X128_721) ),
inference(resolution,[status(thm)],[c_6,c_1066]) ).
tff(c_3014,plain,
! [X128_1764,X129_1765] :
( p47(f5(X128_1764,X129_1765),c54)
| ~ p3(f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c54),X129_1765)
| ~ p2(c48,X128_1764) ),
inference(resolution,[status(thm)],[c_152,c_1070]) ).
tff(c_35595,plain,
! [X128_10651] :
( p47(f5(X128_10651,f13(f16(f18(c50,f20(f22(f24(f26(c55,c51),c52),c53),c54)),f30(f32(f34(f36(c56,c51),c52),c53),c54)),f40(f42(f44(f46(c57,c51),c52),c53),c54))),c54)
| ~ p2(c48,X128_10651) ),
inference(resolution,[status(thm)],[c_158,c_3014]) ).
tff(c_146,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_450]) ).
tff(c_35619,plain,
( p47(f20(f22(f24(f26(c55,c51),c52),c53),c54),c54)
| ~ p2(c48,c48) ),
inference(resolution,[status(thm)],[c_35595,c_146]) ).
tff(c_35632,plain,
p47(f20(f22(f24(f26(c55,c51),c52),c53),c54),c54),
inference(demodulation,[status(thm),theory(equality)],[c_40,c_35619]) ).
tff(c_35634,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_102,c_35632]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : SYN702-1 : TPTP v9.0.0. Released v2.5.0.
% 0.08/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.12/0.34 % Computer : n018.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Apr 9 08:10:47 EDT 2025
% 0.12/0.34 % CPUTime :
% 31.28/16.95 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 31.28/16.96
% 31.28/16.96 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------