%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : LCL010-1 : TPTP v9.3.1. Released v1.0.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 : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 11:11:04 AM UTC 2026
% Result : Unsatisfiable 183.04s 150.96s
% Output : CNFRefutation 183.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 3
% Syntax : Number of formulae : 36 ( 10 unt; 0 typ; 0 def)
% Number of atoms : 73 ( 0 equ)
% Maximal formula atoms : 3 ( 2 avg)
% Number of connectives : 76 ( 39 ~; 37 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 6 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 4 ( 4 usr; 3 con; 0-2 aty)
% Number of variables : 112 ( 112 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ is_a_theorem > equivalent > #nlpp > c > b > a
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(a,type,
a: $i ).
tff(is_a_theorem,type,
is_a_theorem: $i > $o ).
tff(b,type,
b: $i ).
tff(equivalent,type,
equivalent: ( $i * $i ) > $i ).
tff(c,type,
c: $i ).
tff(f_36,axiom,
! [X,Y,Z] : is_a_theorem(equivalent(equivalent(X,Y),equivalent(equivalent(X,Z),equivalent(Z,Y)))),
file(unknown,unknown) ).
tff(f_33,axiom,
! [X,Y] :
( ~ is_a_theorem(equivalent(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ),
file(unknown,unknown) ).
tff(f_39,axiom,
~ is_a_theorem(equivalent(equivalent(a,b),equivalent(equivalent(c,b),equivalent(a,c)))),
file(unknown,unknown) ).
tff(c_4,plain,
! [X_3,Y_4,Z_5] : is_a_theorem(equivalent(equivalent(X_3,Y_4),equivalent(equivalent(X_3,Z_5),equivalent(Z_5,Y_4)))),
inference(cnfTransformation,[status(thm)],[f_36]) ).
tff(c_8,plain,
! [X_8,Y_9,Z_10] : is_a_theorem(equivalent(equivalent(X_8,Y_9),equivalent(equivalent(X_8,Z_10),equivalent(Z_10,Y_9)))),
inference(cnfTransformation,[status(thm)],[f_36]) ).
tff(c_2,plain,
! [Y_2,X_1] :
( is_a_theorem(Y_2)
| ~ is_a_theorem(X_1)
| ~ is_a_theorem(equivalent(X_1,Y_2)) ),
inference(cnfTransformation,[status(thm)],[f_33]) ).
tff(c_13,plain,
! [X_11,Z_12,Y_13] :
( is_a_theorem(equivalent(equivalent(X_11,Z_12),equivalent(Z_12,Y_13)))
| ~ is_a_theorem(equivalent(X_11,Y_13)) ),
inference(resolution,[status(thm)],[c_8,c_2]) ).
tff(c_18,plain,
! [Z_14,Y_15,X_16] :
( is_a_theorem(equivalent(Z_14,Y_15))
| ~ is_a_theorem(equivalent(X_16,Z_14))
| ~ is_a_theorem(equivalent(X_16,Y_15)) ),
inference(resolution,[status(thm)],[c_13,c_2]) ).
tff(c_24,plain,
! [X_3,Z_5,Y_4,Y_15] :
( is_a_theorem(equivalent(equivalent(equivalent(X_3,Z_5),equivalent(Z_5,Y_4)),Y_15))
| ~ is_a_theorem(equivalent(equivalent(X_3,Y_4),Y_15)) ),
inference(resolution,[status(thm)],[c_4,c_18]) ).
tff(c_32,plain,
! [X_21,Z_22,Y_23,Y_24] :
( is_a_theorem(equivalent(equivalent(equivalent(X_21,Z_22),equivalent(Z_22,Y_23)),Y_24))
| ~ is_a_theorem(equivalent(equivalent(X_21,Y_23),Y_24)) ),
inference(resolution,[status(thm)],[c_4,c_18]) ).
tff(c_54,plain,
! [Y_29,X_30,Z_31,Y_32] :
( is_a_theorem(Y_29)
| ~ is_a_theorem(equivalent(equivalent(X_30,Z_31),equivalent(Z_31,Y_32)))
| ~ is_a_theorem(equivalent(equivalent(X_30,Y_32),Y_29)) ),
inference(resolution,[status(thm)],[c_32,c_2]) ).
tff(c_70,plain,
! [Y_33,X_34,Z_35] :
( is_a_theorem(Y_33)
| ~ is_a_theorem(equivalent(equivalent(X_34,equivalent(Z_35,equivalent(X_34,Z_35))),Y_33)) ),
inference(resolution,[status(thm)],[c_4,c_54]) ).
tff(c_108,plain,
! [Y_39,X_40,Z_41] :
( is_a_theorem(Y_39)
| ~ is_a_theorem(equivalent(equivalent(X_40,equivalent(equivalent(X_40,Z_41),Z_41)),Y_39)) ),
inference(resolution,[status(thm)],[c_24,c_70]) ).
tff(c_123,plain,
! [X_3,Z_5,Z_41] : is_a_theorem(equivalent(equivalent(X_3,Z_5),equivalent(Z_5,equivalent(equivalent(X_3,Z_41),Z_41)))),
inference(resolution,[status(thm)],[c_4,c_108]) ).
tff(c_12,plain,
! [X_8,Z_10,Y_9] :
( is_a_theorem(equivalent(equivalent(X_8,Z_10),equivalent(Z_10,Y_9)))
| ~ is_a_theorem(equivalent(X_8,Y_9)) ),
inference(resolution,[status(thm)],[c_8,c_2]) ).
tff(c_23,plain,
! [Z_10,Y_9,Y_15,X_8] :
( is_a_theorem(equivalent(equivalent(Z_10,Y_9),Y_15))
| ~ is_a_theorem(equivalent(equivalent(X_8,Z_10),Y_15))
| ~ is_a_theorem(equivalent(X_8,Y_9)) ),
inference(resolution,[status(thm)],[c_12,c_18]) ).
tff(c_408,plain,
! [Y_64,Y_65,Z_68,X_66,Y_67] :
( is_a_theorem(equivalent(equivalent(equivalent(Z_68,Y_64),Y_65),Y_67))
| ~ is_a_theorem(equivalent(equivalent(X_66,Z_68),Y_65))
| ~ is_a_theorem(equivalent(equivalent(X_66,Y_64),Y_67)) ),
inference(resolution,[status(thm)],[c_32,c_23]) ).
tff(c_3650,plain,
! [Y_199,Y_196,X_197,Y_200,Z_198] :
( is_a_theorem(equivalent(equivalent(equivalent(Y_200,Y_199),equivalent(equivalent(X_197,Z_198),equivalent(Z_198,Y_200))),Y_196))
| ~ is_a_theorem(equivalent(equivalent(X_197,Y_199),Y_196)) ),
inference(resolution,[status(thm)],[c_4,c_408]) ).
tff(c_25,plain,
! [Z_17,Y_18,Y_19,X_20] :
( is_a_theorem(equivalent(equivalent(Z_17,Y_18),Y_19))
| ~ is_a_theorem(equivalent(equivalent(X_20,Z_17),Y_19))
| ~ is_a_theorem(equivalent(X_20,Y_18)) ),
inference(resolution,[status(thm)],[c_12,c_18]) ).
tff(c_202,plain,
! [Z_49,Y_50,Y_51,X_52] :
( is_a_theorem(equivalent(equivalent(Z_49,Y_50),equivalent(Z_49,Y_51)))
| ~ is_a_theorem(equivalent(X_52,Y_50))
| ~ is_a_theorem(equivalent(X_52,Y_51)) ),
inference(resolution,[status(thm)],[c_12,c_25]) ).
tff(c_2114,plain,
! [Y_142,X_144,Z_145,Y_146,Z_143] :
( is_a_theorem(equivalent(equivalent(Z_143,equivalent(equivalent(X_144,Z_145),equivalent(Z_145,Y_146))),equivalent(Z_143,Y_142)))
| ~ is_a_theorem(equivalent(equivalent(X_144,Y_146),Y_142)) ),
inference(resolution,[status(thm)],[c_4,c_202]) ).
tff(c_69,plain,
! [Y_29,X_3,Z_5] :
( is_a_theorem(Y_29)
| ~ is_a_theorem(equivalent(equivalent(X_3,equivalent(Z_5,equivalent(X_3,Z_5))),Y_29)) ),
inference(resolution,[status(thm)],[c_4,c_54]) ).
tff(c_2178,plain,
! [Z_145,Y_142,X_144] :
( is_a_theorem(equivalent(Z_145,Y_142))
| ~ is_a_theorem(equivalent(equivalent(X_144,equivalent(X_144,Z_145)),Y_142)) ),
inference(resolution,[status(thm)],[c_2114,c_69]) ).
tff(c_3735,plain,
! [Z_201,X_202,Y_203] :
( is_a_theorem(equivalent(equivalent(Z_201,X_202),Y_203))
| ~ is_a_theorem(equivalent(equivalent(X_202,Z_201),Y_203)) ),
inference(resolution,[status(thm)],[c_3650,c_2178]) ).
tff(c_3860,plain,
! [Z_5,X_3,Z_41] : is_a_theorem(equivalent(equivalent(Z_5,X_3),equivalent(Z_5,equivalent(equivalent(X_3,Z_41),Z_41)))),
inference(resolution,[status(thm)],[c_123,c_3735]) ).
tff(c_31,plain,
! [Y_4,Y_18,X_3,Z_5] :
( is_a_theorem(equivalent(equivalent(Y_4,Y_18),equivalent(equivalent(X_3,Z_5),equivalent(Z_5,Y_4))))
| ~ is_a_theorem(equivalent(X_3,Y_18)) ),
inference(resolution,[status(thm)],[c_4,c_25]) ).
tff(c_23170,plain,
! [X_546,Z_547,Y_548,Z_549] :
( is_a_theorem(equivalent(equivalent(X_546,Z_547),equivalent(Z_547,Y_548)))
| ~ is_a_theorem(equivalent(X_546,equivalent(Z_549,equivalent(Y_548,Z_549)))) ),
inference(resolution,[status(thm)],[c_31,c_70]) ).
tff(c_23564,plain,
! [Z_550,X_551,Z_552] : is_a_theorem(equivalent(equivalent(equivalent(Z_550,X_551),Z_552),equivalent(Z_552,equivalent(X_551,Z_550)))),
inference(resolution,[status(thm)],[c_3860,c_23170]) ).
tff(c_89,plain,
! [Z_35,X_8,Y_9] :
( is_a_theorem(equivalent(equivalent(Z_35,equivalent(X_8,Z_35)),Y_9))
| ~ is_a_theorem(equivalent(X_8,Y_9)) ),
inference(resolution,[status(thm)],[c_12,c_70]) ).
tff(c_1569,plain,
! [Y_114,Y_115,Z_116,X_117] :
( is_a_theorem(Y_114)
| ~ is_a_theorem(equivalent(equivalent(Y_115,equivalent(Z_116,Y_115)),Y_114))
| ~ is_a_theorem(equivalent(X_117,equivalent(X_117,Z_116))) ),
inference(resolution,[status(thm)],[c_31,c_54]) ).
tff(c_1862,plain,
! [Y_130,X_131,X_132] :
( is_a_theorem(Y_130)
| ~ is_a_theorem(equivalent(X_131,equivalent(X_131,X_132)))
| ~ is_a_theorem(equivalent(X_132,Y_130)) ),
inference(resolution,[status(thm)],[c_89,c_1569]) ).
tff(c_1916,plain,
! [Y_130,Z_5,X_3] :
( is_a_theorem(Y_130)
| ~ is_a_theorem(equivalent(equivalent(Z_5,X_3),Y_130))
| ~ is_a_theorem(equivalent(X_3,Z_5)) ),
inference(resolution,[status(thm)],[c_31,c_1862]) ).
tff(c_321925,plain,
! [Z_2405,X_2406,Z_2407] :
( is_a_theorem(equivalent(Z_2405,equivalent(X_2406,Z_2407)))
| ~ is_a_theorem(equivalent(Z_2405,equivalent(Z_2407,X_2406))) ),
inference(resolution,[status(thm)],[c_23564,c_1916]) ).
tff(c_323366,plain,
! [X_3,Y_4,Z_5] : is_a_theorem(equivalent(equivalent(X_3,Y_4),equivalent(equivalent(Z_5,Y_4),equivalent(X_3,Z_5)))),
inference(resolution,[status(thm)],[c_4,c_321925]) ).
tff(c_6,plain,
~ is_a_theorem(equivalent(equivalent(a,b),equivalent(equivalent(c,b),equivalent(a,c)))),
inference(cnfTransformation,[status(thm)],[f_39]) ).
tff(c_323370,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_323366,c_6]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL010-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % 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.11/0.36 % Computer : n007.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sat Sep 5 12:37:39 UTC 2026
% 0.11/0.37 % CPUTime :
% 183.04/150.96 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 183.04/150.97
% 183.04/150.97 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------