%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYN563-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 : n023.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:03:56 PM UTC 2025
% Result : Unsatisfiable 13.77s 5.03s
% Output : CNFRefutation 13.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 13
% Syntax : Number of formulae : 48 ( 14 unt; 0 typ; 0 def)
% Number of atoms : 103 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 117 ( 62 ~; 55 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 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 : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-1 aty)
% Number of variables : 79 ( 79 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ p6 > p5 > p2 > #nlpp > f4 > f3 > c8 > c7
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(f3,type,
f3: $i > $i ).
tff(p2,type,
p2: ( $i * $i ) > $o ).
tff(c8,type,
c8: $i ).
tff(p5,type,
p5: ( $i * $i ) > $o ).
tff(c7,type,
c7: $i ).
tff(f4,type,
f4: $i > $i ).
tff(p6,type,
p6: ( $i * $i ) > $o ).
tff(f_25,axiom,
! [X22] : p6(X22,X22),
file(unknown,unknown) ).
tff(f_23,axiom,
! [X0] : p2(X0,X0),
file(unknown,unknown) ).
tff(f_47,axiom,
! [X27] :
( p6(c7,f3(X27))
| ~ p6(c7,X27) ),
file(unknown,unknown) ).
tff(f_97,axiom,
! [X23,X24,X26,X25] :
( p6(X23,X24)
| ~ p2(X26,X23)
| ~ p6(X26,X25)
| ~ p2(X25,X24) ),
file(unknown,unknown) ).
tff(f_37,axiom,
! [X16] : p5(f3(f3(X16)),f3(f4(X16))),
file(unknown,unknown) ).
tff(f_86,axiom,
! [X7,X8,X9] :
( p5(X7,X8)
| ~ p5(X9,X8)
| ~ p6(X7,X9) ),
file(unknown,unknown) ).
tff(f_28,axiom,
p2(f4(c7),f4(c8)),
file(unknown,unknown) ).
tff(f_70,axiom,
! [X1,X2,X0] :
( p2(X1,X2)
| ~ p2(X0,X1)
| ~ p2(X0,X2) ),
file(unknown,unknown) ).
tff(f_52,axiom,
! [X10,X11] :
( p6(f4(X10),X11)
| ~ p5(X10,X11) ),
file(unknown,unknown) ).
tff(f_30,axiom,
~ p6(f4(c7),f3(f4(c8))),
file(unknown,unknown) ).
tff(f_57,axiom,
! [X3,X4] :
( p2(f3(X3),f3(X4))
| ~ p2(X3,X4) ),
file(unknown,unknown) ).
tff(f_42,axiom,
! [X10,X11] :
( p5(X10,X11)
| ~ p6(f4(X10),X11) ),
file(unknown,unknown) ).
tff(f_108,axiom,
! [X12,X13,X15,X14] :
( p5(X12,X13)
| ~ p2(X15,X13)
| ~ p5(X14,X15)
| ~ p2(X14,X12) ),
file(unknown,unknown) ).
tff(c_4,plain,
! [X22_2] : p6(X22_2,X22_2),
inference(cnfTransformation,[status(thm)],[f_25]) ).
tff(c_2,plain,
! [X0_1] : p2(X0_1,X0_1),
inference(cnfTransformation,[status(thm)],[f_23]) ).
tff(c_18,plain,
! [X27_8] :
( ~ p6(c7,X27_8)
| p6(c7,f3(X27_8)) ),
inference(cnfTransformation,[status(thm)],[f_47]) ).
tff(c_360,plain,
! [X25_81,X24_82,X26_83,X23_84] :
( ~ p2(X25_81,X24_82)
| ~ p6(X26_83,X25_81)
| ~ p2(X26_83,X23_84)
| p6(X23_84,X24_82) ),
inference(cnfTransformation,[status(thm)],[f_97]) ).
tff(c_495,plain,
! [X26_95,X0_96,X23_97] :
( ~ p6(X26_95,X0_96)
| ~ p2(X26_95,X23_97)
| p6(X23_97,X0_96) ),
inference(resolution,[status(thm)],[c_2,c_360]) ).
tff(c_504,plain,
! [X23_97,X27_8] :
( ~ p2(c7,X23_97)
| p6(X23_97,f3(X27_8))
| ~ p6(c7,X27_8) ),
inference(resolution,[status(thm)],[c_18,c_495]) ).
tff(c_14,plain,
! [X16_5] : p5(f3(f3(X16_5)),f3(f4(X16_5))),
inference(cnfTransformation,[status(thm)],[f_37]) ).
tff(c_184,plain,
! [X7_66,X9_67,X8_68] :
( ~ p6(X7_66,X9_67)
| ~ p5(X9_67,X8_68)
| p5(X7_66,X8_68) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_1218,plain,
! [X27_140,X8_141] :
( ~ p5(f3(X27_140),X8_141)
| p5(c7,X8_141)
| ~ p6(c7,X27_140) ),
inference(resolution,[status(thm)],[c_18,c_184]) ).
tff(c_1303,plain,
! [X16_5] :
( p5(c7,f3(f4(X16_5)))
| ~ p6(c7,f3(X16_5)) ),
inference(resolution,[status(thm)],[c_14,c_1218]) ).
tff(c_8,plain,
p2(f4(c7),f4(c8)),
inference(cnfTransformation,[status(thm)],[f_28]) ).
tff(c_105,plain,
! [X0_53,X2_54,X1_55] :
( ~ p2(X0_53,X2_54)
| ~ p2(X0_53,X1_55)
| p2(X1_55,X2_54) ),
inference(cnfTransformation,[status(thm)],[f_70]) ).
tff(c_118,plain,
! [X0_56,X1_57] :
( ~ p2(X0_56,X1_57)
| p2(X1_57,X0_56) ),
inference(resolution,[status(thm)],[c_2,c_105]) ).
tff(c_129,plain,
p2(f4(c8),f4(c7)),
inference(resolution,[status(thm)],[c_8,c_118]) ).
tff(c_20,plain,
! [X10_9,X11_10] :
( ~ p5(X10_9,X11_10)
| p6(f4(X10_9),X11_10) ),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_7541,plain,
! [X10_303,X23_304,X11_305] :
( ~ p2(f4(X10_303),X23_304)
| p6(X23_304,X11_305)
| ~ p5(X10_303,X11_305) ),
inference(resolution,[status(thm)],[c_20,c_495]) ).
tff(c_7582,plain,
! [X11_306] :
( p6(f4(c7),X11_306)
| ~ p5(c8,X11_306) ),
inference(resolution,[status(thm)],[c_129,c_7541]) ).
tff(c_10,plain,
~ p6(f4(c7),f3(f4(c8))),
inference(cnfTransformation,[status(thm)],[f_30]) ).
tff(c_7642,plain,
~ p5(c8,f3(f4(c8))),
inference(resolution,[status(thm)],[c_7582,c_10]) ).
tff(c_22,plain,
! [X3_11,X4_12] :
( ~ p2(X3_11,X4_12)
| p2(f3(X3_11),f3(X4_12)) ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_2906,plain,
! [X3_190,X1_191,X4_192] :
( ~ p2(f3(X3_190),X1_191)
| p2(X1_191,f3(X4_192))
| ~ p2(X3_190,X4_192) ),
inference(resolution,[status(thm)],[c_22,c_105]) ).
tff(c_8838,plain,
! [X4_326,X4_327,X3_328] :
( p2(f3(X4_326),f3(X4_327))
| ~ p2(X3_328,X4_327)
| ~ p2(X3_328,X4_326) ),
inference(resolution,[status(thm)],[c_22,c_2906]) ).
tff(c_22600,plain,
! [X4_549] :
( p2(f3(X4_549),f3(f4(c8)))
| ~ p2(f4(c7),X4_549) ),
inference(resolution,[status(thm)],[c_8,c_8838]) ).
tff(c_7880,plain,
! [X11_308] :
( p6(f4(c8),X11_308)
| ~ p5(c7,X11_308) ),
inference(resolution,[status(thm)],[c_8,c_7541]) ).
tff(c_16,plain,
! [X10_6,X11_7] :
( ~ p6(f4(X10_6),X11_7)
| p5(X10_6,X11_7) ),
inference(cnfTransformation,[status(thm)],[f_42]) ).
tff(c_7930,plain,
! [X11_309] :
( p5(c8,X11_309)
| ~ p5(c7,X11_309) ),
inference(resolution,[status(thm)],[c_7880,c_16]) ).
tff(c_271,plain,
! [X14_74,X12_75,X15_76,X13_77] :
( ~ p2(X14_74,X12_75)
| ~ p5(X14_74,X15_76)
| ~ p2(X15_76,X13_77)
| p5(X12_75,X13_77) ),
inference(cnfTransformation,[status(thm)],[f_108]) ).
tff(c_304,plain,
! [X0_1,X15_76,X13_77] :
( ~ p5(X0_1,X15_76)
| ~ p2(X15_76,X13_77)
| p5(X0_1,X13_77) ),
inference(resolution,[status(thm)],[c_2,c_271]) ).
tff(c_7974,plain,
! [X11_309,X13_77] :
( ~ p2(X11_309,X13_77)
| p5(c8,X13_77)
| ~ p5(c7,X11_309) ),
inference(resolution,[status(thm)],[c_7930,c_304]) ).
tff(c_22617,plain,
! [X4_549] :
( p5(c8,f3(f4(c8)))
| ~ p5(c7,f3(X4_549))
| ~ p2(f4(c7),X4_549) ),
inference(resolution,[status(thm)],[c_22600,c_7974]) ).
tff(c_22664,plain,
! [X4_550] :
( ~ p5(c7,f3(X4_550))
| ~ p2(f4(c7),X4_550) ),
inference(negUnitSimplification,[status(thm)],[c_7642,c_22617]) ).
tff(c_23383,plain,
! [X16_558] :
( ~ p2(f4(c7),f4(X16_558))
| ~ p6(c7,f3(X16_558)) ),
inference(resolution,[status(thm)],[c_1303,c_22664]) ).
tff(c_23439,plain,
~ p6(c7,f3(c7)),
inference(resolution,[status(thm)],[c_2,c_23383]) ).
tff(c_23451,plain,
( ~ p2(c7,c7)
| ~ p6(c7,c7) ),
inference(resolution,[status(thm)],[c_504,c_23439]) ).
tff(c_23475,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4,c_2,c_23451]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SYN563-1 : TPTP v9.0.0. Released v2.5.0.
% 0.11/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.33 % Computer : n023.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Wed Apr 9 08:00:54 EDT 2025
% 0.13/0.33 % CPUTime :
% 13.77/5.03 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.80/5.04
% 13.80/5.04 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------