%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYN627-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 : n024.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:03 PM UTC 2025
% Result : Unsatisfiable 21.07s 9.82s
% Output : CNFRefutation 21.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 11
% Syntax : Number of formulae : 39 ( 16 unt; 0 typ; 0 def)
% Number of atoms : 75 ( 0 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 76 ( 40 ~; 36 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-5 aty)
% Number of functors : 16 ( 16 usr; 9 con; 0-5 aty)
% Number of variables : 51 ( 51 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ p16 > p8 > p6 > p5 > p3 > p2 > p15 > p10 > f11 > f9 > f7 > f4 > #nlpp > f14 > f13 > f12 > c25 > c24 > c23 > c22 > c21 > c20 > c19 > c18 > c17
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(f12,type,
f12: $i > $i ).
tff(p15,type,
p15: ( $i * $i ) > $o ).
tff(f9,type,
f9: ( $i * $i ) > $i ).
tff(p2,type,
p2: ( $i * $i ) > $o ).
tff(c21,type,
c21: $i ).
tff(f14,type,
f14: $i > $i ).
tff(c23,type,
c23: $i ).
tff(f13,type,
f13: $i > $i ).
tff(c17,type,
c17: $i ).
tff(p8,type,
p8: ( $i * $i ) > $o ).
tff(c22,type,
c22: $i ).
tff(f7,type,
f7: ( $i * $i ) > $i ).
tff(p5,type,
p5: ( $i * $i ) > $o ).
tff(p3,type,
p3: ( $i * $i ) > $o ).
tff(c25,type,
c25: $i ).
tff(f4,type,
f4: ( $i * $i ) > $i ).
tff(f11,type,
f11: ( $i * $i * $i * $i * $i ) > $i ).
tff(c18,type,
c18: $i ).
tff(p10,type,
p10: ( $i * $i ) > $o ).
tff(p6,type,
p6: ( $i * $i ) > $o ).
tff(c19,type,
c19: $i ).
tff(c20,type,
c20: $i ).
tff(p16,type,
p16: ( $i * $i * $i * $i * $i ) > $o ).
tff(c24,type,
c24: $i ).
tff(f_34,axiom,
p15(c18,c19),
file(unknown,unknown) ).
tff(f_121,axiom,
! [X32] :
( p16(c17,c20,f9(c19,X32),f14(X32),c25)
| ~ p15(X32,c19) ),
file(unknown,unknown) ).
tff(f_38,axiom,
p16(c17,c20,f9(c19,c18),c21,c22),
file(unknown,unknown) ).
tff(f_164,axiom,
! [X5,X6,X4,X3] :
( p3(X5,X6)
| ~ p16(c17,c20,X4,X6,X3)
| ~ p16(c17,c20,X4,X5,c22) ),
file(unknown,unknown) ).
tff(f_31,axiom,
! [X40] : p3(X40,X40),
file(unknown,unknown) ).
tff(f_93,axiom,
! [X41,X42,X40] :
( p3(X41,X42)
| ~ p3(X40,X41)
| ~ p3(X40,X42) ),
file(unknown,unknown) ).
tff(f_33,axiom,
! [X33] : p2(X33,X33),
file(unknown,unknown) ).
tff(f_36,axiom,
~ p3(c23,c24),
file(unknown,unknown) ).
tff(f_156,axiom,
! [X57,X58,X59,X60] :
( p3(f4(X57,X58),f4(X59,X60))
| ~ p2(X57,X59)
| ~ p3(X58,X60) ),
file(unknown,unknown) ).
tff(f_37,axiom,
p3(c23,f4(f7(c17,c18),c21)),
file(unknown,unknown) ).
tff(f_106,axiom,
! [X32] :
( p3(c24,f4(f7(c17,X32),f14(X32)))
| ~ p15(X32,c19) ),
file(unknown,unknown) ).
tff(c_14,plain,
p15(c18,c19),
inference(cnfTransformation,[status(thm)],[f_34]) ).
tff(c_46,plain,
! [X32_34] :
( ~ p15(X32_34,c19)
| p16(c17,c20,f9(c19,X32_34),f14(X32_34),c25) ),
inference(cnfTransformation,[status(thm)],[f_121]) ).
tff(c_20,plain,
p16(c17,c20,f9(c19,c18),c21,c22),
inference(cnfTransformation,[status(thm)],[f_38]) ).
tff(c_590,plain,
! [X4_244,X5_245,X6_246,X3_247] :
( ~ p16(c17,c20,X4_244,X5_245,c22)
| ~ p16(c17,c20,X4_244,X6_246,X3_247)
| p3(X5_245,X6_246) ),
inference(cnfTransformation,[status(thm)],[f_164]) ).
tff(c_820,plain,
! [X6_264,X3_265] :
( ~ p16(c17,c20,f9(c19,c18),X6_264,X3_265)
| p3(c21,X6_264) ),
inference(resolution,[status(thm)],[c_20,c_590]) ).
tff(c_824,plain,
( p3(c21,f14(c18))
| ~ p15(c18,c19) ),
inference(resolution,[status(thm)],[c_46,c_820]) ).
tff(c_834,plain,
p3(c21,f14(c18)),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_824]) ).
tff(c_10,plain,
! [X40_5] : p3(X40_5,X40_5),
inference(cnfTransformation,[status(thm)],[f_31]) ).
tff(c_140,plain,
! [X40_137,X42_138,X41_139] :
( ~ p3(X40_137,X42_138)
| ~ p3(X40_137,X41_139)
| p3(X41_139,X42_138) ),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_152,plain,
! [X40_5,X41_139] :
( ~ p3(X40_5,X41_139)
| p3(X41_139,X40_5) ),
inference(resolution,[status(thm)],[c_10,c_140]) ).
tff(c_847,plain,
p3(f14(c18),c21),
inference(resolution,[status(thm)],[c_834,c_152]) ).
tff(c_12,plain,
! [X33_6] : p2(X33_6,X33_6),
inference(cnfTransformation,[status(thm)],[f_33]) ).
tff(c_16,plain,
~ p3(c23,c24),
inference(cnfTransformation,[status(thm)],[f_36]) ).
tff(c_425,plain,
! [X58_218,X60_219,X57_220,X59_221] :
( ~ p3(X58_218,X60_219)
| ~ p2(X57_220,X59_221)
| p3(f4(X57_220,X58_218),f4(X59_221,X60_219)) ),
inference(cnfTransformation,[status(thm)],[f_156]) ).
tff(c_451,plain,
! [X59_228,X60_229,X57_230,X58_231] :
( p3(f4(X59_228,X60_229),f4(X57_230,X58_231))
| ~ p3(X58_231,X60_229)
| ~ p2(X57_230,X59_228) ),
inference(resolution,[status(thm)],[c_425,c_152]) ).
tff(c_18,plain,
p3(c23,f4(f7(c17,c18),c21)),
inference(cnfTransformation,[status(thm)],[f_37]) ).
tff(c_157,plain,
! [X40_141,X41_142] :
( ~ p3(X40_141,X41_142)
| p3(X41_142,X40_141) ),
inference(resolution,[status(thm)],[c_10,c_140]) ).
tff(c_171,plain,
p3(f4(f7(c17,c18),c21),c23),
inference(resolution,[status(thm)],[c_18,c_157]) ).
tff(c_36,plain,
! [X40_27,X42_26,X41_25] :
( ~ p3(X40_27,X42_26)
| ~ p3(X40_27,X41_25)
| p3(X41_25,X42_26) ),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_180,plain,
! [X41_25] :
( ~ p3(f4(f7(c17,c18),c21),X41_25)
| p3(X41_25,c23) ),
inference(resolution,[status(thm)],[c_171,c_36]) ).
tff(c_460,plain,
! [X57_230,X58_231] :
( p3(f4(X57_230,X58_231),c23)
| ~ p3(X58_231,c21)
| ~ p2(X57_230,f7(c17,c18)) ),
inference(resolution,[status(thm)],[c_451,c_180]) ).
tff(c_40,plain,
! [X32_31] :
( ~ p15(X32_31,c19)
| p3(c24,f4(f7(c17,X32_31),f14(X32_31))) ),
inference(cnfTransformation,[status(thm)],[f_106]) ).
tff(c_307,plain,
! [X32_172] :
( p3(f4(f7(c17,X32_172),f14(X32_172)),c24)
| ~ p15(X32_172,c19) ),
inference(resolution,[status(thm)],[c_40,c_157]) ).
tff(c_47524,plain,
! [X32_1480,X41_1481] :
( ~ p3(f4(f7(c17,X32_1480),f14(X32_1480)),X41_1481)
| p3(X41_1481,c24)
| ~ p15(X32_1480,c19) ),
inference(resolution,[status(thm)],[c_307,c_36]) ).
tff(c_47535,plain,
! [X32_1480] :
( p3(c23,c24)
| ~ p15(X32_1480,c19)
| ~ p3(f14(X32_1480),c21)
| ~ p2(f7(c17,X32_1480),f7(c17,c18)) ),
inference(resolution,[status(thm)],[c_460,c_47524]) ).
tff(c_48380,plain,
! [X32_1527] :
( ~ p15(X32_1527,c19)
| ~ p3(f14(X32_1527),c21)
| ~ p2(f7(c17,X32_1527),f7(c17,c18)) ),
inference(negUnitSimplification,[status(thm)],[c_16,c_47535]) ).
tff(c_48392,plain,
( ~ p15(c18,c19)
| ~ p3(f14(c18),c21) ),
inference(resolution,[status(thm)],[c_12,c_48380]) ).
tff(c_48402,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_847,c_14,c_48392]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SYN627-1 : TPTP v9.0.0. Released v2.5.0.
% 0.04/0.13 % 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.13/0.34 % Computer : n024.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:05:06 EDT 2025
% 0.13/0.34 % CPUTime :
% 21.07/9.82 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 21.07/9.83
% 21.07/9.83 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------