%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : LCL091-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 : n019.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 12.08s 4.57s
% Output : CNFRefutation 12.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 3
% Syntax : Number of formulae : 135 ( 95 unt; 0 typ; 0 def)
% Number of atoms : 180 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 110 ( 65 ~; 45 |; 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 : 3 ( 3 usr; 2 con; 0-2 aty)
% Number of variables : 424 ( 424 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ is_a_theorem > implies > #nlpp > 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(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,implies(b,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_412,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_1378,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_412,c_12]) ).
tff(c_2826,plain,
! [S_361,P_365,T_363,T_366,T_359,Q_360,R_358,T_364,T_362] :
( is_a_theorem(implies(T_359,implies(T_362,implies(T_364,implies(T_366,implies(R_358,P_365))))))
| ~ is_a_theorem(implies(implies(T_363,implies(implies(S_361,P_365),implies(P_365,Q_360))),implies(T_364,implies(T_366,implies(R_358,P_365))))) ),
inference(resolution,[status(thm)],[c_1378,c_2]) ).
tff(c_4406,plain,
! [T_435,T_434,P_439,T_437,Q_438,S_436] : is_a_theorem(implies(T_437,implies(T_435,implies(implies(implies(P_439,Q_438),P_439),implies(T_434,implies(implies(S_436,P_439),P_439)))))),
inference(resolution,[status(thm)],[c_4,c_2826]) ).
tff(c_4495,plain,
! [T_435,T_434,P_439,T_437,Q_438,S_436] :
( is_a_theorem(implies(T_435,implies(implies(implies(P_439,Q_438),P_439),implies(T_434,implies(implies(S_436,P_439),P_439)))))
| ~ is_a_theorem(T_437) ),
inference(resolution,[status(thm)],[c_4406,c_2]) ).
tff(c_4647,plain,
! [T_437] : ~ is_a_theorem(T_437),
inference(splitLeft,[status(thm)],[c_4495]) ).
tff(c_1047,plain,
! [T_204,T_207,Q_203,T_206,R_200,P_201,T_202,S_205] :
( is_a_theorem(implies(T_206,implies(T_204,implies(implies(S_205,P_201),implies(P_201,Q_203)))))
| ~ is_a_theorem(implies(implies(T_202,implies(T_207,implies(R_200,P_201))),implies(implies(S_205,P_201),implies(P_201,Q_203)))) ),
inference(resolution,[status(thm)],[c_412,c_2]) ).
tff(c_1149,plain,
! [T_204,T_206,R_200,T_7,R_4] : is_a_theorem(implies(T_206,implies(T_204,implies(implies(implies(R_200,T_7),T_7),implies(T_7,implies(R_4,T_7)))))),
inference(resolution,[status(thm)],[c_4,c_1047]) ).
tff(c_2909,plain,
! [T_204,T_359,R_200,T_7,T_362,R_4] : is_a_theorem(implies(T_359,implies(T_362,implies(T_204,implies(implies(implies(R_200,T_7),T_7),implies(T_7,implies(R_4,T_7))))))),
inference(resolution,[status(thm)],[c_1149,c_2826]) ).
tff(c_4726,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_4647,c_2909]) ).
tff(c_4728,plain,
! [Q_456,T_460,S_457,T_458,P_459] : is_a_theorem(implies(T_460,implies(implies(implies(P_459,Q_456),P_459),implies(T_458,implies(implies(S_457,P_459),P_459))))),
inference(splitRight,[status(thm)],[c_4495]) ).
tff(c_4832,plain,
! [Q_456,T_460,S_457,T_458,P_459] :
( is_a_theorem(implies(implies(implies(P_459,Q_456),P_459),implies(T_458,implies(implies(S_457,P_459),P_459))))
| ~ is_a_theorem(T_460) ),
inference(resolution,[status(thm)],[c_4728,c_2]) ).
tff(c_4833,plain,
! [T_460] : ~ is_a_theorem(T_460),
inference(splitLeft,[status(thm)],[c_4832]) ).
tff(c_4727,plain,
! [T_435,T_434,P_439,Q_438,S_436] : is_a_theorem(implies(T_435,implies(implies(implies(P_439,Q_438),P_439),implies(T_434,implies(implies(S_436,P_439),P_439))))),
inference(splitRight,[status(thm)],[c_4495]) ).
tff(c_4912,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_4833,c_4727]) ).
tff(c_4914,plain,
! [P_461,Q_462,T_463,S_464] : is_a_theorem(implies(implies(implies(P_461,Q_462),P_461),implies(T_463,implies(implies(S_464,P_461),P_461)))),
inference(splitRight,[status(thm)],[c_4832]) ).
tff(c_5028,plain,
! [T_471,S_472,P_473,Q_474] :
( is_a_theorem(implies(T_471,implies(implies(S_472,P_473),P_473)))
| ~ is_a_theorem(implies(implies(P_473,Q_474),P_473)) ),
inference(resolution,[status(thm)],[c_4914,c_2]) ).
tff(c_5211,plain,
! [T_475,S_476,T_477,S_478] : is_a_theorem(implies(T_475,implies(implies(S_476,implies(T_477,implies(S_478,S_478))),implies(T_477,implies(S_478,S_478))))),
inference(resolution,[status(thm)],[c_143,c_5028]) ).
tff(c_5300,plain,
! [S_476,T_477,S_478,T_475] :
( is_a_theorem(implies(implies(S_476,implies(T_477,implies(S_478,S_478))),implies(T_477,implies(S_478,S_478))))
| ~ is_a_theorem(T_475) ),
inference(resolution,[status(thm)],[c_5211,c_2]) ).
tff(c_5301,plain,
! [T_475] : ~ is_a_theorem(T_475),
inference(splitLeft,[status(thm)],[c_5300]) ).
tff(c_5205,plain,
! [T_471,S_472,T_10,S_62] : is_a_theorem(implies(T_471,implies(implies(S_472,implies(T_10,implies(S_62,S_62))),implies(T_10,implies(S_62,S_62))))),
inference(resolution,[status(thm)],[c_143,c_5028]) ).
tff(c_5385,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_5301,c_5205]) ).
tff(c_5387,plain,
! [S_479,T_480,S_481] : is_a_theorem(implies(implies(S_479,implies(T_480,implies(S_481,S_481))),implies(T_480,implies(S_481,S_481)))),
inference(splitRight,[status(thm)],[c_5300]) ).
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_1611,plain,
! [T_253,T_255,R_252,P_256,T_251,T_254] : is_a_theorem(implies(implies(implies(T_255,implies(T_251,implies(R_252,T_254))),P_256),implies(T_253,implies(T_254,P_256)))),
inference(resolution,[status(thm)],[c_203,c_12]) ).
tff(c_1646,plain,
! [T_253,T_255,R_252,P_256,T_251,T_254] :
( is_a_theorem(implies(T_253,implies(T_254,P_256)))
| ~ is_a_theorem(implies(implies(T_255,implies(T_251,implies(R_252,T_254))),P_256)) ),
inference(resolution,[status(thm)],[c_1611,c_2]) ).
tff(c_5550,plain,
! [T_485,S_486,T_487] : is_a_theorem(implies(T_485,implies(S_486,implies(T_487,implies(S_486,S_486))))),
inference(resolution,[status(thm)],[c_5387,c_1646]) ).
tff(c_5646,plain,
! [S_486,T_487,T_485] :
( is_a_theorem(implies(S_486,implies(T_487,implies(S_486,S_486))))
| ~ is_a_theorem(T_485) ),
inference(resolution,[status(thm)],[c_5550,c_2]) ).
tff(c_5984,plain,
! [T_485] : ~ is_a_theorem(T_485),
inference(splitLeft,[status(thm)],[c_5646]) ).
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_5456,plain,
! [T_482,T_483,S_484] : is_a_theorem(implies(T_482,implies(T_483,implies(S_484,implies(S_484,S_484))))),
inference(resolution,[status(thm)],[c_5387,c_132]) ).
tff(c_5549,plain,
! [T_483,S_484,T_482] :
( is_a_theorem(implies(T_483,implies(S_484,implies(S_484,S_484))))
| ~ is_a_theorem(T_482) ),
inference(resolution,[status(thm)],[c_5456,c_2]) ).
tff(c_5647,plain,
! [T_482] : ~ is_a_theorem(T_482),
inference(splitLeft,[status(thm)],[c_5549]) ).
tff(c_5442,plain,
! [T_253,S_481,T_480] : is_a_theorem(implies(T_253,implies(S_481,implies(T_480,implies(S_481,S_481))))),
inference(resolution,[status(thm)],[c_5387,c_1646]) ).
tff(c_5734,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_5647,c_5442]) ).
tff(c_5736,plain,
! [T_488,S_489] : is_a_theorem(implies(T_488,implies(S_489,implies(S_489,S_489)))),
inference(splitRight,[status(thm)],[c_5549]) ).
tff(c_5840,plain,
! [S_489,T_488] :
( is_a_theorem(implies(S_489,implies(S_489,S_489)))
| ~ is_a_theorem(T_488) ),
inference(resolution,[status(thm)],[c_5736,c_2]) ).
tff(c_5841,plain,
! [T_488] : ~ is_a_theorem(T_488),
inference(splitLeft,[status(thm)],[c_5840]) ).
tff(c_5735,plain,
! [T_483,S_484] : is_a_theorem(implies(T_483,implies(S_484,implies(S_484,S_484)))),
inference(splitRight,[status(thm)],[c_5549]) ).
tff(c_5929,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_5841,c_5735]) ).
tff(c_5930,plain,
! [S_489] : is_a_theorem(implies(S_489,implies(S_489,S_489))),
inference(splitRight,[status(thm)],[c_5840]) ).
tff(c_6072,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_5984,c_5930]) ).
tff(c_6073,plain,
! [S_486,T_487] : is_a_theorem(implies(S_486,implies(T_487,implies(S_486,S_486)))),
inference(splitRight,[status(thm)],[c_5646]) ).
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_6134,plain,
! [T_493,S_494,T_495] : is_a_theorem(implies(T_493,implies(implies(S_494,S_494),implies(T_495,implies(S_494,S_494))))),
inference(resolution,[status(thm)],[c_5387,c_180]) ).
tff(c_6227,plain,
! [S_494,T_495,T_493] :
( is_a_theorem(implies(implies(S_494,S_494),implies(T_495,implies(S_494,S_494))))
| ~ is_a_theorem(T_493) ),
inference(resolution,[status(thm)],[c_6134,c_2]) ).
tff(c_6387,plain,
! [T_493] : ~ is_a_theorem(T_493),
inference(splitLeft,[status(thm)],[c_6227]) ).
tff(c_5454,plain,
! [S_481,S_479,T_10,T_480] : is_a_theorem(implies(implies(implies(S_481,S_481),S_479),implies(T_10,implies(T_480,S_479)))),
inference(resolution,[status(thm)],[c_5387,c_12]) ).
tff(c_6479,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6387,c_5454]) ).
tff(c_6481,plain,
! [S_504,T_505] : is_a_theorem(implies(implies(S_504,S_504),implies(T_505,implies(S_504,S_504)))),
inference(splitRight,[status(thm)],[c_6227]) ).
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_335,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_337,plain,
! [T_100] : ~ is_a_theorem(T_100),
inference(splitLeft,[status(thm)],[c_335]) ).
tff(c_354,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_337,c_237]) ).
tff(c_356,plain,
! [R_103,T_104] :
( is_a_theorem(implies(R_103,T_104))
| ~ is_a_theorem(T_104) ),
inference(splitRight,[status(thm)],[c_335]) ).
tff(c_749,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_356,c_12]) ).
tff(c_3270,plain,
! [P_387,T_388,T_385,S_384,R_386] :
( is_a_theorem(implies(implies(implies(R_386,P_387),S_384),implies(T_385,implies(T_388,S_384))))
| ~ is_a_theorem(implies(R_386,S_384)) ),
inference(resolution,[status(thm)],[c_749,c_12]) ).
tff(c_3318,plain,
! [P_387,T_388,T_385,S_384,R_386] :
( is_a_theorem(implies(T_385,implies(T_388,S_384)))
| ~ is_a_theorem(implies(implies(R_386,P_387),S_384))
| ~ is_a_theorem(implies(R_386,S_384)) ),
inference(resolution,[status(thm)],[c_3270,c_2]) ).
tff(c_6485,plain,
! [T_385,T_388,T_505,S_504] :
( is_a_theorem(implies(T_385,implies(T_388,implies(T_505,implies(S_504,S_504)))))
| ~ is_a_theorem(implies(S_504,implies(T_505,implies(S_504,S_504)))) ),
inference(resolution,[status(thm)],[c_6481,c_3318]) ).
tff(c_6541,plain,
! [T_506,T_507,T_508,S_509] : is_a_theorem(implies(T_506,implies(T_507,implies(T_508,implies(S_509,S_509))))),
inference(demodulation,[status(thm),theory(equality)],[c_6073,c_6485]) ).
tff(c_6634,plain,
! [T_507,T_508,S_509,T_506] :
( is_a_theorem(implies(T_507,implies(T_508,implies(S_509,S_509))))
| ~ is_a_theorem(T_506) ),
inference(resolution,[status(thm)],[c_6541,c_2]) ).
tff(c_6635,plain,
! [T_506] : ~ is_a_theorem(T_506),
inference(splitLeft,[status(thm)],[c_6634]) ).
tff(c_6518,plain,
! [T_385,T_388,T_505,S_504] : is_a_theorem(implies(T_385,implies(T_388,implies(T_505,implies(S_504,S_504))))),
inference(demodulation,[status(thm),theory(equality)],[c_6073,c_6485]) ).
tff(c_6724,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6635,c_6518]) ).
tff(c_6731,plain,
! [T_510,T_511,S_512] : is_a_theorem(implies(T_510,implies(T_511,implies(S_512,S_512)))),
inference(splitRight,[status(thm)],[c_6634]) ).
tff(c_6841,plain,
! [T_511,S_512,T_510] :
( is_a_theorem(implies(T_511,implies(S_512,S_512)))
| ~ is_a_theorem(T_510) ),
inference(resolution,[status(thm)],[c_6731,c_2]) ).
tff(c_6842,plain,
! [T_510] : ~ is_a_theorem(T_510),
inference(splitLeft,[status(thm)],[c_6841]) ).
tff(c_6725,plain,
! [T_507,T_508,S_509] : is_a_theorem(implies(T_507,implies(T_508,implies(S_509,S_509)))),
inference(splitRight,[status(thm)],[c_6634]) ).
tff(c_6928,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_6842,c_6725]) ).
tff(c_7167,plain,
! [T_517,S_518] : is_a_theorem(implies(T_517,implies(S_518,S_518))),
inference(splitRight,[status(thm)],[c_6841]) ).
tff(c_7282,plain,
! [S_518,T_517] :
( is_a_theorem(implies(S_518,S_518))
| ~ is_a_theorem(T_517) ),
inference(resolution,[status(thm)],[c_7167,c_2]) ).
tff(c_7283,plain,
! [T_517] : ~ is_a_theorem(T_517),
inference(splitLeft,[status(thm)],[c_7282]) ).
tff(c_6929,plain,
! [T_511,S_512] : is_a_theorem(implies(T_511,implies(S_512,S_512))),
inference(splitRight,[status(thm)],[c_6841]) ).
tff(c_7370,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_7283,c_6929]) ).
tff(c_7372,plain,
! [S_519] : is_a_theorem(implies(S_519,S_519)),
inference(splitRight,[status(thm)],[c_7282]) ).
tff(c_1185,plain,
! [T_215,T_214,R_217,T_213,R_216] : is_a_theorem(implies(T_215,implies(T_213,implies(implies(implies(R_217,T_214),T_214),implies(T_214,implies(R_216,T_214)))))),
inference(resolution,[status(thm)],[c_4,c_1047]) ).
tff(c_1223,plain,
! [T_215,T_214,R_217,T_213,R_216] :
( is_a_theorem(implies(T_213,implies(implies(implies(R_217,T_214),T_214),implies(T_214,implies(R_216,T_214)))))
| ~ is_a_theorem(T_215) ),
inference(resolution,[status(thm)],[c_1185,c_2]) ).
tff(c_1224,plain,
! [T_215] : ~ is_a_theorem(T_215),
inference(splitLeft,[status(thm)],[c_1223]) ).
tff(c_1263,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1224,c_1149]) ).
tff(c_1265,plain,
! [T_218,R_219,T_220,R_221] : is_a_theorem(implies(T_218,implies(implies(implies(R_219,T_220),T_220),implies(T_220,implies(R_221,T_220))))),
inference(splitRight,[status(thm)],[c_1223]) ).
tff(c_1310,plain,
! [R_219,T_220,R_221,T_218] :
( is_a_theorem(implies(implies(implies(R_219,T_220),T_220),implies(T_220,implies(R_221,T_220))))
| ~ is_a_theorem(T_218) ),
inference(resolution,[status(thm)],[c_1265,c_2]) ).
tff(c_1311,plain,
! [T_218] : ~ is_a_theorem(T_218),
inference(splitLeft,[status(thm)],[c_1310]) ).
tff(c_1264,plain,
! [T_213,R_217,T_214,R_216] : is_a_theorem(implies(T_213,implies(implies(implies(R_217,T_214),T_214),implies(T_214,implies(R_216,T_214))))),
inference(splitRight,[status(thm)],[c_1223]) ).
tff(c_1350,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1311,c_1264]) ).
tff(c_1352,plain,
! [R_222,T_223,R_224] : is_a_theorem(implies(implies(implies(R_222,T_223),T_223),implies(T_223,implies(R_224,T_223)))),
inference(splitRight,[status(thm)],[c_1310]) ).
tff(c_1473,plain,
! [R_237,T_238,R_239,T_240] : is_a_theorem(implies(implies(implies(R_237,T_238),implies(R_239,T_238)),implies(T_240,implies(T_238,implies(R_239,T_238))))),
inference(resolution,[status(thm)],[c_1352,c_12]) ).
tff(c_1502,plain,
! [T_240,T_238,R_239,R_237] :
( is_a_theorem(implies(T_240,implies(T_238,implies(R_239,T_238))))
| ~ is_a_theorem(implies(implies(R_237,T_238),implies(R_239,T_238))) ),
inference(resolution,[status(thm)],[c_1473,c_2]) ).
tff(c_7454,plain,
! [T_520,T_521,R_522] : is_a_theorem(implies(T_520,implies(T_521,implies(R_522,T_521)))),
inference(resolution,[status(thm)],[c_7372,c_1502]) ).
tff(c_7547,plain,
! [T_521,R_522,T_520] :
( is_a_theorem(implies(T_521,implies(R_522,T_521)))
| ~ is_a_theorem(T_520) ),
inference(resolution,[status(thm)],[c_7454,c_2]) ).
tff(c_7677,plain,
! [T_520] : ~ is_a_theorem(T_520),
inference(splitLeft,[status(thm)],[c_7547]) ).
tff(c_144,plain,
! [T_63,T_64,R_65,S_62] :
( is_a_theorem(implies(T_63,implies(T_64,implies(R_65,T_63))))
| ~ is_a_theorem(implies(S_62,T_63)) ),
inference(resolution,[status(thm)],[c_134,c_2]) ).
tff(c_7447,plain,
! [S_519,T_64,R_65] : is_a_theorem(implies(S_519,implies(T_64,implies(R_65,S_519)))),
inference(resolution,[status(thm)],[c_7372,c_144]) ).
tff(c_7764,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_7677,c_7447]) ).
tff(c_7765,plain,
! [T_521,R_522] : is_a_theorem(implies(T_521,implies(R_522,T_521))),
inference(splitRight,[status(thm)],[c_7547]) ).
tff(c_6,plain,
~ is_a_theorem(implies(a,implies(b,a))),
inference(cnfTransformation,[status(thm)],[f_36]) ).
tff(c_7770,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_7765,c_6]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL091-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.36 % Computer : n019.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 5 22:45:08 UTC 2026
% 0.09/0.37 % CPUTime :
% 12.08/4.57 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.46/4.60
% 12.46/4.60 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------