%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : LCL131-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 : n026.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:19 AM UTC 2026
% Result : Unsatisfiable 239.80s 173.77s
% Output : CNFRefutation 240.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 3
% Syntax : Number of formulae : 45 ( 23 unt; 0 typ; 0 def)
% Number of atoms : 73 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 58 ( 30 ~; 28 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 5 avg)
% Maximal term depth : 6 ( 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 : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 148 ( 148 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ is_a_theorem > equivalent > #nlpp > e > 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(e,type,
e: $i ).
tff(c,type,
c: $i ).
tff(f_37,axiom,
! [X,Y,Z,U] : is_a_theorem(equivalent(equivalent(X,equivalent(equivalent(equivalent(Y,Z),equivalent(U,Z)),equivalent(Y,U))),X)),
file(unknown,unknown) ).
tff(f_35,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(a,equivalent(a,equivalent(equivalent(b,c),equivalent(equivalent(b,e),equivalent(c,e)))))),
file(unknown,unknown) ).
tff(c_4,plain,
! [X_3,Y_4,Z_5,U_6] : is_a_theorem(equivalent(equivalent(X_3,equivalent(equivalent(equivalent(Y_4,Z_5),equivalent(U_6,Z_5)),equivalent(Y_4,U_6))),X_3)),
inference(cnfTransformation,[status(thm)],[f_37]) ).
tff(c_8,plain,
! [X_9,Y_10,Z_11,U_12] : is_a_theorem(equivalent(equivalent(X_9,equivalent(equivalent(equivalent(Y_10,Z_11),equivalent(U_12,Z_11)),equivalent(Y_10,U_12))),X_9)),
inference(cnfTransformation,[status(thm)],[f_37]) ).
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_35]) ).
tff(c_13,plain,
! [X_13,Y_14,Z_15,U_16] :
( is_a_theorem(X_13)
| ~ is_a_theorem(equivalent(X_13,equivalent(equivalent(equivalent(Y_14,Z_15),equivalent(U_16,Z_15)),equivalent(Y_14,U_16)))) ),
inference(resolution,[status(thm)],[c_8,c_2]) ).
tff(c_18,plain,
! [Y_14,Z_5,U_6,Z_15,Y_4,U_16] : is_a_theorem(equivalent(equivalent(equivalent(equivalent(Y_14,Z_15),equivalent(U_16,Z_15)),equivalent(Y_14,U_16)),equivalent(equivalent(equivalent(Y_4,Z_5),equivalent(U_6,Z_5)),equivalent(Y_4,U_6)))),
inference(resolution,[status(thm)],[c_4,c_13]) ).
tff(c_19,plain,
! [U_19,Z_17,Z_20,Y_22,U_21,Y_18] : is_a_theorem(equivalent(equivalent(equivalent(equivalent(Y_18,Z_17),equivalent(U_19,Z_17)),equivalent(Y_18,U_19)),equivalent(equivalent(equivalent(Y_22,Z_20),equivalent(U_21,Z_20)),equivalent(Y_22,U_21)))),
inference(resolution,[status(thm)],[c_4,c_13]) ).
tff(c_12,plain,
! [X_9,Y_10,Z_11,U_12] :
( is_a_theorem(X_9)
| ~ is_a_theorem(equivalent(X_9,equivalent(equivalent(equivalent(Y_10,Z_11),equivalent(U_12,Z_11)),equivalent(Y_10,U_12)))) ),
inference(resolution,[status(thm)],[c_8,c_2]) ).
tff(c_28,plain,
! [Y_23,Z_24,U_25] : is_a_theorem(equivalent(equivalent(equivalent(Y_23,Z_24),equivalent(U_25,Z_24)),equivalent(Y_23,U_25))),
inference(resolution,[status(thm)],[c_19,c_12]) ).
tff(c_38,plain,
! [Y_26,U_27,Z_28] :
( is_a_theorem(equivalent(Y_26,U_27))
| ~ is_a_theorem(equivalent(equivalent(Y_26,Z_28),equivalent(U_27,Z_28))) ),
inference(resolution,[status(thm)],[c_28,c_2]) ).
tff(c_47,plain,
! [Y_4,Z_15,U_6,Z_5] : is_a_theorem(equivalent(equivalent(equivalent(Y_4,Z_15),equivalent(U_6,Z_15)),equivalent(equivalent(Y_4,Z_5),equivalent(U_6,Z_5)))),
inference(resolution,[status(thm)],[c_18,c_38]) ).
tff(c_50,plain,
! [Y_29,Z_30,U_31,Z_32] : is_a_theorem(equivalent(equivalent(equivalent(equivalent(Y_29,Z_30),equivalent(U_31,Z_30)),Z_32),equivalent(equivalent(Y_29,U_31),Z_32))),
inference(resolution,[status(thm)],[c_28,c_12]) ).
tff(c_75,plain,
! [Y_37,U_38,Z_39,Z_40] :
( is_a_theorem(equivalent(equivalent(Y_37,U_38),Z_39))
| ~ is_a_theorem(equivalent(equivalent(equivalent(Y_37,Z_40),equivalent(U_38,Z_40)),Z_39)) ),
inference(resolution,[status(thm)],[c_50,c_2]) ).
tff(c_138,plain,
! [Y_44,U_45,Z_46] : is_a_theorem(equivalent(equivalent(Y_44,U_45),equivalent(equivalent(Y_44,Z_46),equivalent(U_45,Z_46)))),
inference(resolution,[status(thm)],[c_47,c_75]) ).
tff(c_147,plain,
! [Y_44,Z_46,U_45] :
( is_a_theorem(equivalent(equivalent(Y_44,Z_46),equivalent(U_45,Z_46)))
| ~ is_a_theorem(equivalent(Y_44,U_45)) ),
inference(resolution,[status(thm)],[c_138,c_2]) ).
tff(c_65,plain,
! [Y_33,Z_34,U_35,Z_36] : is_a_theorem(equivalent(equivalent(equivalent(Y_33,Z_34),equivalent(U_35,Z_34)),equivalent(equivalent(Y_33,Z_36),equivalent(U_35,Z_36)))),
inference(resolution,[status(thm)],[c_18,c_38]) ).
tff(c_37,plain,
! [Y_23,U_25,Z_24] :
( is_a_theorem(equivalent(Y_23,U_25))
| ~ is_a_theorem(equivalent(equivalent(Y_23,Z_24),equivalent(U_25,Z_24))) ),
inference(resolution,[status(thm)],[c_28,c_2]) ).
tff(c_94,plain,
! [Y_41,Z_42] : is_a_theorem(equivalent(equivalent(Y_41,Z_42),equivalent(Y_41,Z_42))),
inference(resolution,[status(thm)],[c_65,c_37]) ).
tff(c_110,plain,
! [Y_41] : is_a_theorem(equivalent(Y_41,Y_41)),
inference(resolution,[status(thm)],[c_94,c_37]) ).
tff(c_151,plain,
! [Y_47,Z_48,U_49] :
( is_a_theorem(equivalent(equivalent(Y_47,Z_48),equivalent(U_49,Z_48)))
| ~ is_a_theorem(equivalent(Y_47,U_49)) ),
inference(resolution,[status(thm)],[c_138,c_2]) ).
tff(c_171,plain,
! [U_50,Z_51,Y_52] :
( is_a_theorem(equivalent(U_50,Z_51))
| ~ is_a_theorem(equivalent(Y_52,Z_51))
| ~ is_a_theorem(equivalent(Y_52,U_50)) ),
inference(resolution,[status(thm)],[c_151,c_2]) ).
tff(c_222,plain,
! [U_57,Y_58] :
( is_a_theorem(equivalent(U_57,Y_58))
| ~ is_a_theorem(equivalent(Y_58,U_57)) ),
inference(resolution,[status(thm)],[c_110,c_171]) ).
tff(c_239,plain,
! [U_45,Z_46,Y_44] :
( is_a_theorem(equivalent(equivalent(U_45,Z_46),equivalent(Y_44,Z_46)))
| ~ is_a_theorem(equivalent(Y_44,U_45)) ),
inference(resolution,[status(thm)],[c_147,c_222]) ).
tff(c_93,plain,
! [Y_37,Y_4,Z_5,U_6] : is_a_theorem(equivalent(equivalent(Y_37,equivalent(equivalent(Y_4,Z_5),equivalent(U_6,Z_5))),equivalent(Y_37,equivalent(Y_4,U_6)))),
inference(resolution,[status(thm)],[c_4,c_75]) ).
tff(c_26,plain,
! [Y_18,Z_17,U_19] : is_a_theorem(equivalent(equivalent(equivalent(Y_18,Z_17),equivalent(U_19,Z_17)),equivalent(Y_18,U_19))),
inference(resolution,[status(thm)],[c_19,c_12]) ).
tff(c_51250,plain,
! [U_879,Y_880,U_881,Z_882] :
( is_a_theorem(equivalent(U_879,equivalent(Y_880,U_881)))
| ~ is_a_theorem(equivalent(equivalent(equivalent(Y_880,Z_882),equivalent(U_881,Z_882)),U_879)) ),
inference(resolution,[status(thm)],[c_26,c_171]) ).
tff(c_51930,plain,
! [Y_880,U_6,Z_5,Y_4] : is_a_theorem(equivalent(equivalent(equivalent(Y_880,equivalent(U_6,Z_5)),equivalent(Y_4,U_6)),equivalent(Y_880,equivalent(Y_4,Z_5)))),
inference(resolution,[status(thm)],[c_93,c_51250]) ).
tff(c_423,plain,
! [Y_80,Y_81,Z_82,U_83] : is_a_theorem(equivalent(equivalent(Y_80,equivalent(equivalent(Y_81,Z_82),equivalent(U_83,Z_82))),equivalent(Y_80,equivalent(Y_81,U_83)))),
inference(resolution,[status(thm)],[c_4,c_75]) ).
tff(c_64,plain,
! [Y_29,U_31,Z_32,Z_30] :
( is_a_theorem(equivalent(equivalent(Y_29,U_31),Z_32))
| ~ is_a_theorem(equivalent(equivalent(equivalent(Y_29,Z_30),equivalent(U_31,Z_30)),Z_32)) ),
inference(resolution,[status(thm)],[c_50,c_2]) ).
tff(c_555,plain,
! [Y_96,Y_97,Z_98,U_99] : is_a_theorem(equivalent(equivalent(Y_96,equivalent(Y_97,Z_98)),equivalent(equivalent(Y_96,equivalent(U_99,Z_98)),equivalent(Y_97,U_99)))),
inference(resolution,[status(thm)],[c_423,c_64]) ).
tff(c_308,plain,
! [Y_65,Z_66,Z_67,U_68] : is_a_theorem(equivalent(equivalent(equivalent(equivalent(Y_65,Z_66),Z_67),equivalent(equivalent(U_68,Z_66),Z_67)),equivalent(Y_65,U_68))),
inference(resolution,[status(thm)],[c_50,c_12]) ).
tff(c_331,plain,
! [Y_65,U_68,Z_66,Z_67] :
( is_a_theorem(equivalent(Y_65,U_68))
| ~ is_a_theorem(equivalent(equivalent(equivalent(Y_65,Z_66),Z_67),equivalent(equivalent(U_68,Z_66),Z_67))) ),
inference(resolution,[status(thm)],[c_308,c_2]) ).
tff(c_599,plain,
! [Y_100,U_101] : is_a_theorem(equivalent(Y_100,equivalent(Y_100,equivalent(U_101,U_101)))),
inference(resolution,[status(thm)],[c_555,c_331]) ).
tff(c_169,plain,
! [U_49,Z_48,Y_47] :
( is_a_theorem(equivalent(U_49,Z_48))
| ~ is_a_theorem(equivalent(Y_47,Z_48))
| ~ is_a_theorem(equivalent(Y_47,U_49)) ),
inference(resolution,[status(thm)],[c_151,c_2]) ).
tff(c_644,plain,
! [U_49,Y_100,U_101] :
( is_a_theorem(equivalent(U_49,equivalent(Y_100,equivalent(U_101,U_101))))
| ~ is_a_theorem(equivalent(Y_100,U_49)) ),
inference(resolution,[status(thm)],[c_599,c_169]) ).
tff(c_945,plain,
! [Y_115,U_116,Z_117,Y_118] :
( is_a_theorem(equivalent(equivalent(Y_115,equivalent(U_116,Z_117)),equivalent(Y_118,U_116)))
| ~ is_a_theorem(equivalent(Y_115,equivalent(Y_118,Z_117))) ),
inference(resolution,[status(thm)],[c_555,c_2]) ).
tff(c_4901,plain,
! [Y_237,U_238,Y_239,Z_240] :
( is_a_theorem(equivalent(Y_237,U_238))
| ~ is_a_theorem(equivalent(Y_239,equivalent(U_238,Z_240)))
| ~ is_a_theorem(equivalent(Y_239,equivalent(Y_237,Z_240))) ),
inference(resolution,[status(thm)],[c_945,c_2]) ).
tff(c_66630,plain,
! [Y_1021,Y_1022,U_1023,U_1024] :
( is_a_theorem(equivalent(Y_1021,Y_1022))
| ~ is_a_theorem(equivalent(U_1023,equivalent(Y_1021,equivalent(U_1024,U_1024))))
| ~ is_a_theorem(equivalent(Y_1022,U_1023)) ),
inference(resolution,[status(thm)],[c_644,c_4901]) ).
tff(c_306240,plain,
! [Y_2360,Y_2361,U_2362,Z_2363] :
( is_a_theorem(equivalent(Y_2360,Y_2361))
| ~ is_a_theorem(equivalent(Y_2361,equivalent(equivalent(Y_2360,equivalent(U_2362,Z_2363)),equivalent(Z_2363,U_2362)))) ),
inference(resolution,[status(thm)],[c_51930,c_66630]) ).
tff(c_449757,plain,
! [Y_2920,U_2921,Z_2922,U_2923] :
( is_a_theorem(equivalent(Y_2920,equivalent(U_2921,equivalent(Z_2922,U_2923))))
| ~ is_a_theorem(equivalent(equivalent(Y_2920,equivalent(U_2923,Z_2922)),U_2921)) ),
inference(resolution,[status(thm)],[c_239,c_306240]) ).
tff(c_451839,plain,
! [X_3,Y_4,U_6,Z_5] : is_a_theorem(equivalent(X_3,equivalent(X_3,equivalent(equivalent(Y_4,U_6),equivalent(equivalent(Y_4,Z_5),equivalent(U_6,Z_5)))))),
inference(resolution,[status(thm)],[c_4,c_449757]) ).
tff(c_6,plain,
~ is_a_theorem(equivalent(a,equivalent(a,equivalent(equivalent(b,c),equivalent(equivalent(b,e),equivalent(c,e)))))),
inference(cnfTransformation,[status(thm)],[f_39]) ).
tff(c_458052,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_451839,c_6]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL131-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.37 % Computer : n026.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % 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 05:44:10 UTC 2026
% 0.11/0.37 % CPUTime :
% 239.80/173.77 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 239.80/173.78
% 239.80/173.78 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------