%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : REL015-1 : TPTP v9.0.0. Released v4.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 : n013.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 08:29:07 PM UTC 2025
% Result : Unsatisfiable 13.39s 4.60s
% Output : CNFRefutation 13.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 13
% Syntax : Number of formulae : 123 ( 123 unt; 0 typ; 0 def)
% Number of atoms : 123 ( 122 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-2 aty)
% Number of variables : 133 ( 133 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ meet > join > composition > #nlpp > converse > complement > zero > top > one
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(top,type,
top: $i ).
tff(converse,type,
converse: $i > $i ).
tff(join,type,
join: ( $i * $i ) > $i ).
tff(composition,type,
composition: ( $i * $i ) > $i ).
tff(complement,type,
complement: $i > $i ).
tff(one,type,
one: $i ).
tff(meet,type,
meet: ( $i * $i ) > $i ).
tff(zero,type,
zero: $i ).
tff(f_75,axiom,
composition(top,top) != top,
file(unknown,unknown) ).
tff(f_69,axiom,
! [A] : ( top = join(A,complement(A)) ),
file(unknown,unknown) ).
tff(f_61,axiom,
! [A] : ( converse(converse(A)) = A ),
file(unknown,unknown) ).
tff(f_63,axiom,
! [A,B] : ( converse(join(A,B)) = join(converse(A),converse(B)) ),
file(unknown,unknown) ).
tff(f_47,axiom,
! [A,B] : ( join(A,B) = join(B,A) ),
file(unknown,unknown) ).
tff(f_71,axiom,
! [A] : ( zero = meet(A,complement(A)) ),
file(unknown,unknown) ).
tff(f_53,axiom,
! [A,B] : ( meet(A,B) = complement(join(complement(A),complement(B))) ),
file(unknown,unknown) ).
tff(f_51,axiom,
! [A,B] : ( A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))) ),
file(unknown,unknown) ).
tff(f_49,axiom,
! [A,B,C] : ( join(A,join(B,C)) = join(join(A,B),C) ),
file(unknown,unknown) ).
tff(f_65,axiom,
! [A,B] : ( converse(composition(A,B)) = composition(converse(B),converse(A)) ),
file(unknown,unknown) ).
tff(f_67,axiom,
! [A,B] : ( join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B) ),
file(unknown,unknown) ).
tff(f_59,axiom,
! [A,B,C] : ( composition(join(A,B),C) = join(composition(A,C),composition(B,C)) ),
file(unknown,unknown) ).
tff(f_57,axiom,
! [A] : ( composition(A,one) = A ),
file(unknown,unknown) ).
tff(c_28,plain,
composition(top,top) != top,
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_24,plain,
! [A_24] : ( join(A_24,complement(A_24)) = top ),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_16,plain,
! [A_17] : ( converse(converse(A_17)) = A_17 ),
inference(cnfTransformation,[status(thm)],[f_61]) ).
tff(c_118,plain,
! [A_34,B_35] : ( join(converse(A_34),converse(B_35)) = converse(join(A_34,B_35)) ),
inference(cnfTransformation,[status(thm)],[f_63]) ).
tff(c_4519,plain,
! [A_117,B_118] : ( converse(join(converse(A_117),B_118)) = join(A_117,converse(B_118)) ),
inference(superposition,[status(thm),theory(equality)],[c_16,c_118]) ).
tff(c_5294,plain,
! [A_125] : ( join(A_125,converse(complement(converse(A_125)))) = converse(top) ),
inference(superposition,[status(thm),theory(equality)],[c_24,c_4519]) ).
tff(c_2,plain,
! [B_2,A_1] : ( join(B_2,A_1) = join(A_1,B_2) ),
inference(cnfTransformation,[status(thm)],[f_47]) ).
tff(c_26,plain,
! [A_25] : ( meet(A_25,complement(A_25)) = zero ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_145,plain,
! [A_36,B_37] : ( complement(join(complement(A_36),complement(B_37))) = meet(A_36,B_37) ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_179,plain,
! [A_36] : ( meet(A_36,complement(A_36)) = complement(top) ),
inference(superposition,[status(thm),theory(equality)],[c_24,c_145]) ).
tff(c_182,plain,
complement(top) = zero,
inference(demodulation,[status(thm),theory(equality)],[c_26,c_179]) ).
tff(c_8,plain,
! [A_8,B_9] : ( complement(join(complement(A_8),complement(B_9))) = meet(A_8,B_9) ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_6,plain,
! [A_6,B_7] : ( join(complement(join(complement(A_6),complement(B_7))),complement(join(complement(A_6),B_7))) = A_6 ),
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_560,plain,
! [A_53,B_54] : ( join(meet(A_53,B_54),complement(join(complement(A_53),B_54))) = A_53 ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_6]) ).
tff(c_614,plain,
! [A_53] : ( join(meet(A_53,complement(complement(A_53))),complement(top)) = A_53 ),
inference(superposition,[status(thm),theory(equality)],[c_24,c_560]) ).
tff(c_625,plain,
! [A_53] : ( join(zero,meet(A_53,complement(complement(A_53)))) = A_53 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_182,c_614]) ).
tff(c_225,plain,
join(top,zero) = top,
inference(superposition,[status(thm),theory(equality)],[c_182,c_24]) ).
tff(c_317,plain,
! [A_44,B_45,C_46] : ( join(join(A_44,B_45),C_46) = join(A_44,join(B_45,C_46)) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_525,plain,
! [C_52] : ( join(top,join(zero,C_52)) = join(top,C_52) ),
inference(superposition,[status(thm),theory(equality)],[c_225,c_317]) ).
tff(c_546,plain,
join(top,complement(zero)) = join(top,top),
inference(superposition,[status(thm),theory(equality)],[c_24,c_525]) ).
tff(c_222,plain,
! [A_8] : ( complement(join(complement(A_8),zero)) = meet(A_8,top) ),
inference(superposition,[status(thm),theory(equality)],[c_182,c_8]) ).
tff(c_390,plain,
! [A_47] : ( complement(join(zero,complement(A_47))) = meet(A_47,top) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_222]) ).
tff(c_439,plain,
meet(zero,top) = complement(top),
inference(superposition,[status(thm),theory(equality)],[c_24,c_390]) ).
tff(c_443,plain,
meet(zero,top) = zero,
inference(demodulation,[status(thm),theory(equality)],[c_182,c_439]) ).
tff(c_581,plain,
join(zero,complement(join(complement(zero),top))) = zero,
inference(superposition,[status(thm),theory(equality)],[c_443,c_560]) ).
tff(c_623,plain,
join(zero,complement(join(top,top))) = zero,
inference(demodulation,[status(thm),theory(equality)],[c_546,c_2,c_581]) ).
tff(c_342,plain,
! [C_46] : ( join(top,join(zero,C_46)) = join(top,C_46) ),
inference(superposition,[status(thm),theory(equality)],[c_225,c_317]) ).
tff(c_646,plain,
join(top,complement(join(top,top))) = join(top,zero),
inference(superposition,[status(thm),theory(equality)],[c_623,c_342]) ).
tff(c_658,plain,
join(top,complement(join(top,top))) = top,
inference(demodulation,[status(thm),theory(equality)],[c_225,c_646]) ).
tff(c_231,plain,
! [A_8] : ( complement(join(zero,complement(A_8))) = meet(A_8,top) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_222]) ).
tff(c_649,plain,
meet(join(top,top),top) = complement(zero),
inference(superposition,[status(thm),theory(equality)],[c_623,c_231]) ).
tff(c_29,plain,
! [A_6,B_7] : ( join(meet(A_6,B_7),complement(join(complement(A_6),B_7))) = A_6 ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_6]) ).
tff(c_738,plain,
join(complement(zero),complement(join(complement(join(top,top)),top))) = join(top,top),
inference(superposition,[status(thm),theory(equality)],[c_649,c_29]) ).
tff(c_747,plain,
join(top,top) = top,
inference(demodulation,[status(thm),theory(equality)],[c_24,c_182,c_2,c_658,c_2,c_738]) ).
tff(c_754,plain,
join(zero,complement(top)) = zero,
inference(demodulation,[status(thm),theory(equality)],[c_747,c_623]) ).
tff(c_757,plain,
join(zero,zero) = zero,
inference(demodulation,[status(thm),theory(equality)],[c_182,c_754]) ).
tff(c_4,plain,
! [A_3,B_4,C_5] : ( join(join(A_3,B_4),C_5) = join(A_3,join(B_4,C_5)) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_1188,plain,
! [C_67] : ( join(zero,join(zero,C_67)) = join(zero,C_67) ),
inference(superposition,[status(thm),theory(equality)],[c_757,c_4]) ).
tff(c_1212,plain,
! [A_53] : ( join(zero,meet(A_53,complement(complement(A_53)))) = join(zero,A_53) ),
inference(superposition,[status(thm),theory(equality)],[c_625,c_1188]) ).
tff(c_1247,plain,
! [A_68] : ( join(zero,A_68) = A_68 ),
inference(demodulation,[status(thm),theory(equality)],[c_625,c_1212]) ).
tff(c_1276,plain,
complement(zero) = top,
inference(superposition,[status(thm),theory(equality)],[c_1247,c_24]) ).
tff(c_1238,plain,
! [A_53] : ( join(zero,A_53) = A_53 ),
inference(demodulation,[status(thm),theory(equality)],[c_625,c_1212]) ).
tff(c_1332,plain,
! [B_9] : ( complement(join(top,complement(B_9))) = meet(zero,B_9) ),
inference(superposition,[status(thm),theory(equality)],[c_1276,c_8]) ).
tff(c_761,plain,
! [C_5] : ( join(top,join(top,C_5)) = join(top,C_5) ),
inference(superposition,[status(thm),theory(equality)],[c_747,c_4]) ).
tff(c_891,plain,
! [B_60,A_61] : ( complement(join(complement(B_60),complement(A_61))) = meet(A_61,B_60) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_145]) ).
tff(c_927,plain,
! [B_60,A_61] : ( meet(B_60,A_61) = meet(A_61,B_60) ),
inference(superposition,[status(thm),theory(equality)],[c_891,c_8]) ).
tff(c_362,plain,
! [A_24,C_46] : ( join(A_24,join(complement(A_24),C_46)) = join(top,C_46) ),
inference(superposition,[status(thm),theory(equality)],[c_24,c_317]) ).
tff(c_219,plain,
! [B_9] : ( complement(join(zero,complement(B_9))) = meet(top,B_9) ),
inference(superposition,[status(thm),theory(equality)],[c_182,c_8]) ).
tff(c_1246,plain,
! [B_9] : ( complement(complement(B_9)) = meet(top,B_9) ),
inference(demodulation,[status(thm),theory(equality)],[c_1238,c_219]) ).
tff(c_1260,plain,
! [A_53] : ( meet(A_53,complement(complement(A_53))) = A_53 ),
inference(superposition,[status(thm),theory(equality)],[c_1247,c_625]) ).
tff(c_1883,plain,
! [A_53] : ( meet(A_53,meet(top,A_53)) = A_53 ),
inference(demodulation,[status(thm),theory(equality)],[c_1246,c_1260]) ).
tff(c_1688,plain,
! [B_75] : ( complement(complement(B_75)) = meet(top,B_75) ),
inference(demodulation,[status(thm),theory(equality)],[c_1238,c_219]) ).
tff(c_979,plain,
! [B_60] : ( meet(complement(B_60),B_60) = complement(top) ),
inference(superposition,[status(thm),theory(equality)],[c_24,c_891]) ).
tff(c_987,plain,
! [B_60] : ( meet(complement(B_60),B_60) = zero ),
inference(demodulation,[status(thm),theory(equality)],[c_182,c_979]) ).
tff(c_2127,plain,
! [B_82] : ( meet(meet(top,B_82),complement(B_82)) = zero ),
inference(superposition,[status(thm),theory(equality)],[c_1688,c_987]) ).
tff(c_2138,plain,
! [B_82] : ( join(zero,complement(join(complement(meet(top,B_82)),complement(B_82)))) = meet(top,B_82) ),
inference(superposition,[status(thm),theory(equality)],[c_2127,c_29]) ).
tff(c_2195,plain,
! [B_82] : ( meet(top,B_82) = B_82 ),
inference(demodulation,[status(thm),theory(equality)],[c_1883,c_1238,c_8,c_2,c_2138]) ).
tff(c_2210,plain,
! [B_9] : ( complement(complement(B_9)) = B_9 ),
inference(demodulation,[status(thm),theory(equality)],[c_2195,c_1246]) ).
tff(c_1245,plain,
! [A_8] : ( complement(complement(A_8)) = meet(A_8,top) ),
inference(demodulation,[status(thm),theory(equality)],[c_1238,c_231]) ).
tff(c_2282,plain,
! [A_8] : ( meet(A_8,top) = A_8 ),
inference(demodulation,[status(thm),theory(equality)],[c_2210,c_1245]) ).
tff(c_2713,plain,
! [A_91,B_92] : ( join(meet(A_91,complement(B_92)),meet(A_91,B_92)) = A_91 ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_560]) ).
tff(c_2760,plain,
! [A_91] : ( join(meet(A_91,top),meet(A_91,zero)) = A_91 ),
inference(superposition,[status(thm),theory(equality)],[c_1276,c_2713]) ).
tff(c_2817,plain,
! [A_93] : ( join(A_93,meet(A_93,zero)) = A_93 ),
inference(demodulation,[status(thm),theory(equality)],[c_2282,c_2760]) ).
tff(c_366,plain,
! [A_44,B_45] : ( join(A_44,join(B_45,complement(join(A_44,B_45)))) = top ),
inference(superposition,[status(thm),theory(equality)],[c_24,c_317]) ).
tff(c_2827,plain,
! [A_93] : ( join(A_93,join(meet(A_93,zero),complement(A_93))) = top ),
inference(superposition,[status(thm),theory(equality)],[c_2817,c_366]) ).
tff(c_2892,plain,
! [A_94] : ( join(top,meet(A_94,zero)) = top ),
inference(demodulation,[status(thm),theory(equality)],[c_362,c_2,c_2827]) ).
tff(c_2925,plain,
! [A_61] : ( join(top,meet(zero,A_61)) = top ),
inference(superposition,[status(thm),theory(equality)],[c_927,c_2892]) ).
tff(c_3721,plain,
! [B_106] : ( complement(join(top,complement(B_106))) = meet(zero,B_106) ),
inference(superposition,[status(thm),theory(equality)],[c_1276,c_8]) ).
tff(c_3724,plain,
! [B_106] : ( meet(zero,join(top,complement(B_106))) = complement(join(top,meet(zero,B_106))) ),
inference(superposition,[status(thm),theory(equality)],[c_3721,c_1332]) ).
tff(c_3803,plain,
! [B_107] : ( meet(zero,join(top,complement(B_107))) = zero ),
inference(demodulation,[status(thm),theory(equality)],[c_182,c_2925,c_3724]) ).
tff(c_3821,plain,
! [B_107] : ( join(zero,complement(join(complement(zero),join(top,complement(B_107))))) = zero ),
inference(superposition,[status(thm),theory(equality)],[c_3803,c_29]) ).
tff(c_3861,plain,
! [B_108] : ( meet(zero,B_108) = zero ),
inference(demodulation,[status(thm),theory(equality)],[c_1332,c_1238,c_761,c_1276,c_3821]) ).
tff(c_3901,plain,
! [B_108] : ( join(zero,complement(join(complement(zero),B_108))) = zero ),
inference(superposition,[status(thm),theory(equality)],[c_3861,c_29]) ).
tff(c_4022,plain,
! [B_110] : ( complement(join(top,B_110)) = zero ),
inference(demodulation,[status(thm),theory(equality)],[c_1238,c_1276,c_3901]) ).
tff(c_4033,plain,
! [B_110] : ( join(top,B_110) = complement(zero) ),
inference(superposition,[status(thm),theory(equality)],[c_4022,c_2210]) ).
tff(c_4098,plain,
! [B_110] : ( join(top,B_110) = top ),
inference(demodulation,[status(thm),theory(equality)],[c_1276,c_4033]) ).
tff(c_5312,plain,
converse(top) = top,
inference(superposition,[status(thm),theory(equality)],[c_5294,c_4098]) ).
tff(c_20,plain,
! [B_21,A_20] : ( composition(converse(B_21),converse(A_20)) = converse(composition(A_20,B_21)) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_24289,plain,
! [B_267] : ( composition(converse(B_267),top) = converse(composition(top,B_267)) ),
inference(superposition,[status(thm),theory(equality)],[c_5312,c_20]) ).
tff(c_24340,plain,
converse(composition(top,top)) = composition(top,top),
inference(superposition,[status(thm),theory(equality)],[c_5312,c_24289]) ).
tff(c_1296,plain,
! [A_1] : ( join(A_1,zero) = A_1 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_1247]) ).
tff(c_4607,plain,
! [A_117] : ( join(A_117,converse(zero)) = converse(converse(A_117)) ),
inference(superposition,[status(thm),theory(equality)],[c_1296,c_4519]) ).
tff(c_4643,plain,
! [A_119] : ( join(A_119,converse(zero)) = A_119 ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_4607]) ).
tff(c_4678,plain,
converse(zero) = zero,
inference(superposition,[status(thm),theory(equality)],[c_4643,c_1238]) ).
tff(c_660,plain,
! [A_56,B_57] : ( join(composition(converse(A_56),complement(composition(A_56,B_57))),complement(B_57)) = complement(B_57) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_699,plain,
! [B_21,A_20] : ( join(composition(converse(converse(B_21)),complement(converse(composition(A_20,B_21)))),complement(converse(A_20))) = complement(converse(A_20)) ),
inference(superposition,[status(thm),theory(equality)],[c_20,c_660]) ).
tff(c_719,plain,
! [A_20,B_21] : ( join(complement(converse(A_20)),composition(B_21,complement(converse(composition(A_20,B_21))))) = complement(converse(A_20)) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_16,c_699]) ).
tff(c_24401,plain,
join(complement(converse(top)),composition(top,complement(composition(top,top)))) = complement(converse(top)),
inference(superposition,[status(thm),theory(equality)],[c_24340,c_719]) ).
tff(c_24496,plain,
composition(top,complement(composition(top,top))) = zero,
inference(demodulation,[status(thm),theory(equality)],[c_182,c_5312,c_1238,c_182,c_5312,c_24401]) ).
tff(c_4123,plain,
! [B_111] : ( join(top,B_111) = top ),
inference(demodulation,[status(thm),theory(equality)],[c_1276,c_4033]) ).
tff(c_4153,plain,
! [B_111] : ( join(B_111,top) = top ),
inference(superposition,[status(thm),theory(equality)],[c_4123,c_2]) ).
tff(c_448,plain,
! [A_48,C_49,B_50] : ( join(composition(A_48,C_49),composition(B_50,C_49)) = composition(join(A_48,B_50),C_49) ),
inference(cnfTransformation,[status(thm)],[f_59]) ).
tff(c_460,plain,
! [B_50,C_49,A_48] : ( join(composition(B_50,C_49),composition(A_48,C_49)) = composition(join(A_48,B_50),C_49) ),
inference(superposition,[status(thm),theory(equality)],[c_448,c_2]) ).
tff(c_24521,plain,
! [A_48] : ( join(zero,composition(A_48,complement(composition(top,top)))) = composition(join(A_48,top),complement(composition(top,top))) ),
inference(superposition,[status(thm),theory(equality)],[c_24496,c_460]) ).
tff(c_24583,plain,
! [A_268] : ( composition(A_268,complement(composition(top,top))) = zero ),
inference(demodulation,[status(thm),theory(equality)],[c_24496,c_4153,c_1238,c_24521]) ).
tff(c_12,plain,
! [A_13] : ( composition(A_13,one) = A_13 ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_103,plain,
! [B_32,A_33] : ( composition(converse(B_32),converse(A_33)) = converse(composition(A_33,B_32)) ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_4282,plain,
! [A_113,B_114] : ( converse(composition(converse(A_113),B_114)) = composition(converse(B_114),A_113) ),
inference(superposition,[status(thm),theory(equality)],[c_16,c_103]) ).
tff(c_4355,plain,
! [A_113] : ( composition(converse(one),A_113) = converse(converse(A_113)) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_4282]) ).
tff(c_4371,plain,
! [A_115] : ( composition(converse(one),A_115) = A_115 ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_4355]) ).
tff(c_4409,plain,
converse(one) = one,
inference(superposition,[status(thm),theory(equality)],[c_4371,c_12]) ).
tff(c_4369,plain,
! [A_113] : ( composition(converse(one),A_113) = A_113 ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_4355]) ).
tff(c_4435,plain,
! [A_113] : ( composition(one,A_113) = A_113 ),
inference(demodulation,[status(thm),theory(equality)],[c_4409,c_4369]) ).
tff(c_24616,plain,
complement(composition(top,top)) = zero,
inference(superposition,[status(thm),theory(equality)],[c_24583,c_4435]) ).
tff(c_5392,plain,
! [A_17] : ( join(converse(A_17),converse(complement(A_17))) = converse(top) ),
inference(superposition,[status(thm),theory(equality)],[c_16,c_5294]) ).
tff(c_5580,plain,
! [A_128] : ( join(converse(A_128),converse(complement(A_128))) = top ),
inference(demodulation,[status(thm),theory(equality)],[c_5312,c_5392]) ).
tff(c_5648,plain,
! [B_9] : ( join(converse(complement(B_9)),converse(B_9)) = top ),
inference(superposition,[status(thm),theory(equality)],[c_2210,c_5580]) ).
tff(c_25616,plain,
join(converse(zero),converse(composition(top,top))) = top,
inference(superposition,[status(thm),theory(equality)],[c_24616,c_5648]) ).
tff(c_25714,plain,
composition(top,top) = top,
inference(demodulation,[status(thm),theory(equality)],[c_24340,c_1238,c_4678,c_25616]) ).
tff(c_25716,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_28,c_25714]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.01/0.06 % Problem : REL015-1 : TPTP v9.0.0. Released v4.0.0.
% 0.01/0.07 % 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.06/0.25 % Computer : n013.cluster.edu
% 0.06/0.25 % Model : x86_64 x86_64
% 0.06/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.25 % Memory : 8042.1875MB
% 0.06/0.25 % OS : Linux 3.10.0-693.el7.x86_64
% 0.06/0.25 % CPULimit : 300
% 0.06/0.25 % WCLimit : 300
% 0.06/0.25 % DateTime : Tue Apr 8 17:46:17 EDT 2025
% 0.06/0.26 % CPUTime :
% 13.39/4.60 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.39/4.62
% 13.39/4.62 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------