%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : COM007+1 : TPTP v9.0.0. Released v3.2.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 : n006.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 05:50:33 PM UTC 2025
% Result : Theorem 3.36s 1.90s
% Output : CNFRefutation 3.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 10
% Syntax : Number of formulae : 52 ( 20 unt; 0 typ; 0 def)
% Number of atoms : 101 ( 0 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 96 ( 47 ~; 37 |; 5 &)
% ( 0 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 4 usr; 2 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 3 con; 0-3 aty)
% Number of variables : 52 ( 51 !; 1 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ rewrite > reflexive_rewrite > equalish > #nlpp > goal > c > b > a > #skF_1
%Foreground sorts:
%Background operators:
%Foreground operators:
tff('#skF_1',type,
'#skF_1': ( $i * $i * $i ) > $i ).
tff(rewrite,type,
rewrite: ( $i * $i ) > $o ).
tff(a,type,
a: $i ).
tff(goal,type,
goal: $o ).
tff(b,type,
b: $i ).
tff(equalish,type,
equalish: ( $i * $i ) > $o ).
tff(reflexive_rewrite,type,
reflexive_rewrite: ( $i * $i ) > $o ).
tff(c,type,
c: $i ).
tff(f_35,axiom,
! [A] : equalish(A,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity) ).
tff(f_49,axiom,
! [A,B] :
( equalish(A,B)
=> reflexive_rewrite(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equalish_in_reflexive_rewrite) ).
tff(f_27,axiom,
( reflexive_rewrite(a,b)
& reflexive_rewrite(a,c) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',assumption) ).
tff(f_45,axiom,
! [A,B,C] :
( ( equalish(A,B)
& reflexive_rewrite(B,C) )
=> reflexive_rewrite(A,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',substitution) ).
tff(f_70,negated_conjecture,
~ goal,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal_to_be_proved) ).
tff(f_33,axiom,
! [A] :
( ( reflexive_rewrite(b,A)
& reflexive_rewrite(c,A) )
=> goal ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal_ax) ).
tff(f_59,axiom,
! [A,B] :
( reflexive_rewrite(A,B)
=> ( equalish(A,B)
| rewrite(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equalish_or_rewrite) ).
tff(f_68,axiom,
! [A,B,C] :
( ( rewrite(A,B)
& rewrite(A,C) )
=> ? [D] :
( rewrite(B,D)
& rewrite(C,D) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rewrite_diamond) ).
tff(f_53,axiom,
! [A,B] :
( rewrite(A,B)
=> reflexive_rewrite(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rewrite_in_reflexive_rewrite) ).
tff(f_39,axiom,
! [A,B] :
( equalish(A,B)
=> equalish(B,A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmtery) ).
tff(c_8,plain,
! [A_2] : equalish(A_2,A_2),
inference(cnfTransformation,[status(thm)],[f_35]) ).
tff(c_14,plain,
! [A_8,B_9] :
( reflexive_rewrite(A_8,B_9)
| ~ equalish(A_8,B_9) ),
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_2,plain,
reflexive_rewrite(a,c),
inference(cnfTransformation,[status(thm)],[f_27]) ).
tff(c_52,plain,
! [A_28,C_29,B_30] :
( reflexive_rewrite(A_28,C_29)
| ~ reflexive_rewrite(B_30,C_29)
| ~ equalish(A_28,B_30) ),
inference(cnfTransformation,[status(thm)],[f_45]) ).
tff(c_62,plain,
! [A_31] :
( reflexive_rewrite(A_31,c)
| ~ equalish(A_31,a) ),
inference(resolution,[status(thm)],[c_2,c_52]) ).
tff(c_24,plain,
~ goal,
inference(cnfTransformation,[status(thm)],[f_70]) ).
tff(c_6,plain,
! [A_1] :
( goal
| ~ reflexive_rewrite(c,A_1)
| ~ reflexive_rewrite(b,A_1) ),
inference(cnfTransformation,[status(thm)],[f_33]) ).
tff(c_25,plain,
! [A_1] :
( ~ reflexive_rewrite(c,A_1)
| ~ reflexive_rewrite(b,A_1) ),
inference(negUnitSimplification,[status(thm)],[c_24,c_6]) ).
tff(c_77,plain,
( ~ reflexive_rewrite(b,c)
| ~ equalish(c,a) ),
inference(resolution,[status(thm)],[c_62,c_25]) ).
tff(c_97,plain,
~ equalish(c,a),
inference(splitLeft,[status(thm)],[c_77]) ).
tff(c_34,plain,
! [A_25] :
( ~ reflexive_rewrite(c,A_25)
| ~ reflexive_rewrite(b,A_25) ),
inference(negUnitSimplification,[status(thm)],[c_24,c_6]) ).
tff(c_39,plain,
! [B_9] :
( ~ reflexive_rewrite(b,B_9)
| ~ equalish(c,B_9) ),
inference(resolution,[status(thm)],[c_14,c_34]) ).
tff(c_68,plain,
( ~ equalish(c,c)
| ~ equalish(b,a) ),
inference(resolution,[status(thm)],[c_62,c_39]) ).
tff(c_76,plain,
~ equalish(b,a),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_68]) ).
tff(c_4,plain,
reflexive_rewrite(a,b),
inference(cnfTransformation,[status(thm)],[f_27]) ).
tff(c_18,plain,
! [A_12,B_13] :
( rewrite(A_12,B_13)
| equalish(A_12,B_13)
| ~ reflexive_rewrite(A_12,B_13) ),
inference(cnfTransformation,[status(thm)],[f_59]) ).
tff(c_98,plain,
! [B_35,A_36,C_37] :
( rewrite(B_35,'#skF_1'(A_36,B_35,C_37))
| ~ rewrite(A_36,C_37)
| ~ rewrite(A_36,B_35) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_16,plain,
! [A_10,B_11] :
( reflexive_rewrite(A_10,B_11)
| ~ rewrite(A_10,B_11) ),
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_102,plain,
! [B_35,A_36,C_37] :
( reflexive_rewrite(B_35,'#skF_1'(A_36,B_35,C_37))
| ~ rewrite(A_36,C_37)
| ~ rewrite(A_36,B_35) ),
inference(resolution,[status(thm)],[c_98,c_16]) ).
tff(c_115,plain,
! [C_45,A_46,B_47] :
( rewrite(C_45,'#skF_1'(A_46,B_47,C_45))
| ~ rewrite(A_46,C_45)
| ~ rewrite(A_46,B_47) ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_134,plain,
! [C_51,A_52,B_53] :
( reflexive_rewrite(C_51,'#skF_1'(A_52,B_53,C_51))
| ~ rewrite(A_52,C_51)
| ~ rewrite(A_52,B_53) ),
inference(resolution,[status(thm)],[c_115,c_16]) ).
tff(c_149,plain,
! [A_56,B_57] :
( ~ reflexive_rewrite(b,'#skF_1'(A_56,B_57,c))
| ~ rewrite(A_56,c)
| ~ rewrite(A_56,B_57) ),
inference(resolution,[status(thm)],[c_134,c_25]) ).
tff(c_159,plain,
! [A_58] :
( ~ rewrite(A_58,c)
| ~ rewrite(A_58,b) ),
inference(resolution,[status(thm)],[c_102,c_149]) ).
tff(c_175,plain,
! [A_61] :
( ~ rewrite(A_61,b)
| equalish(A_61,c)
| ~ reflexive_rewrite(A_61,c) ),
inference(resolution,[status(thm)],[c_18,c_159]) ).
tff(c_184,plain,
! [A_68] :
( equalish(A_68,c)
| ~ reflexive_rewrite(A_68,c)
| equalish(A_68,b)
| ~ reflexive_rewrite(A_68,b) ),
inference(resolution,[status(thm)],[c_18,c_175]) ).
tff(c_194,plain,
( equalish(a,c)
| equalish(a,b)
| ~ reflexive_rewrite(a,b) ),
inference(resolution,[status(thm)],[c_2,c_184]) ).
tff(c_199,plain,
( equalish(a,c)
| equalish(a,b) ),
inference(demodulation,[status(thm),theory(equality)],[c_4,c_194]) ).
tff(c_224,plain,
equalish(a,b),
inference(splitLeft,[status(thm)],[c_199]) ).
tff(c_10,plain,
! [B_4,A_3] :
( equalish(B_4,A_3)
| ~ equalish(A_3,B_4) ),
inference(cnfTransformation,[status(thm)],[f_39]) ).
tff(c_232,plain,
equalish(b,a),
inference(resolution,[status(thm)],[c_224,c_10]) ).
tff(c_241,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_76,c_232]) ).
tff(c_242,plain,
equalish(a,c),
inference(splitRight,[status(thm)],[c_199]) ).
tff(c_251,plain,
equalish(c,a),
inference(resolution,[status(thm)],[c_242,c_10]) ).
tff(c_260,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_97,c_251]) ).
tff(c_262,plain,
equalish(c,a),
inference(splitRight,[status(thm)],[c_77]) ).
tff(c_78,plain,
! [A_32] :
( reflexive_rewrite(A_32,b)
| ~ equalish(A_32,a) ),
inference(resolution,[status(thm)],[c_4,c_52]) ).
tff(c_91,plain,
( ~ reflexive_rewrite(b,b)
| ~ equalish(c,a) ),
inference(resolution,[status(thm)],[c_78,c_25]) ).
tff(c_263,plain,
~ equalish(c,a),
inference(splitLeft,[status(thm)],[c_91]) ).
tff(c_280,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_262,c_263]) ).
tff(c_281,plain,
~ reflexive_rewrite(b,b),
inference(splitRight,[status(thm)],[c_91]) ).
tff(c_296,plain,
~ equalish(b,b),
inference(resolution,[status(thm)],[c_14,c_281]) ).
tff(c_301,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_8,c_296]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : COM007+1 : TPTP v9.0.0. Released v3.2.0.
% 0.06/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 : n006.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 : Mon Apr 7 16:11:08 EDT 2025
% 0.13/0.34 % CPUTime :
% 3.36/1.90 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.36/1.90
% 3.36/1.90 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------