%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYN710-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 : n032.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:15 PM UTC 2025
% Result : Unsatisfiable 12.63s 4.05s
% Output : CNFRefutation 12.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 8
% Syntax : Number of formulae : 30 ( 7 unt; 0 typ; 0 def)
% Number of atoms : 57 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 52 ( 25 ~; 27 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 25 ( 24 usr; 1 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 18 con; 0-2 aty)
% Number of variables : 54 ( 54 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ p8 > p7 > p6 > p4 > p37 > p36 > p35 > p34 > p33 > p31 > p3 > p29 > p28 > p26 > p24 > p23 > p21 > p2 > p19 > p17 > p15 > p14 > p12 > p10 > f9 > f5 > f32 > f30 > f27 > f25 > f22 > f20 > f18 > f16 > f13 > f11 > #nlpp > c55 > c54 > c53 > c52 > c51 > c50 > c49 > c48 > c47 > c46 > c45 > c44 > c43 > c42 > c41 > c40 > c39 > c38
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(f11,type,
f11: ( $i * $i ) > $i ).
tff(f5,type,
f5: ( $i * $i ) > $i ).
tff(p15,type,
p15: ( $i * $i ) > $o ).
tff(p4,type,
p4: ( $i * $i ) > $o ).
tff(f32,type,
f32: ( $i * $i ) > $i ).
tff(c47,type,
c47: $i ).
tff(f22,type,
f22: ( $i * $i ) > $i ).
tff(p23,type,
p23: ( $i * $i ) > $o ).
tff(c55,type,
c55: $i ).
tff(c45,type,
c45: $i ).
tff(f13,type,
f13: ( $i * $i ) > $i ).
tff(f9,type,
f9: ( $i * $i ) > $i ).
tff(p2,type,
p2: ( $i * $i ) > $o ).
tff(c52,type,
c52: $i ).
tff(c40,type,
c40: $i ).
tff(p21,type,
p21: ( $i * $i ) > $o ).
tff(p29,type,
p29: ( $i * $i ) > $o ).
tff(c48,type,
c48: $i ).
tff(c42,type,
c42: $i ).
tff(p31,type,
p31: ( $i * $i ) > $o ).
tff(p17,type,
p17: ( $i * $i ) > $o ).
tff(p8,type,
p8: ( $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(c41,type,
c41: $i ).
tff(c39,type,
c39: $i ).
tff(c44,type,
c44: $i ).
tff(f18,type,
f18: ( $i * $i ) > $i ).
tff(p3,type,
p3: ( $i * $i ) > $o ).
tff(c54,type,
c54: $i ).
tff(c38,type,
c38: $i ).
tff(p37,type,
p37: ( $i * $i ) > $o ).
tff(c46,type,
c46: $i ).
tff(p19,type,
p19: ( $i * $i ) > $o ).
tff(p14,type,
p14: ( $i * $i ) > $o ).
tff(p24,type,
p24: ( $i * $i ) > $o ).
tff(c50,type,
c50: $i ).
tff(c43,type,
c43: $i ).
tff(p10,type,
p10: ( $i * $i ) > $o ).
tff(f16,type,
f16: ( $i * $i ) > $i ).
tff(p6,type,
p6: ( $i * $i ) > $o ).
tff(p36,type,
p36: ( $i * $i ) > $o ).
tff(f27,type,
f27: ( $i * $i ) > $i ).
tff(c51,type,
c51: $i ).
tff(p28,type,
p28: ( $i * $i ) > $o ).
tff(p26,type,
p26: ( $i * $i ) > $o ).
tff(p7,type,
p7: ( $i * $i ) > $o ).
tff(p34,type,
p34: ( $i * $i ) > $o ).
tff(c49,type,
c49: $i ).
tff(p12,type,
p12: ( $i * $i ) > $o ).
tff(f20,type,
f20: ( $i * $i ) > $i ).
tff(f25,type,
f25: ( $i * $i ) > $i ).
tff(f_67,axiom,
~ p33(f11(c46,c50),f9(c47,c43)),
file(unknown,unknown) ).
tff(f_425,axiom,
! [X79,X80] :
( p33(f11(c46,X79),X80)
| p33(f18(c51,f20(f22(c52,X79),X80)),X79) ),
file(unknown,unknown) ).
tff(f_77,axiom,
! [X83,X82] :
( p36(X83,X82)
| ~ p33(f18(c51,X82),X83) ),
file(unknown,unknown) ).
tff(f_440,axiom,
! [X13,X14,X15] :
( p33(f18(c51,X13),f13(f16(c48,X14),X15))
| ~ p33(f18(c51,X13),X15) ),
file(unknown,unknown) ).
tff(f_430,axiom,
! [X79,X80] :
( p33(f11(c46,X79),X80)
| ~ p33(f18(c51,f20(f22(c52,X79),X80)),X80) ),
file(unknown,unknown) ).
tff(f_82,axiom,
! [X82,X83] :
( p33(f18(c51,X82),X83)
| ~ p36(X83,X82) ),
file(unknown,unknown) ).
tff(f_488,axiom,
! [X81,X80,X79] :
( p33(f18(c51,X81),X80)
| ~ p33(f11(c46,X79),X80)
| ~ p33(f18(c51,X81),X79) ),
file(unknown,unknown) ).
tff(f_245,axiom,
p33(f11(c46,f13(f16(c48,c49),c50)),f9(c47,c43)),
file(unknown,unknown) ).
tff(c_50,plain,
~ p33(f11(c46,c50),f9(c47,c43)),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_614,plain,
! [X79_428,X80_429] :
( p33(f18(c51,f20(f22(c52,X79_428),X80_429)),X79_428)
| p33(f11(c46,X79_428),X80_429) ),
inference(cnfTransformation,[status(thm)],[f_425]) ).
tff(c_54,plain,
! [X82_23,X83_22] :
( ~ p33(f18(c51,X82_23),X83_22)
| p36(X83_22,X82_23) ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_621,plain,
! [X79_428,X80_429] :
( p36(X79_428,f20(f22(c52,X79_428),X80_429))
| p33(f11(c46,X79_428),X80_429) ),
inference(resolution,[status(thm)],[c_614,c_54]) ).
tff(c_144,plain,
! [X79_163,X80_164] :
( p33(f18(c51,f20(f22(c52,X79_163),X80_164)),X79_163)
| p33(f11(c46,X79_163),X80_164) ),
inference(cnfTransformation,[status(thm)],[f_425]) ).
tff(c_150,plain,
! [X13_170,X15_172,X14_171] :
( ~ p33(f18(c51,X13_170),X15_172)
| p33(f18(c51,X13_170),f13(f16(c48,X14_171),X15_172)) ),
inference(cnfTransformation,[status(thm)],[f_440]) ).
tff(c_777,plain,
! [X79_493,X80_494] :
( ~ p33(f18(c51,f20(f22(c52,X79_493),X80_494)),X80_494)
| p33(f11(c46,X79_493),X80_494) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_3745,plain,
! [X79_1062,X14_1063,X15_1064] :
( p33(f11(c46,X79_1062),f13(f16(c48,X14_1063),X15_1064))
| ~ p33(f18(c51,f20(f22(c52,X79_1062),f13(f16(c48,X14_1063),X15_1064))),X15_1064) ),
inference(resolution,[status(thm)],[c_150,c_777]) ).
tff(c_3868,plain,
! [X79_1065,X14_1066] : p33(f11(c46,X79_1065),f13(f16(c48,X14_1066),X79_1065)),
inference(resolution,[status(thm)],[c_144,c_3745]) ).
tff(c_56,plain,
! [X83_25,X82_24] :
( ~ p36(X83_25,X82_24)
| p33(f18(c51,X82_24),X83_25) ),
inference(cnfTransformation,[status(thm)],[f_82]) ).
tff(c_935,plain,
! [X81_528,X79_529,X80_530] :
( ~ p33(f18(c51,X81_528),X79_529)
| ~ p33(f11(c46,X79_529),X80_530)
| p33(f18(c51,X81_528),X80_530) ),
inference(cnfTransformation,[status(thm)],[f_488]) ).
tff(c_947,plain,
! [X83_25,X80_530,X82_24] :
( ~ p33(f11(c46,X83_25),X80_530)
| p33(f18(c51,X82_24),X80_530)
| ~ p36(X83_25,X82_24) ),
inference(resolution,[status(thm)],[c_56,c_935]) ).
tff(c_3898,plain,
! [X82_1067,X14_1068,X79_1069] :
( p33(f18(c51,X82_1067),f13(f16(c48,X14_1068),X79_1069))
| ~ p36(X79_1069,X82_1067) ),
inference(resolution,[status(thm)],[c_3868,c_947]) ).
tff(c_3923,plain,
! [X14_1070,X79_1071,X82_1072] :
( p36(f13(f16(c48,X14_1070),X79_1071),X82_1072)
| ~ p36(X79_1071,X82_1072) ),
inference(resolution,[status(thm)],[c_3898,c_54]) ).
tff(c_100,plain,
p33(f11(c46,f13(f16(c48,c49),c50)),f9(c47,c43)),
inference(cnfTransformation,[status(thm)],[f_245]) ).
tff(c_948,plain,
! [X83_531,X80_532,X82_533] :
( ~ p33(f11(c46,X83_531),X80_532)
| p33(f18(c51,X82_533),X80_532)
| ~ p36(X83_531,X82_533) ),
inference(resolution,[status(thm)],[c_56,c_935]) ).
tff(c_980,plain,
! [X82_533] :
( p33(f18(c51,X82_533),f9(c47,c43))
| ~ p36(f13(f16(c48,c49),c50),X82_533) ),
inference(resolution,[status(thm)],[c_100,c_948]) ).
tff(c_3985,plain,
! [X82_1077] :
( p33(f18(c51,X82_1077),f9(c47,c43))
| ~ p36(c50,X82_1077) ),
inference(resolution,[status(thm)],[c_3923,c_980]) ).
tff(c_146,plain,
! [X79_165,X80_166] :
( ~ p33(f18(c51,f20(f22(c52,X79_165),X80_166)),X80_166)
| p33(f11(c46,X79_165),X80_166) ),
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_4950,plain,
! [X79_1176] :
( p33(f11(c46,X79_1176),f9(c47,c43))
| ~ p36(c50,f20(f22(c52,X79_1176),f9(c47,c43))) ),
inference(resolution,[status(thm)],[c_3985,c_146]) ).
tff(c_4958,plain,
p33(f11(c46,c50),f9(c47,c43)),
inference(resolution,[status(thm)],[c_621,c_4950]) ).
tff(c_4964,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_50,c_50,c_4958]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.10 % Problem : SYN710-1 : TPTP v9.0.0. Released v2.5.0.
% 0.10/0.11 % 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.11/0.30 % Computer : n032.cluster.edu
% 0.11/0.30 % Model : x86_64 x86_64
% 0.11/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.30 % Memory : 8042.1875MB
% 0.11/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.30 % CPULimit : 300
% 0.11/0.30 % WCLimit : 300
% 0.11/0.30 % DateTime : Wed Apr 9 08:12:00 EDT 2025
% 0.11/0.30 % CPUTime :
% 12.63/4.05 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.63/4.06
% 12.63/4.06 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------