%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : LCL090-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/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 : n020.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:13 AM UTC 2026
% Result : Unsatisfiable 11.34s 3.90s
% Output : CNFRefutation 11.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 3
% Syntax : Number of formulae : 114 ( 80 unt; 0 typ; 0 def)
% Number of atoms : 153 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 95 ( 56 ~; 39 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 7 ( 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 : 2 ( 2 usr; 1 con; 0-2 aty)
% Number of variables : 360 ( 360 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ is_a_theorem > implies > #nlpp > a
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(a,type,
a: $i ).
tff(is_a_theorem,type,
is_a_theorem: $i > $o ).
tff(implies,type,
implies: ( $i * $i ) > $i ).
tff(f_34,axiom,
! [P,R,S,Q,T] : is_a_theorem(implies(implies(implies(P,Q),implies(R,S)),implies(implies(S,P),implies(T,implies(R,P))))),
file(unknown,unknown) ).
tff(f_32,axiom,
! [X,Y] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X)
| is_a_theorem(Y) ),
file(unknown,unknown) ).
tff(f_36,axiom,
~ is_a_theorem(implies(a,a)),
file(unknown,unknown) ).
tff(c_4,plain,
! [S_5,T_7,P_3,R_4,Q_6] : is_a_theorem(implies(implies(implies(P_3,Q_6),implies(R_4,S_5)),implies(implies(S_5,P_3),implies(T_7,implies(R_4,P_3))))),
inference(cnfTransformation,[status(thm)],[f_34]) ).
tff(c_8,plain,
! [P_14,Q_13,S_11,T_10,R_12] : is_a_theorem(implies(implies(implies(P_14,Q_13),implies(R_12,S_11)),implies(implies(S_11,P_14),implies(T_10,implies(R_12,P_14))))),
inference(cnfTransformation,[status(thm)],[f_34]) ).
tff(c_2,plain,
! [Y_2,X_1] :
( is_a_theorem(Y_2)
| ~ is_a_theorem(X_1)
| ~ is_a_theorem(implies(X_1,Y_2)) ),
inference(cnfTransformation,[status(thm)],[f_32]) ).
tff(c_13,plain,
! [R_18,T_16,P_19,Q_15,S_17] :
( is_a_theorem(implies(implies(S_17,P_19),implies(T_16,implies(R_18,P_19))))
| ~ is_a_theorem(implies(implies(P_19,Q_15),implies(R_18,S_17))) ),
inference(resolution,[status(thm)],[c_8,c_2]) ).
tff(c_16,plain,
! [S_5,T_7,T_16,P_3,R_4,Q_6] : is_a_theorem(implies(implies(implies(T_7,implies(R_4,P_3)),implies(P_3,Q_6)),implies(T_16,implies(implies(S_5,P_3),implies(P_3,Q_6))))),
inference(resolution,[status(thm)],[c_4,c_13]) ).
tff(c_17,plain,
! [T_20,P_25,Q_24,S_21,T_22,R_23] : is_a_theorem(implies(implies(implies(T_20,implies(R_23,P_25)),implies(P_25,Q_24)),implies(T_22,implies(implies(S_21,P_25),implies(P_25,Q_24))))),
inference(resolution,[status(thm)],[c_4,c_13]) ).
tff(c_25,plain,
! [R_26,T_31,T_28,P_29,S_27,Q_30] :
( is_a_theorem(implies(T_31,implies(implies(S_27,P_29),implies(P_29,Q_30))))
| ~ is_a_theorem(implies(implies(T_28,implies(R_26,P_29)),implies(P_29,Q_30))) ),
inference(resolution,[status(thm)],[c_17,c_2]) ).
tff(c_30,plain,
! [T_35,S_33,P_36,T_34,S_32] : is_a_theorem(implies(T_35,implies(implies(S_32,T_34),implies(T_34,implies(implies(S_33,P_36),implies(P_36,T_34)))))),
inference(resolution,[status(thm)],[c_16,c_25]) ).
tff(c_42,plain,
! [T_35,S_33,P_36,T_34,S_32] :
( is_a_theorem(implies(implies(S_32,T_34),implies(T_34,implies(implies(S_33,P_36),implies(P_36,T_34)))))
| ~ is_a_theorem(T_35) ),
inference(resolution,[status(thm)],[c_30,c_2]) ).
tff(c_43,plain,
! [T_35] : ~ is_a_theorem(T_35),
inference(splitLeft,[status(thm)],[c_42]) ).
tff(c_29,plain,
! [S_5,T_31,T_16,S_27,P_3] : is_a_theorem(implies(T_31,implies(implies(S_27,T_16),implies(T_16,implies(implies(S_5,P_3),implies(P_3,T_16)))))),
inference(resolution,[status(thm)],[c_16,c_25]) ).
tff(c_50,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_43,c_29]) ).
tff(c_52,plain,
! [S_37,T_38,S_39,P_40] : is_a_theorem(implies(implies(S_37,T_38),implies(T_38,implies(implies(S_39,P_40),implies(P_40,T_38))))),
inference(splitRight,[status(thm)],[c_42]) ).
tff(c_12,plain,
! [P_14,Q_13,S_11,T_10,R_12] :
( is_a_theorem(implies(implies(S_11,P_14),implies(T_10,implies(R_12,P_14))))
| ~ is_a_theorem(implies(implies(P_14,Q_13),implies(R_12,S_11))) ),
inference(resolution,[status(thm)],[c_8,c_2]) ).
tff(c_73,plain,
! [S_45,T_49,S_47,P_48,T_46] : is_a_theorem(implies(implies(implies(implies(S_47,P_48),implies(P_48,T_49)),S_45),implies(T_46,implies(T_49,S_45)))),
inference(resolution,[status(thm)],[c_52,c_12]) ).
tff(c_24,plain,
! [T_20,P_25,Q_24,S_21,T_22,R_23] :
( is_a_theorem(implies(T_22,implies(implies(S_21,P_25),implies(P_25,Q_24))))
| ~ is_a_theorem(implies(implies(T_20,implies(R_23,P_25)),implies(P_25,Q_24))) ),
inference(resolution,[status(thm)],[c_17,c_2]) ).
tff(c_89,plain,
! [S_51,T_53,T_52,T_54,R_50] : is_a_theorem(implies(T_54,implies(implies(S_51,T_52),implies(T_52,implies(T_53,implies(R_50,T_52)))))),
inference(resolution,[status(thm)],[c_73,c_24]) ).
tff(c_104,plain,
! [S_51,T_53,T_52,T_54,R_50] :
( is_a_theorem(implies(implies(S_51,T_52),implies(T_52,implies(T_53,implies(R_50,T_52)))))
| ~ is_a_theorem(T_54) ),
inference(resolution,[status(thm)],[c_89,c_2]) ).
tff(c_105,plain,
! [T_54] : ~ is_a_theorem(T_54),
inference(splitLeft,[status(thm)],[c_104]) ).
tff(c_85,plain,
! [T_49,S_21,T_22,R_23,T_46] : is_a_theorem(implies(T_22,implies(implies(S_21,T_46),implies(T_46,implies(T_49,implies(R_23,T_46)))))),
inference(resolution,[status(thm)],[c_73,c_24]) ).
tff(c_115,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_105,c_85]) ).
tff(c_134,plain,
! [S_62,T_63,T_64,R_65] : is_a_theorem(implies(implies(S_62,T_63),implies(T_63,implies(T_64,implies(R_65,T_63))))),
inference(splitRight,[status(thm)],[c_104]) ).
tff(c_143,plain,
! [S_62,R_65,T_63,T_10,T_64] : is_a_theorem(implies(implies(implies(T_64,implies(R_65,T_63)),S_62),implies(T_10,implies(T_63,S_62)))),
inference(resolution,[status(thm)],[c_134,c_12]) ).
tff(c_117,plain,
! [S_56,T_58,P_59,R_55,Q_60,T_61,T_57] : is_a_theorem(implies(implies(implies(implies(S_56,P_59),implies(P_59,Q_60)),implies(T_58,implies(R_55,P_59))),implies(T_57,implies(T_61,implies(T_58,implies(R_55,P_59)))))),
inference(resolution,[status(thm)],[c_17,c_12]) ).
tff(c_404,plain,
! [Q_113,T_112,P_114,T_116,T_111,R_117,S_110,T_115] : is_a_theorem(implies(implies(implies(T_115,implies(T_116,implies(R_117,P_114))),implies(implies(S_110,P_114),implies(P_114,Q_113))),implies(T_112,implies(T_111,implies(implies(S_110,P_114),implies(P_114,Q_113)))))),
inference(resolution,[status(thm)],[c_117,c_12]) ).
tff(c_1412,plain,
! [T_232,P_227,S_231,Q_229,T_225,T_233,T_228,T_230,R_226] : is_a_theorem(implies(implies(implies(T_230,implies(implies(S_231,P_227),implies(P_227,Q_229))),implies(T_228,implies(T_233,implies(R_226,P_227)))),implies(T_225,implies(T_232,implies(T_228,implies(T_233,implies(R_226,P_227))))))),
inference(resolution,[status(thm)],[c_404,c_12]) ).
tff(c_3147,plain,
! [T_380,T_382,Q_376,T_379,P_381,T_375,T_378,R_374,S_377] :
( is_a_theorem(implies(T_375,implies(T_378,implies(T_380,implies(T_382,implies(R_374,P_381))))))
| ~ is_a_theorem(implies(implies(T_379,implies(implies(S_377,P_381),implies(P_381,Q_376))),implies(T_380,implies(T_382,implies(R_374,P_381))))) ),
inference(resolution,[status(thm)],[c_1412,c_2]) ).
tff(c_4919,plain,
! [T_475,Q_477,P_478,T_476,T_474,S_479] : is_a_theorem(implies(T_475,implies(T_474,implies(implies(implies(P_478,Q_477),P_478),implies(T_476,implies(implies(S_479,P_478),P_478)))))),
inference(resolution,[status(thm)],[c_4,c_3147]) ).
tff(c_5008,plain,
! [T_475,Q_477,P_478,T_476,T_474,S_479] :
( is_a_theorem(implies(T_474,implies(implies(implies(P_478,Q_477),P_478),implies(T_476,implies(implies(S_479,P_478),P_478)))))
| ~ is_a_theorem(T_475) ),
inference(resolution,[status(thm)],[c_4919,c_2]) ).
tff(c_5072,plain,
! [T_475] : ~ is_a_theorem(T_475),
inference(splitLeft,[status(thm)],[c_5008]) ).
tff(c_103,plain,
! [S_51,T_53,P_14,T_52,T_10,R_50] : is_a_theorem(implies(implies(implies(T_52,implies(T_53,implies(R_50,T_52))),P_14),implies(T_10,implies(implies(S_51,T_52),P_14)))),
inference(resolution,[status(thm)],[c_89,c_12]) ).
tff(c_5152,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_5072,c_103]) ).
tff(c_5154,plain,
! [S_488,T_489,P_486,Q_490,T_487] : is_a_theorem(implies(T_487,implies(implies(implies(P_486,Q_490),P_486),implies(T_489,implies(implies(S_488,P_486),P_486))))),
inference(splitRight,[status(thm)],[c_5008]) ).
tff(c_5258,plain,
! [S_488,T_489,P_486,Q_490,T_487] :
( is_a_theorem(implies(implies(implies(P_486,Q_490),P_486),implies(T_489,implies(implies(S_488,P_486),P_486))))
| ~ is_a_theorem(T_487) ),
inference(resolution,[status(thm)],[c_5154,c_2]) ).
tff(c_5259,plain,
! [T_487] : ~ is_a_theorem(T_487),
inference(splitLeft,[status(thm)],[c_5258]) ).
tff(c_5153,plain,
! [Q_477,P_478,T_476,T_474,S_479] : is_a_theorem(implies(T_474,implies(implies(implies(P_478,Q_477),P_478),implies(T_476,implies(implies(S_479,P_478),P_478))))),
inference(splitRight,[status(thm)],[c_5008]) ).
tff(c_5340,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_5259,c_5153]) ).
tff(c_5342,plain,
! [P_491,Q_492,T_493,S_494] : is_a_theorem(implies(implies(implies(P_491,Q_492),P_491),implies(T_493,implies(implies(S_494,P_491),P_491)))),
inference(splitRight,[status(thm)],[c_5258]) ).
tff(c_5456,plain,
! [T_501,S_502,P_503,Q_504] :
( is_a_theorem(implies(T_501,implies(implies(S_502,P_503),P_503)))
| ~ is_a_theorem(implies(implies(P_503,Q_504),P_503)) ),
inference(resolution,[status(thm)],[c_5342,c_2]) ).
tff(c_5647,plain,
! [T_505,S_506,T_507,S_508] : is_a_theorem(implies(T_505,implies(implies(S_506,implies(T_507,implies(S_508,S_508))),implies(T_507,implies(S_508,S_508))))),
inference(resolution,[status(thm)],[c_143,c_5456]) ).
tff(c_5736,plain,
! [S_506,T_507,S_508,T_505] :
( is_a_theorem(implies(implies(S_506,implies(T_507,implies(S_508,S_508))),implies(T_507,implies(S_508,S_508))))
| ~ is_a_theorem(T_505) ),
inference(resolution,[status(thm)],[c_5647,c_2]) ).
tff(c_5737,plain,
! [T_505] : ~ is_a_theorem(T_505),
inference(splitLeft,[status(thm)],[c_5736]) ).
tff(c_5641,plain,
! [T_501,S_502,T_10,S_62] : is_a_theorem(implies(T_501,implies(implies(S_502,implies(T_10,implies(S_62,S_62))),implies(T_10,implies(S_62,S_62))))),
inference(resolution,[status(thm)],[c_143,c_5456]) ).
tff(c_6043,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_5737,c_5641]) ).
tff(c_6045,plain,
! [S_515,T_516,S_517] : is_a_theorem(implies(implies(S_515,implies(T_516,implies(S_517,S_517))),implies(T_516,implies(S_517,S_517)))),
inference(splitRight,[status(thm)],[c_5736]) ).
tff(c_165,plain,
! [S_73,T_74,R_70,T_71,T_72] : is_a_theorem(implies(implies(implies(T_71,implies(R_70,T_74)),S_73),implies(T_72,implies(T_74,S_73)))),
inference(resolution,[status(thm)],[c_134,c_12]) ).
tff(c_181,plain,
! [T_75,R_78,S_77,T_76,T_79] :
( is_a_theorem(implies(T_79,implies(T_75,S_77)))
| ~ is_a_theorem(implies(implies(T_76,implies(R_78,T_75)),S_77)) ),
inference(resolution,[status(thm)],[c_165,c_2]) ).
tff(c_203,plain,
! [T_84,T_81,T_83,T_80,R_82] : is_a_theorem(implies(T_84,implies(T_81,implies(T_80,implies(T_83,implies(R_82,T_81)))))),
inference(resolution,[status(thm)],[c_143,c_181]) ).
tff(c_2038,plain,
! [T_288,P_291,R_287,T_290,T_286,T_289] : is_a_theorem(implies(implies(implies(T_290,implies(T_286,implies(R_287,T_289))),P_291),implies(T_288,implies(T_289,P_291)))),
inference(resolution,[status(thm)],[c_203,c_12]) ).
tff(c_2077,plain,
! [T_288,P_291,R_287,T_290,T_286,T_289] :
( is_a_theorem(implies(T_288,implies(T_289,P_291)))
| ~ is_a_theorem(implies(implies(T_290,implies(T_286,implies(R_287,T_289))),P_291)) ),
inference(resolution,[status(thm)],[c_2038,c_2]) ).
tff(c_6208,plain,
! [T_521,S_522,T_523] : is_a_theorem(implies(T_521,implies(S_522,implies(T_523,implies(S_522,S_522))))),
inference(resolution,[status(thm)],[c_6045,c_2077]) ).
tff(c_6304,plain,
! [S_522,T_523,T_521] :
( is_a_theorem(implies(S_522,implies(T_523,implies(S_522,S_522))))
| ~ is_a_theorem(T_521) ),
inference(resolution,[status(thm)],[c_6208,c_2]) ).
tff(c_6646,plain,
! [T_521] : ~ is_a_theorem(T_521),
inference(splitLeft,[status(thm)],[c_6304]) ).
tff(c_132,plain,
! [S_56,T_58,P_59,R_55,Q_60,T_61,T_57] :
( is_a_theorem(implies(T_57,implies(T_61,implies(T_58,implies(R_55,P_59)))))
| ~ is_a_theorem(implies(implies(implies(S_56,P_59),implies(P_59,Q_60)),implies(T_58,implies(R_55,P_59)))) ),
inference(resolution,[status(thm)],[c_117,c_2]) ).
tff(c_6114,plain,
! [T_518,T_519,S_520] : is_a_theorem(implies(T_518,implies(T_519,implies(S_520,implies(S_520,S_520))))),
inference(resolution,[status(thm)],[c_6045,c_132]) ).
tff(c_6207,plain,
! [T_519,S_520,T_518] :
( is_a_theorem(implies(T_519,implies(S_520,implies(S_520,S_520))))
| ~ is_a_theorem(T_518) ),
inference(resolution,[status(thm)],[c_6114,c_2]) ).
tff(c_6305,plain,
! [T_518] : ~ is_a_theorem(T_518),
inference(splitLeft,[status(thm)],[c_6207]) ).
tff(c_6100,plain,
! [T_288,S_517,T_516] : is_a_theorem(implies(T_288,implies(S_517,implies(T_516,implies(S_517,S_517))))),
inference(resolution,[status(thm)],[c_6045,c_2077]) ).
tff(c_6394,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6305,c_6100]) ).
tff(c_6396,plain,
! [T_524,S_525] : is_a_theorem(implies(T_524,implies(S_525,implies(S_525,S_525)))),
inference(splitRight,[status(thm)],[c_6207]) ).
tff(c_6500,plain,
! [S_525,T_524] :
( is_a_theorem(implies(S_525,implies(S_525,S_525)))
| ~ is_a_theorem(T_524) ),
inference(resolution,[status(thm)],[c_6396,c_2]) ).
tff(c_6501,plain,
! [T_524] : ~ is_a_theorem(T_524),
inference(splitLeft,[status(thm)],[c_6500]) ).
tff(c_6395,plain,
! [T_519,S_520] : is_a_theorem(implies(T_519,implies(S_520,implies(S_520,S_520)))),
inference(splitRight,[status(thm)],[c_6207]) ).
tff(c_6591,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6501,c_6395]) ).
tff(c_6592,plain,
! [S_525] : is_a_theorem(implies(S_525,implies(S_525,S_525))),
inference(splitRight,[status(thm)],[c_6500]) ).
tff(c_6736,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6646,c_6592]) ).
tff(c_6737,plain,
! [S_522,T_523] : is_a_theorem(implies(S_522,implies(T_523,implies(S_522,S_522)))),
inference(splitRight,[status(thm)],[c_6304]) ).
tff(c_180,plain,
! [S_73,T_74,R_70,T_71,T_72] :
( is_a_theorem(implies(T_72,implies(T_74,S_73)))
| ~ is_a_theorem(implies(implies(T_71,implies(R_70,T_74)),S_73)) ),
inference(resolution,[status(thm)],[c_165,c_2]) ).
tff(c_6798,plain,
! [T_529,S_530,T_531] : is_a_theorem(implies(T_529,implies(implies(S_530,S_530),implies(T_531,implies(S_530,S_530))))),
inference(resolution,[status(thm)],[c_6045,c_180]) ).
tff(c_6891,plain,
! [S_530,T_531,T_529] :
( is_a_theorem(implies(implies(S_530,S_530),implies(T_531,implies(S_530,S_530))))
| ~ is_a_theorem(T_529) ),
inference(resolution,[status(thm)],[c_6798,c_2]) ).
tff(c_7051,plain,
! [T_529] : ~ is_a_theorem(T_529),
inference(splitLeft,[status(thm)],[c_6891]) ).
tff(c_6112,plain,
! [S_517,S_515,T_10,T_516] : is_a_theorem(implies(implies(implies(S_517,S_517),S_515),implies(T_10,implies(T_516,S_515)))),
inference(resolution,[status(thm)],[c_6045,c_12]) ).
tff(c_7145,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_7051,c_6112]) ).
tff(c_7147,plain,
! [S_540,T_541] : is_a_theorem(implies(implies(S_540,S_540),implies(T_541,implies(S_540,S_540)))),
inference(splitRight,[status(thm)],[c_6891]) ).
tff(c_222,plain,
! [T_84,T_81,T_83,T_80,R_82] :
( is_a_theorem(implies(T_81,implies(T_80,implies(T_83,implies(R_82,T_81)))))
| ~ is_a_theorem(T_84) ),
inference(resolution,[status(thm)],[c_203,c_2]) ).
tff(c_223,plain,
! [T_84] : ~ is_a_theorem(T_84),
inference(splitLeft,[status(thm)],[c_222]) ).
tff(c_197,plain,
! [T_75,R_78,T_63,T_79,T_10] : is_a_theorem(implies(T_79,implies(T_75,implies(T_10,implies(T_63,implies(R_78,T_75)))))),
inference(resolution,[status(thm)],[c_143,c_181]) ).
tff(c_236,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_223,c_197]) ).
tff(c_238,plain,
! [T_85,T_86,T_87,R_88] : is_a_theorem(implies(T_85,implies(T_86,implies(T_87,implies(R_88,T_85))))),
inference(splitRight,[status(thm)],[c_222]) ).
tff(c_258,plain,
! [T_89,T_90,R_91,T_92] :
( is_a_theorem(implies(T_89,implies(T_90,implies(R_91,T_92))))
| ~ is_a_theorem(T_92) ),
inference(resolution,[status(thm)],[c_238,c_2]) ).
tff(c_277,plain,
! [T_90,R_91,T_92,T_89] :
( is_a_theorem(implies(T_90,implies(R_91,T_92)))
| ~ is_a_theorem(T_89)
| ~ is_a_theorem(T_92) ),
inference(resolution,[status(thm)],[c_258,c_2]) ).
tff(c_291,plain,
! [T_89] : ~ is_a_theorem(T_89),
inference(splitLeft,[status(thm)],[c_277]) ).
tff(c_237,plain,
! [T_81,T_80,T_83,R_82] : is_a_theorem(implies(T_81,implies(T_80,implies(T_83,implies(R_82,T_81))))),
inference(splitRight,[status(thm)],[c_222]) ).
tff(c_307,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_291,c_237]) ).
tff(c_309,plain,
! [T_100,R_101,T_102] :
( is_a_theorem(implies(T_100,implies(R_101,T_102)))
| ~ is_a_theorem(T_102) ),
inference(splitRight,[status(thm)],[c_277]) ).
tff(c_332,plain,
! [R_101,T_102,T_100] :
( is_a_theorem(implies(R_101,T_102))
| ~ is_a_theorem(T_100)
| ~ is_a_theorem(T_102) ),
inference(resolution,[status(thm)],[c_309,c_2]) ).
tff(c_333,plain,
! [T_100] : ~ is_a_theorem(T_100),
inference(splitLeft,[status(thm)],[c_332]) ).
tff(c_350,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_333,c_237]) ).
tff(c_352,plain,
! [R_103,T_104] :
( is_a_theorem(implies(R_103,T_104))
| ~ is_a_theorem(T_104) ),
inference(splitRight,[status(thm)],[c_332]) ).
tff(c_742,plain,
! [S_163,P_164,T_165,R_166] :
( is_a_theorem(implies(implies(S_163,P_164),implies(T_165,implies(R_166,P_164))))
| ~ is_a_theorem(implies(R_166,S_163)) ),
inference(resolution,[status(thm)],[c_352,c_12]) ).
tff(c_3325,plain,
! [T_393,T_390,P_392,S_389,R_391] :
( is_a_theorem(implies(implies(implies(R_391,P_392),S_389),implies(T_390,implies(T_393,S_389))))
| ~ is_a_theorem(implies(R_391,S_389)) ),
inference(resolution,[status(thm)],[c_742,c_12]) ).
tff(c_3373,plain,
! [T_393,T_390,P_392,S_389,R_391] :
( is_a_theorem(implies(T_390,implies(T_393,S_389)))
| ~ is_a_theorem(implies(implies(R_391,P_392),S_389))
| ~ is_a_theorem(implies(R_391,S_389)) ),
inference(resolution,[status(thm)],[c_3325,c_2]) ).
tff(c_7151,plain,
! [T_390,T_393,T_541,S_540] :
( is_a_theorem(implies(T_390,implies(T_393,implies(T_541,implies(S_540,S_540)))))
| ~ is_a_theorem(implies(S_540,implies(T_541,implies(S_540,S_540)))) ),
inference(resolution,[status(thm)],[c_7147,c_3373]) ).
tff(c_7207,plain,
! [T_542,T_543,T_544,S_545] : is_a_theorem(implies(T_542,implies(T_543,implies(T_544,implies(S_545,S_545))))),
inference(demodulation,[status(thm),theory(equality)],[c_6737,c_7151]) ).
tff(c_7300,plain,
! [T_543,T_544,S_545,T_542] :
( is_a_theorem(implies(T_543,implies(T_544,implies(S_545,S_545))))
| ~ is_a_theorem(T_542) ),
inference(resolution,[status(thm)],[c_7207,c_2]) ).
tff(c_7301,plain,
! [T_542] : ~ is_a_theorem(T_542),
inference(splitLeft,[status(thm)],[c_7300]) ).
tff(c_7184,plain,
! [T_390,T_393,T_541,S_540] : is_a_theorem(implies(T_390,implies(T_393,implies(T_541,implies(S_540,S_540))))),
inference(demodulation,[status(thm),theory(equality)],[c_6737,c_7151]) ).
tff(c_7392,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_7301,c_7184]) ).
tff(c_7399,plain,
! [T_546,T_547,S_548] : is_a_theorem(implies(T_546,implies(T_547,implies(S_548,S_548)))),
inference(splitRight,[status(thm)],[c_7300]) ).
tff(c_7509,plain,
! [T_547,S_548,T_546] :
( is_a_theorem(implies(T_547,implies(S_548,S_548)))
| ~ is_a_theorem(T_546) ),
inference(resolution,[status(thm)],[c_7399,c_2]) ).
tff(c_7510,plain,
! [T_546] : ~ is_a_theorem(T_546),
inference(splitLeft,[status(thm)],[c_7509]) ).
tff(c_7393,plain,
! [T_543,T_544,S_545] : is_a_theorem(implies(T_543,implies(T_544,implies(S_545,S_545)))),
inference(splitRight,[status(thm)],[c_7300]) ).
tff(c_7598,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_7510,c_7393]) ).
tff(c_7845,plain,
! [T_553,S_554] : is_a_theorem(implies(T_553,implies(S_554,S_554))),
inference(splitRight,[status(thm)],[c_7509]) ).
tff(c_7960,plain,
! [S_554,T_553] :
( is_a_theorem(implies(S_554,S_554))
| ~ is_a_theorem(T_553) ),
inference(resolution,[status(thm)],[c_7845,c_2]) ).
tff(c_7961,plain,
! [T_553] : ~ is_a_theorem(T_553),
inference(splitLeft,[status(thm)],[c_7960]) ).
tff(c_7599,plain,
! [T_547,S_548] : is_a_theorem(implies(T_547,implies(S_548,S_548))),
inference(splitRight,[status(thm)],[c_7509]) ).
tff(c_8050,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_7961,c_7599]) ).
tff(c_8051,plain,
! [S_554] : is_a_theorem(implies(S_554,S_554)),
inference(splitRight,[status(thm)],[c_7960]) ).
tff(c_6,plain,
~ is_a_theorem(implies(a,a)),
inference(cnfTransformation,[status(thm)],[f_36]) ).
tff(c_8054,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_8051,c_6]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL090-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/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.09/0.35 % Computer : n020.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Fri Sep 4 23:17:57 UTC 2026
% 0.09/0.35 % CPUTime :
% 11.34/3.90 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.34/3.92
% 11.34/3.92 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------