%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : REL023+2 : 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 : n019.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:10 PM UTC 2025
% Result : Theorem 10.08s 3.45s
% Output : CNFRefutation 10.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 14
% Syntax : Number of formulae : 68 ( 68 unt; 0 typ; 0 def)
% Number of atoms : 68 ( 67 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 5 ( 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 : 11 ( 11 usr; 6 con; 0-2 aty)
% Number of variables : 102 ( 102 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ meet > join > composition > #nlpp > converse > complement > zero > top > one > #skF_2 > #skF_3 > #skF_1
%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('#skF_2',type,
'#skF_2': $i ).
tff('#skF_3',type,
'#skF_3': $i ).
tff('#skF_1',type,
'#skF_1': $i ).
tff(one,type,
one: $i ).
tff(meet,type,
meet: ( $i * $i ) > $i ).
tff(zero,type,
zero: $i ).
tff(f_53,axiom,
! [X0,X1] : ( join(X0,X1) = join(X1,X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',maddux1_join_commutativity) ).
tff(f_59,axiom,
! [X0,X1] : ( meet(X0,X1) = complement(join(complement(X0),complement(X1))) ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',maddux4_definiton_of_meet) ).
tff(f_57,axiom,
! [X0,X1] : ( X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',maddux3_a_kind_of_de_Morgan) ).
tff(f_80,axiom,
! [X0] : ( zero = meet(X0,complement(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',def_zero) ).
tff(f_78,axiom,
! [X0] : ( top = join(X0,complement(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',def_top) ).
tff(f_69,axiom,
! [X0] : ( converse(converse(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',converse_idempotence) ).
tff(f_71,axiom,
! [X0,X1] : ( converse(join(X0,X1)) = join(converse(X0),converse(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',converse_additivity) ).
tff(f_64,axiom,
! [X0] : ( composition(X0,one) = X0 ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',composition_identity) ).
tff(f_73,axiom,
! [X0,X1] : ( converse(composition(X0,X1)) = composition(converse(X1),converse(X0)) ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',converse_multiplicativity) ).
tff(f_62,axiom,
! [X0,X1,X2] : ( composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',composition_associativity) ).
tff(f_75,axiom,
! [X0,X1] : ( join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',converse_cancellativity) ).
tff(f_55,axiom,
! [X0,X1,X2] : ( join(X0,join(X1,X2)) = join(join(X0,X1),X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',maddux2_join_associativity) ).
tff(f_66,axiom,
! [X0,X1,X2] : ( composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/REL001+0.ax',composition_distributivity) ).
tff(f_118,negated_conjecture,
~ ! [X0,X1,X2] : ( join(composition(meet(X0,converse(X1)),meet(X1,X2)),composition(X0,meet(X1,X2))) = composition(X0,meet(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
tff(c_2,plain,
! [X1_2,X0_1] : ( join(X1_2,X0_1) = join(X0_1,X1_2) ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_8,plain,
! [X0_8,X1_9] : ( complement(join(complement(X0_8),complement(X1_9))) = meet(X0_8,X1_9) ),
inference(cnfTransformation,[status(thm)],[f_59]) ).
tff(c_6,plain,
! [X0_6,X1_7] : ( join(complement(join(complement(X0_6),complement(X1_7))),complement(join(complement(X0_6),X1_7))) = X0_6 ),
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_635,plain,
! [X0_61,X1_62] : ( join(meet(X0_61,X1_62),complement(join(complement(X0_61),X1_62))) = X0_61 ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_6]) ).
tff(c_678,plain,
! [X0_61,X1_2] : ( join(meet(X0_61,X1_2),complement(join(X1_2,complement(X0_61)))) = X0_61 ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_635]) ).
tff(c_26,plain,
! [X0_25] : ( meet(X0_25,complement(X0_25)) = zero ),
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_24,plain,
! [X0_24] : ( join(X0_24,complement(X0_24)) = top ),
inference(cnfTransformation,[status(thm)],[f_78]) ).
tff(c_138,plain,
! [X0_43,X1_44] : ( complement(join(complement(X0_43),complement(X1_44))) = meet(X0_43,X1_44) ),
inference(cnfTransformation,[status(thm)],[f_59]) ).
tff(c_172,plain,
! [X0_43] : ( meet(X0_43,complement(X0_43)) = complement(top) ),
inference(superposition,[status(thm),theory(equality)],[c_24,c_138]) ).
tff(c_175,plain,
complement(top) = zero,
inference(demodulation,[status(thm),theory(equality)],[c_26,c_172]) ).
tff(c_686,plain,
! [X0_61] : ( join(meet(X0_61,complement(complement(X0_61))),complement(top)) = X0_61 ),
inference(superposition,[status(thm),theory(equality)],[c_24,c_635]) ).
tff(c_697,plain,
! [X0_61] : ( join(zero,meet(X0_61,complement(complement(X0_61)))) = X0_61 ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_175,c_686]) ).
tff(c_2689,plain,
! [X1_98,X0_99] : ( complement(join(complement(X1_98),complement(X0_99))) = meet(X0_99,X1_98) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_138]) ).
tff(c_2734,plain,
! [X1_98,X0_99] : ( meet(X1_98,X0_99) = meet(X0_99,X1_98) ),
inference(superposition,[status(thm),theory(equality)],[c_2689,c_8]) ).
tff(c_16,plain,
! [X0_17] : ( converse(converse(X0_17)) = X0_17 ),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_111,plain,
! [X0_41,X1_42] : ( join(converse(X0_41),converse(X1_42)) = converse(join(X0_41,X1_42)) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_479,plain,
! [X1_57,X0_58] : ( join(converse(X1_57),converse(X0_58)) = converse(join(X0_58,X1_57)) ),
inference(superposition,[status(thm),theory(equality)],[c_2,c_111]) ).
tff(c_18,plain,
! [X0_18,X1_19] : ( join(converse(X0_18),converse(X1_19)) = converse(join(X0_18,X1_19)) ),
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_522,plain,
! [X1_59,X0_60] : ( converse(join(X1_59,X0_60)) = converse(join(X0_60,X1_59)) ),
inference(superposition,[status(thm),theory(equality)],[c_479,c_18]) ).
tff(c_823,plain,
! [X0_68,X1_69] : ( converse(converse(join(X0_68,X1_69))) = join(X1_69,X0_68) ),
inference(superposition,[status(thm),theory(equality)],[c_522,c_16]) ).
tff(c_898,plain,
! [X0_24] : ( join(complement(X0_24),X0_24) = converse(converse(top)) ),
inference(superposition,[status(thm),theory(equality)],[c_24,c_823]) ).
tff(c_919,plain,
! [X0_70] : ( join(complement(X0_70),X0_70) = top ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_898]) ).
tff(c_940,plain,
! [X1_9] : ( meet(complement(X1_9),X1_9) = complement(top) ),
inference(superposition,[status(thm),theory(equality)],[c_919,c_8]) ).
tff(c_977,plain,
! [X1_9] : ( meet(complement(X1_9),X1_9) = zero ),
inference(demodulation,[status(thm),theory(equality)],[c_175,c_940]) ).
tff(c_2994,plain,
! [X0_103,X1_104] : ( join(meet(X0_103,complement(X1_104)),meet(X0_103,X1_104)) = X0_103 ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_635]) ).
tff(c_3042,plain,
! [X1_104] : ( join(zero,meet(complement(complement(X1_104)),X1_104)) = complement(complement(X1_104)) ),
inference(superposition,[status(thm),theory(equality)],[c_977,c_2994]) ).
tff(c_3080,plain,
! [X1_104] : ( complement(complement(X1_104)) = X1_104 ),
inference(demodulation,[status(thm),theory(equality)],[c_697,c_2734,c_3042]) ).
tff(c_12,plain,
! [X0_13] : ( composition(X0_13,one) = X0_13 ),
inference(cnfTransformation,[status(thm)],[f_64]) ).
tff(c_316,plain,
! [X1_47,X0_48] : ( composition(converse(X1_47),converse(X0_48)) = converse(composition(X0_48,X1_47)) ),
inference(cnfTransformation,[status(thm)],[f_73]) ).
tff(c_3662,plain,
! [X0_109,X1_110] : ( converse(composition(converse(X0_109),X1_110)) = composition(converse(X1_110),X0_109) ),
inference(superposition,[status(thm),theory(equality)],[c_16,c_316]) ).
tff(c_3759,plain,
! [X0_109] : ( composition(converse(one),X0_109) = converse(converse(X0_109)) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_3662]) ).
tff(c_3777,plain,
! [X0_109] : ( composition(converse(one),X0_109) = X0_109 ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_3759]) ).
tff(c_3779,plain,
! [X0_111] : ( composition(converse(one),X0_111) = X0_111 ),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_3759]) ).
tff(c_360,plain,
! [X0_50,X1_51,X2_52] : ( composition(composition(X0_50,X1_51),X2_52) = composition(X0_50,composition(X1_51,X2_52)) ),
inference(cnfTransformation,[status(thm)],[f_62]) ).
tff(c_382,plain,
! [X0_13,X2_52] : ( composition(X0_13,composition(one,X2_52)) = composition(X0_13,X2_52) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_360]) ).
tff(c_3816,plain,
! [X2_52] : ( composition(converse(one),X2_52) = composition(one,X2_52) ),
inference(superposition,[status(thm),theory(equality)],[c_3779,c_382]) ).
tff(c_3850,plain,
! [X2_52] : ( composition(one,X2_52) = X2_52 ),
inference(demodulation,[status(thm),theory(equality)],[c_3777,c_3816]) ).
tff(c_3827,plain,
converse(one) = one,
inference(superposition,[status(thm),theory(equality)],[c_3779,c_12]) ).
tff(c_3922,plain,
! [X2_112] : ( composition(one,X2_112) = X2_112 ),
inference(demodulation,[status(thm),theory(equality)],[c_3777,c_3816]) ).
tff(c_22,plain,
! [X0_22,X1_23] : ( join(composition(converse(X0_22),complement(composition(X0_22,X1_23))),complement(X1_23)) = complement(X1_23) ),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_3935,plain,
! [X2_112] : ( join(composition(converse(one),complement(X2_112)),complement(X2_112)) = complement(X2_112) ),
inference(superposition,[status(thm),theory(equality)],[c_3922,c_22]) ).
tff(c_4349,plain,
! [X2_116] : ( join(complement(X2_116),complement(X2_116)) = complement(X2_116) ),
inference(demodulation,[status(thm),theory(equality)],[c_3850,c_2,c_3827,c_3935]) ).
tff(c_4382,plain,
! [X1_104] : ( join(X1_104,complement(complement(X1_104))) = complement(complement(X1_104)) ),
inference(superposition,[status(thm),theory(equality)],[c_3080,c_4349]) ).
tff(c_4813,plain,
! [X1_122] : ( join(X1_122,X1_122) = X1_122 ),
inference(demodulation,[status(thm),theory(equality)],[c_3080,c_3080,c_4382]) ).
tff(c_4,plain,
! [X0_3,X1_4,X2_5] : ( join(join(X0_3,X1_4),X2_5) = join(X0_3,join(X1_4,X2_5)) ),
inference(cnfTransformation,[status(thm)],[f_55]) ).
tff(c_14523,plain,
! [X1_214,X2_215] : ( join(X1_214,join(X1_214,X2_215)) = join(X1_214,X2_215) ),
inference(superposition,[status(thm),theory(equality)],[c_4813,c_4]) ).
tff(c_14741,plain,
! [X0_61,X1_2] : ( join(meet(X0_61,X1_2),complement(join(X1_2,complement(X0_61)))) = join(meet(X0_61,X1_2),X0_61) ),
inference(superposition,[status(thm),theory(equality)],[c_678,c_14523]) ).
tff(c_14908,plain,
! [X0_61,X1_2] : ( join(X0_61,meet(X0_61,X1_2)) = X0_61 ),
inference(demodulation,[status(thm),theory(equality)],[c_678,c_2,c_14741]) ).
tff(c_14,plain,
! [X0_14,X2_16,X1_15] : ( join(composition(X0_14,X2_16),composition(X1_15,X2_16)) = composition(join(X0_14,X1_15),X2_16) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_34,plain,
join(composition(meet('#skF_1',converse('#skF_2')),meet('#skF_2','#skF_3')),composition('#skF_1',meet('#skF_2','#skF_3'))) != composition('#skF_1',meet('#skF_2','#skF_3')),
inference(cnfTransformation,[status(thm)],[f_118]) ).
tff(c_35,plain,
composition(join(meet('#skF_1',converse('#skF_2')),'#skF_1'),meet('#skF_2','#skF_3')) != composition('#skF_1',meet('#skF_2','#skF_3')),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_34]) ).
tff(c_37,plain,
composition(join('#skF_1',meet('#skF_1',converse('#skF_2'))),meet('#skF_2','#skF_3')) != composition('#skF_1',meet('#skF_2','#skF_3')),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_35]) ).
tff(c_2805,plain,
composition(join('#skF_1',meet('#skF_1',converse('#skF_2'))),meet('#skF_3','#skF_2')) != composition('#skF_1',meet('#skF_3','#skF_2')),
inference(demodulation,[status(thm),theory(equality)],[c_2734,c_2734,c_37]) ).
tff(c_14939,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_14908,c_2805]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : REL023+2 : TPTP v9.0.0. Released v4.0.0.
% 0.03/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.34 % Computer : n019.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Tue Apr 8 17:56:47 EDT 2025
% 0.13/0.34 % CPUTime :
% 10.08/3.45 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.08/3.46
% 10.08/3.46 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------