%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : REL001-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 : n002.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:01 PM UTC 2025
% Result : Unsatisfiable 4.06s 2.03s
% Output : CNFRefutation 4.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 7
% Syntax : Number of formulae : 46 ( 46 unt; 0 typ; 0 def)
% Number of atoms : 46 ( 45 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 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 : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 43 ( 43 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ meet > join > composition > #nlpp > converse > complement > zero > top > sk1 > one
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(top,type,
top: $i ).
tff(sk1,type,
sk1: $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_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_69,axiom,
! [A] : ( top = join(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_75,axiom,
join(zero,sk1) != sk1,
file(unknown,unknown) ).
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_24,plain,
! [A_24] : ( join(A_24,complement(A_24)) = top ),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_119,plain,
! [A_34,B_35] : ( complement(join(complement(A_34),complement(B_35))) = meet(A_34,B_35) ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_153,plain,
! [A_34] : ( meet(A_34,complement(A_34)) = complement(top) ),
inference(superposition,[status(thm),theory(equality)],[c_24,c_119]) ).
tff(c_156,plain,
complement(top) = zero,
inference(demodulation,[status(thm),theory(equality)],[c_26,c_153]) ).
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_522,plain,
! [A_50,B_51] : ( join(meet(A_50,B_51),complement(join(complement(A_50),B_51))) = A_50 ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_6]) ).
tff(c_579,plain,
! [A_50] : ( join(meet(A_50,complement(complement(A_50))),complement(top)) = A_50 ),
inference(superposition,[status(thm),theory(equality)],[c_24,c_522]) ).
tff(c_588,plain,
! [A_50] : ( join(zero,meet(A_50,complement(complement(A_50)))) = A_50 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_156,c_579]) ).
tff(c_169,plain,
join(top,zero) = top,
inference(superposition,[status(thm),theory(equality)],[c_156,c_24]) ).
tff(c_382,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_474,plain,
! [C_49] : ( join(top,join(zero,C_49)) = join(top,C_49) ),
inference(superposition,[status(thm),theory(equality)],[c_169,c_382]) ).
tff(c_495,plain,
join(top,complement(zero)) = join(top,top),
inference(superposition,[status(thm),theory(equality)],[c_24,c_474]) ).
tff(c_163,plain,
! [A_8] : ( complement(join(complement(A_8),zero)) = meet(A_8,top) ),
inference(superposition,[status(thm),theory(equality)],[c_156,c_8]) ).
tff(c_266,plain,
! [A_39] : ( complement(join(zero,complement(A_39))) = meet(A_39,top) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_163]) ).
tff(c_315,plain,
meet(zero,top) = complement(top),
inference(superposition,[status(thm),theory(equality)],[c_24,c_266]) ).
tff(c_319,plain,
meet(zero,top) = zero,
inference(demodulation,[status(thm),theory(equality)],[c_156,c_315]) ).
tff(c_543,plain,
join(zero,complement(join(complement(zero),top))) = zero,
inference(superposition,[status(thm),theory(equality)],[c_319,c_522]) ).
tff(c_585,plain,
join(zero,complement(join(top,top))) = zero,
inference(demodulation,[status(thm),theory(equality)],[c_495,c_2,c_543]) ).
tff(c_407,plain,
! [C_46] : ( join(top,join(zero,C_46)) = join(top,C_46) ),
inference(superposition,[status(thm),theory(equality)],[c_169,c_382]) ).
tff(c_608,plain,
join(top,complement(join(top,top))) = join(top,zero),
inference(superposition,[status(thm),theory(equality)],[c_585,c_407]) ).
tff(c_620,plain,
join(top,complement(join(top,top))) = top,
inference(demodulation,[status(thm),theory(equality)],[c_169,c_608]) ).
tff(c_172,plain,
! [A_8] : ( complement(join(zero,complement(A_8))) = meet(A_8,top) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_163]) ).
tff(c_614,plain,
meet(join(top,top),top) = complement(zero),
inference(superposition,[status(thm),theory(equality)],[c_585,c_172]) ).
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_692,plain,
join(complement(zero),complement(join(complement(join(top,top)),top))) = join(top,top),
inference(superposition,[status(thm),theory(equality)],[c_614,c_29]) ).
tff(c_701,plain,
join(top,top) = top,
inference(demodulation,[status(thm),theory(equality)],[c_24,c_156,c_2,c_620,c_2,c_692]) ).
tff(c_708,plain,
join(zero,complement(top)) = zero,
inference(demodulation,[status(thm),theory(equality)],[c_701,c_585]) ).
tff(c_711,plain,
join(zero,zero) = zero,
inference(demodulation,[status(thm),theory(equality)],[c_156,c_708]) ).
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_1428,plain,
! [C_69] : ( join(zero,join(zero,C_69)) = join(zero,C_69) ),
inference(superposition,[status(thm),theory(equality)],[c_711,c_4]) ).
tff(c_1496,plain,
! [A_50] : ( join(zero,meet(A_50,complement(complement(A_50)))) = join(zero,A_50) ),
inference(superposition,[status(thm),theory(equality)],[c_588,c_1428]) ).
tff(c_1547,plain,
! [A_70] : ( join(zero,A_70) = A_70 ),
inference(demodulation,[status(thm),theory(equality)],[c_588,c_1496]) ).
tff(c_1617,plain,
! [B_2] : ( join(B_2,zero) = B_2 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_1547]) ).
tff(c_28,plain,
join(zero,sk1) != sk1,
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_30,plain,
join(sk1,zero) != sk1,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_28]) ).
tff(c_1692,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1617,c_30]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : REL001-1 : TPTP v9.0.0. Released v4.0.0.
% 0.13/0.13 % 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.13/0.33 % Computer : n002.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Tue Apr 8 17:40:17 EDT 2025
% 0.13/0.33 % CPUTime :
% 4.06/2.03 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.06/2.04
% 4.06/2.04 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------