%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : HWC001-1 : TPTP v9.0.0. Bugfixed v1.1.1.
% 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 : n025.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 06:46:38 PM UTC 2025
% Result : Unsatisfiable 11.56s 4.21s
% Output : CNFRefutation 11.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 9
% Syntax : Number of formulae : 85 ( 35 unt; 0 typ; 0 def)
% Number of atoms : 145 ( 14 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 125 ( 65 ~; 60 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-4 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 136 ( 136 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ output > nand > and > #nlpp > not > n1 > n0
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(nand,type,
nand: ( $i * $i ) > $i ).
tff(n1,type,
n1: $i ).
tff(not,type,
not: $i > $i ).
tff(n0,type,
n0: $i ).
tff(and,type,
and: ( $i * $i ) > $i ).
tff(output,type,
output: ( $i * $i * $i * $i ) > $o ).
tff(f_44,axiom,
~ output(n0,n1,n1,n1),
file(unknown,unknown) ).
tff(f_31,axiom,
not(n0) = n1,
file(unknown,unknown) ).
tff(f_28,axiom,
! [X] : ( and(X,n0) = n0 ),
file(unknown,unknown) ).
tff(f_26,axiom,
! [X,Y] : ( nand(X,Y) = not(and(X,Y)) ),
file(unknown,unknown) ).
tff(f_32,axiom,
not(n1) = n0,
file(unknown,unknown) ).
tff(f_30,axiom,
! [X] : ( and(X,n1) = X ),
file(unknown,unknown) ).
tff(f_42,axiom,
output(n0,n1,n0,n1),
file(unknown,unknown) ).
tff(f_40,axiom,
! [X3,Y3,Y1,X1,Y2,X2,X4,Y4] :
( ~ output(X1,X2,X3,X4)
| ~ output(Y1,Y2,Y3,Y4)
| output(nand(X1,Y1),nand(X2,Y2),nand(X3,Y3),nand(X4,Y4)) ),
file(unknown,unknown) ).
tff(f_41,axiom,
output(n0,n0,n1,n1),
file(unknown,unknown) ).
tff(c_18,plain,
~ output(n0,n1,n1,n1),
inference(cnfTransformation,[status(thm)],[f_44]) ).
tff(c_8,plain,
not(n0) = n1,
inference(cnfTransformation,[status(thm)],[f_31]) ).
tff(c_4,plain,
! [X_3] : ( and(X_3,n0) = n0 ),
inference(cnfTransformation,[status(thm)],[f_28]) ).
tff(c_43,plain,
! [X_15,Y_16] : ( not(and(X_15,Y_16)) = nand(X_15,Y_16) ),
inference(cnfTransformation,[status(thm)],[f_26]) ).
tff(c_55,plain,
! [X_3] : ( nand(X_3,n0) = not(n0) ),
inference(superposition,[status(thm),theory(equality)],[c_4,c_43]) ).
tff(c_58,plain,
! [X_3] : ( nand(X_3,n0) = n1 ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_55]) ).
tff(c_10,plain,
not(n1) = n0,
inference(cnfTransformation,[status(thm)],[f_32]) ).
tff(c_6,plain,
! [X_4] : ( and(X_4,n1) = X_4 ),
inference(cnfTransformation,[status(thm)],[f_30]) ).
tff(c_52,plain,
! [X_4] : ( nand(X_4,n1) = not(X_4) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_43]) ).
tff(c_16,plain,
output(n0,n1,n0,n1),
inference(cnfTransformation,[status(thm)],[f_42]) ).
tff(c_66,plain,
! [X2_24,Y4_19,Y1_22,X1_20,X3_25,Y3_21,Y2_23,X4_18] :
( output(nand(X1_20,Y1_22),nand(X2_24,Y2_23),nand(X3_25,Y3_21),nand(X4_18,Y4_19))
| ~ output(Y1_22,Y2_23,Y3_21,Y4_19)
| ~ output(X1_20,X2_24,X3_25,X4_18) ),
inference(cnfTransformation,[status(thm)],[f_40]) ).
tff(c_176,plain,
! [Y4_42,X3_40,X4_43,Y3_44,X2_46,X_45,Y2_41] :
( output(n1,nand(X2_46,Y2_41),nand(X3_40,Y3_44),nand(X4_43,Y4_42))
| ~ output(n0,Y2_41,Y3_44,Y4_42)
| ~ output(X_45,X2_46,X3_40,X4_43) ),
inference(superposition,[status(thm),theory(equality)],[c_58,c_66]) ).
tff(c_1130,plain,
! [Y2_126,Y3_127,Y4_128] :
( output(n1,nand(n1,Y2_126),nand(n0,Y3_127),nand(n1,Y4_128))
| ~ output(n0,Y2_126,Y3_127,Y4_128) ),
inference(resolution,[status(thm)],[c_16,c_176]) ).
tff(c_1227,plain,
! [Y2_132,Y3_133] :
( output(n1,nand(n1,Y2_132),nand(n0,Y3_133),n1)
| ~ output(n0,Y2_132,Y3_133,n0) ),
inference(superposition,[status(thm),theory(equality)],[c_58,c_1130]) ).
tff(c_1237,plain,
! [Y3_133] :
( output(n1,not(n1),nand(n0,Y3_133),n1)
| ~ output(n0,n1,Y3_133,n0) ),
inference(superposition,[status(thm),theory(equality)],[c_52,c_1227]) ).
tff(c_1255,plain,
! [Y3_134] :
( output(n1,n0,nand(n0,Y3_134),n1)
| ~ output(n0,n1,Y3_134,n0) ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_1237]) ).
tff(c_1269,plain,
( output(n1,n0,n1,n1)
| ~ output(n0,n1,n0,n0) ),
inference(superposition,[status(thm),theory(equality)],[c_58,c_1255]) ).
tff(c_1339,plain,
~ output(n0,n1,n0,n0),
inference(splitLeft,[status(thm)],[c_1269]) ).
tff(c_14,plain,
output(n0,n0,n1,n1),
inference(cnfTransformation,[status(thm)],[f_41]) ).
tff(c_100,plain,
! [X1_27,X3_29,X_32,X2_33,Y1_28,Y2_30,Y3_31] :
( output(nand(X1_27,Y1_28),nand(X2_33,Y2_30),nand(X3_29,Y3_31),n1)
| ~ output(Y1_28,Y2_30,Y3_31,n0)
| ~ output(X1_27,X2_33,X3_29,X_32) ),
inference(superposition,[status(thm),theory(equality)],[c_58,c_66]) ).
tff(c_110,plain,
! [Y1_34,Y2_35,Y3_36] :
( output(nand(n0,Y1_34),nand(n0,Y2_35),nand(n1,Y3_36),n1)
| ~ output(Y1_34,Y2_35,Y3_36,n0) ),
inference(resolution,[status(thm)],[c_14,c_100]) ).
tff(c_116,plain,
! [Y2_35,Y3_36] :
( output(not(n0),nand(n0,Y2_35),nand(n1,Y3_36),n1)
| ~ output(n1,Y2_35,Y3_36,n0) ),
inference(superposition,[status(thm),theory(equality)],[c_52,c_110]) ).
tff(c_141,plain,
! [Y2_37,Y3_38] :
( output(n1,nand(n0,Y2_37),nand(n1,Y3_38),n1)
| ~ output(n1,Y2_37,Y3_38,n0) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_116]) ).
tff(c_147,plain,
! [Y3_38] :
( output(n1,not(n0),nand(n1,Y3_38),n1)
| ~ output(n1,n1,Y3_38,n0) ),
inference(superposition,[status(thm),theory(equality)],[c_52,c_141]) ).
tff(c_163,plain,
! [Y3_39] :
( output(n1,n1,nand(n1,Y3_39),n1)
| ~ output(n1,n1,Y3_39,n0) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_147]) ).
tff(c_169,plain,
( output(n1,n1,not(n1),n1)
| ~ output(n1,n1,n1,n0) ),
inference(superposition,[status(thm),theory(equality)],[c_52,c_163]) ).
tff(c_175,plain,
( output(n1,n1,n0,n1)
| ~ output(n1,n1,n1,n0) ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_169]) ).
tff(c_195,plain,
~ output(n1,n1,n1,n0),
inference(splitLeft,[status(thm)],[c_175]) ).
tff(c_197,plain,
! [Y2_47,Y3_48,Y4_49] :
( output(n1,nand(n0,Y2_47),nand(n1,Y3_48),nand(n1,Y4_49))
| ~ output(n0,Y2_47,Y3_48,Y4_49) ),
inference(resolution,[status(thm)],[c_14,c_176]) ).
tff(c_349,plain,
! [Y2_63,Y4_64] :
( output(n1,nand(n0,Y2_63),n1,nand(n1,Y4_64))
| ~ output(n0,Y2_63,n0,Y4_64) ),
inference(superposition,[status(thm),theory(equality)],[c_58,c_197]) ).
tff(c_359,plain,
! [Y4_64] :
( output(n1,not(n0),n1,nand(n1,Y4_64))
| ~ output(n0,n1,n0,Y4_64) ),
inference(superposition,[status(thm),theory(equality)],[c_52,c_349]) ).
tff(c_377,plain,
! [Y4_65] :
( output(n1,n1,n1,nand(n1,Y4_65))
| ~ output(n0,n1,n0,Y4_65) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_359]) ).
tff(c_387,plain,
( output(n1,n1,n1,not(n1))
| ~ output(n0,n1,n0,n1) ),
inference(superposition,[status(thm),theory(equality)],[c_52,c_377]) ).
tff(c_396,plain,
output(n1,n1,n1,n0),
inference(demodulation,[status(thm),theory(equality)],[c_16,c_10,c_387]) ).
tff(c_398,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_195,c_396]) ).
tff(c_400,plain,
output(n1,n1,n1,n0),
inference(splitRight,[status(thm)],[c_175]) ).
tff(c_2592,plain,
! [Y1_230,Y2_231,Y3_232] :
( output(nand(n0,Y1_230),nand(n1,Y2_231),nand(n0,Y3_232),n1)
| ~ output(Y1_230,Y2_231,Y3_232,n0) ),
inference(resolution,[status(thm)],[c_16,c_100]) ).
tff(c_2604,plain,
! [Y2_231,Y3_232] :
( output(not(n0),nand(n1,Y2_231),nand(n0,Y3_232),n1)
| ~ output(n1,Y2_231,Y3_232,n0) ),
inference(superposition,[status(thm),theory(equality)],[c_52,c_2592]) ).
tff(c_3181,plain,
! [Y2_258,Y3_259] :
( output(n1,nand(n1,Y2_258),nand(n0,Y3_259),n1)
| ~ output(n1,Y2_258,Y3_259,n0) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_2604]) ).
tff(c_3195,plain,
! [Y3_259] :
( output(n1,not(n1),nand(n0,Y3_259),n1)
| ~ output(n1,n1,Y3_259,n0) ),
inference(superposition,[status(thm),theory(equality)],[c_52,c_3181]) ).
tff(c_3249,plain,
! [Y3_266] :
( output(n1,n0,nand(n0,Y3_266),n1)
| ~ output(n1,n1,Y3_266,n0) ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_3195]) ).
tff(c_3263,plain,
( output(n1,n0,not(n0),n1)
| ~ output(n1,n1,n1,n0) ),
inference(superposition,[status(thm),theory(equality)],[c_52,c_3249]) ).
tff(c_3275,plain,
output(n1,n0,n1,n1),
inference(demodulation,[status(thm),theory(equality)],[c_400,c_8,c_3263]) ).
tff(c_79,plain,
! [X_26] : ( nand(X_26,n1) = not(X_26) ),
inference(superposition,[status(thm),theory(equality)],[c_6,c_43]) ).
tff(c_12,plain,
! [Y1_7,X3_5,X2_10,Y4_12,X1_8,X4_11,Y2_9,Y3_6] :
( output(nand(X1_8,Y1_7),nand(X2_10,Y2_9),nand(X3_5,Y3_6),nand(X4_11,Y4_12))
| ~ output(Y1_7,Y2_9,Y3_6,Y4_12)
| ~ output(X1_8,X2_10,X3_5,X4_11) ),
inference(cnfTransformation,[status(thm)],[f_40]) ).
tff(c_1761,plain,
! [X3_176,X_170,Y3_173,Y4_172,X2_175,X4_171,Y2_174] :
( output(not(X_170),nand(X2_175,Y2_174),nand(X3_176,Y3_173),nand(X4_171,Y4_172))
| ~ output(n1,Y2_174,Y3_173,Y4_172)
| ~ output(X_170,X2_175,X3_176,X4_171) ),
inference(superposition,[status(thm),theory(equality)],[c_79,c_12]) ).
tff(c_5709,plain,
! [X_352,Y4_350,X_353,X3_354,X4_351,Y3_349] :
( output(not(X_353),n1,nand(X3_354,Y3_349),nand(X4_351,Y4_350))
| ~ output(n1,n0,Y3_349,Y4_350)
| ~ output(X_353,X_352,X3_354,X4_351) ),
inference(superposition,[status(thm),theory(equality)],[c_58,c_1761]) ).
tff(c_5765,plain,
! [Y3_349,Y4_350] :
( output(not(n1),n1,nand(n1,Y3_349),nand(n1,Y4_350))
| ~ output(n1,n0,Y3_349,Y4_350) ),
inference(resolution,[status(thm)],[c_3275,c_5709]) ).
tff(c_6906,plain,
! [Y3_379,Y4_380] :
( output(n0,n1,nand(n1,Y3_379),nand(n1,Y4_380))
| ~ output(n1,n0,Y3_379,Y4_380) ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_5765]) ).
tff(c_6932,plain,
! [Y4_380] :
( output(n0,n1,not(n1),nand(n1,Y4_380))
| ~ output(n1,n0,n1,Y4_380) ),
inference(superposition,[status(thm),theory(equality)],[c_52,c_6906]) ).
tff(c_6962,plain,
! [Y4_381] :
( output(n0,n1,n0,nand(n1,Y4_381))
| ~ output(n1,n0,n1,Y4_381) ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_6932]) ).
tff(c_6988,plain,
( output(n0,n1,n0,not(n1))
| ~ output(n1,n0,n1,n1) ),
inference(superposition,[status(thm),theory(equality)],[c_52,c_6962]) ).
tff(c_7010,plain,
output(n0,n1,n0,n0),
inference(demodulation,[status(thm),theory(equality)],[c_3275,c_10,c_6988]) ).
tff(c_7012,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1339,c_7010]) ).
tff(c_7013,plain,
output(n1,n0,n1,n1),
inference(splitRight,[status(thm)],[c_1269]) ).
tff(c_173,plain,
( output(n1,n1,n1,n1)
| ~ output(n1,n1,n0,n0) ),
inference(superposition,[status(thm),theory(equality)],[c_58,c_163]) ).
tff(c_413,plain,
~ output(n1,n1,n0,n0),
inference(splitLeft,[status(thm)],[c_173]) ).
tff(c_414,plain,
! [X1_66,Y4_69,X3_68,X_72,Y3_71,X4_70,Y1_67] :
( output(nand(X1_66,Y1_67),n1,nand(X3_68,Y3_71),nand(X4_70,Y4_69))
| ~ output(Y1_67,n0,Y3_71,Y4_69)
| ~ output(X1_66,X_72,X3_68,X4_70) ),
inference(superposition,[status(thm),theory(equality)],[c_58,c_66]) ).
tff(c_459,plain,
! [Y1_74,Y3_75,Y4_76] :
( output(nand(n0,Y1_74),n1,nand(n1,Y3_75),nand(n1,Y4_76))
| ~ output(Y1_74,n0,Y3_75,Y4_76) ),
inference(resolution,[status(thm)],[c_14,c_414]) ).
tff(c_477,plain,
! [Y1_74,Y3_75] :
( output(nand(n0,Y1_74),n1,nand(n1,Y3_75),not(n1))
| ~ output(Y1_74,n0,Y3_75,n1) ),
inference(superposition,[status(thm),theory(equality)],[c_52,c_459]) ).
tff(c_790,plain,
! [Y1_98,Y3_99] :
( output(nand(n0,Y1_98),n1,nand(n1,Y3_99),n0)
| ~ output(Y1_98,n0,Y3_99,n1) ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_477]) ).
tff(c_806,plain,
! [Y1_98] :
( output(nand(n0,Y1_98),n1,not(n1),n0)
| ~ output(Y1_98,n0,n1,n1) ),
inference(superposition,[status(thm),theory(equality)],[c_52,c_790]) ).
tff(c_948,plain,
! [Y1_112] :
( output(nand(n0,Y1_112),n1,n0,n0)
| ~ output(Y1_112,n0,n1,n1) ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_806]) ).
tff(c_964,plain,
( output(n1,n1,n0,n0)
| ~ output(n0,n0,n1,n1) ),
inference(superposition,[status(thm),theory(equality)],[c_58,c_948]) ).
tff(c_972,plain,
output(n1,n1,n0,n0),
inference(demodulation,[status(thm),theory(equality)],[c_14,c_964]) ).
tff(c_974,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_413,c_972]) ).
tff(c_976,plain,
output(n1,n1,n0,n0),
inference(splitRight,[status(thm)],[c_173]) ).
tff(c_7713,plain,
! [Y2_432,X1_429,X3_434,Y1_431,X2_433,Y3_430,X_428] :
( output(nand(X1_429,Y1_431),nand(X2_433,Y2_432),nand(X3_434,Y3_430),not(X_428))
| ~ output(Y1_431,Y2_432,Y3_430,n1)
| ~ output(X1_429,X2_433,X3_434,X_428) ),
inference(superposition,[status(thm),theory(equality)],[c_79,c_12]) ).
tff(c_12202,plain,
! [X_617,Y1_615,X_613,X1_618,Y3_616,X3_614] :
( output(nand(X1_618,Y1_615),n1,nand(X3_614,Y3_616),not(X_613))
| ~ output(Y1_615,n0,Y3_616,n1)
| ~ output(X1_618,X_617,X3_614,X_613) ),
inference(superposition,[status(thm),theory(equality)],[c_58,c_7713]) ).
tff(c_12416,plain,
! [Y1_615,Y3_616] :
( output(nand(n1,Y1_615),n1,nand(n0,Y3_616),not(n0))
| ~ output(Y1_615,n0,Y3_616,n1) ),
inference(resolution,[status(thm)],[c_976,c_12202]) ).
tff(c_12879,plain,
! [Y1_630,Y3_631] :
( output(nand(n1,Y1_630),n1,nand(n0,Y3_631),n1)
| ~ output(Y1_630,n0,Y3_631,n1) ),
inference(demodulation,[status(thm),theory(equality)],[c_8,c_12416]) ).
tff(c_12905,plain,
! [Y3_631] :
( output(not(n1),n1,nand(n0,Y3_631),n1)
| ~ output(n1,n0,Y3_631,n1) ),
inference(superposition,[status(thm),theory(equality)],[c_52,c_12879]) ).
tff(c_12937,plain,
! [Y3_632] :
( output(n0,n1,nand(n0,Y3_632),n1)
| ~ output(n1,n0,Y3_632,n1) ),
inference(demodulation,[status(thm),theory(equality)],[c_10,c_12905]) ).
tff(c_12963,plain,
( output(n0,n1,not(n0),n1)
| ~ output(n1,n0,n1,n1) ),
inference(superposition,[status(thm),theory(equality)],[c_52,c_12937]) ).
tff(c_12986,plain,
output(n0,n1,n1,n1),
inference(demodulation,[status(thm),theory(equality)],[c_7013,c_8,c_12963]) ).
tff(c_12988,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_18,c_12986]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.10 % Problem : HWC001-1 : TPTP v9.0.0. Bugfixed v1.1.1.
% 0.05/0.10 % 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.10/0.31 % Computer : n025.cluster.edu
% 0.10/0.31 % Model : x86_64 x86_64
% 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.31 % Memory : 8042.1875MB
% 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.31 % CPULimit : 300
% 0.10/0.31 % WCLimit : 300
% 0.10/0.31 % DateTime : Mon Apr 7 22:52:50 EDT 2025
% 0.10/0.32 % CPUTime :
% 11.56/4.21 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.56/4.22
% 11.56/4.22 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------