%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : PUZ026-1 : TPTP v9.0.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n027.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:25:04 PM UTC 2025
% Result : Unsatisfiable 4.01s 2.00s
% Output : CNFRefutation 4.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 17
% Syntax : Number of formulae : 97 ( 53 unt; 0 typ; 0 def)
% Number of atoms : 162 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 164 ( 99 ~; 65 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 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 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-2 aty)
% Number of variables : 83 ( 83 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ people > a_truth > says > #nlpp > truthteller > not_normal > normal > liar > c > b > a
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(not_normal,type,
not_normal: $i > $i ).
tff(a,type,
a: $i ).
tff(liar,type,
liar: $i > $i ).
tff(people,type,
people: ( $i * $i * $i ) > $o ).
tff(b,type,
b: $i ).
tff(normal,type,
normal: $i > $i ).
tff(a_truth,type,
a_truth: $i > $o ).
tff(truthteller,type,
truthteller: $i > $i ).
tff(says,type,
says: ( $i * $i ) > $i ).
tff(c,type,
c: $i ).
tff(f_185,axiom,
a_truth(says(b,normal(a))),
file(unknown,unknown) ).
tff(f_93,axiom,
! [X,Y] :
( ~ a_truth(liar(X))
| ~ a_truth(says(X,Y))
| ~ a_truth(Y) ),
file(unknown,unknown) ).
tff(f_186,axiom,
a_truth(says(c,not_normal(c))),
file(unknown,unknown) ).
tff(f_182,axiom,
people(b,c,a),
file(unknown,unknown) ).
tff(f_195,axiom,
! [Liar,Normal,Truthteller] :
( ~ a_truth(liar(Liar))
| ~ a_truth(normal(Normal))
| ~ a_truth(truthteller(Truthteller)) ),
file(unknown,unknown) ).
tff(f_58,axiom,
! [X] :
( a_truth(truthteller(X))
| a_truth(liar(X))
| a_truth(normal(X)) ),
file(unknown,unknown) ).
tff(f_84,axiom,
! [X,Y] :
( ~ a_truth(truthteller(X))
| ~ a_truth(says(X,Y))
| a_truth(Y) ),
file(unknown,unknown) ).
tff(f_184,axiom,
a_truth(says(a,normal(a))),
file(unknown,unknown) ).
tff(f_171,axiom,
! [X,Y,Z] :
( ~ people(X,Y,Z)
| ~ a_truth(normal(X))
| ~ a_truth(normal(Y)) ),
file(unknown,unknown) ).
tff(f_181,axiom,
people(a,b,c),
file(unknown,unknown) ).
tff(f_64,axiom,
! [X] :
( ~ a_truth(truthteller(X))
| ~ a_truth(normal(X)) ),
file(unknown,unknown) ).
tff(f_180,axiom,
! [X,Y,Z] :
( ~ people(X,Y,Z)
| ~ a_truth(normal(X))
| ~ a_truth(normal(Z)) ),
file(unknown,unknown) ).
tff(f_183,axiom,
people(c,b,a),
file(unknown,unknown) ).
tff(f_135,axiom,
! [X,Y,Z] :
( ~ people(X,Y,Z)
| ~ a_truth(truthteller(X))
| ~ a_truth(truthteller(Y)) ),
file(unknown,unknown) ).
tff(f_162,axiom,
! [X,Y,Z] :
( ~ people(X,Y,Z)
| ~ a_truth(liar(X))
| ~ a_truth(liar(Z)) ),
file(unknown,unknown) ).
tff(f_124,axiom,
! [X] :
( a_truth(not_normal(X))
| a_truth(normal(X)) ),
file(unknown,unknown) ).
tff(f_76,axiom,
! [X] :
( ~ a_truth(liar(X))
| ~ a_truth(normal(X)) ),
file(unknown,unknown) ).
tff(c_42,plain,
a_truth(says(b,normal(a))),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_446,plain,
! [Y_146,X_147] :
( ~ a_truth(Y_146)
| ~ a_truth(says(X_147,Y_146))
| ~ a_truth(liar(X_147)) ),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_456,plain,
( ~ a_truth(normal(a))
| ~ a_truth(liar(b)) ),
inference(resolution,[status(thm)],[c_42,c_446]) ).
tff(c_459,plain,
~ a_truth(liar(b)),
inference(splitLeft,[status(thm)],[c_456]) ).
tff(c_44,plain,
a_truth(says(c,not_normal(c))),
inference(cnfTransformation,[status(thm)],[f_186]) ).
tff(c_458,plain,
( ~ a_truth(not_normal(c))
| ~ a_truth(liar(c)) ),
inference(resolution,[status(thm)],[c_44,c_446]) ).
tff(c_460,plain,
~ a_truth(liar(c)),
inference(splitLeft,[status(thm)],[c_458]) ).
tff(c_36,plain,
people(b,c,a),
inference(cnfTransformation,[status(thm)],[f_182]) ).
tff(c_46,plain,
! [Truthteller_35,Normal_34,Liar_33] :
( ~ a_truth(truthteller(Truthteller_35))
| ~ a_truth(normal(Normal_34))
| ~ a_truth(liar(Liar_33)) ),
inference(cnfTransformation,[status(thm)],[f_195]) ).
tff(c_56,plain,
! [Liar_33] : ~ a_truth(liar(Liar_33)),
inference(splitLeft,[status(thm)],[c_46]) ).
tff(c_2,plain,
! [X_1] :
( a_truth(normal(X_1))
| a_truth(liar(X_1))
| a_truth(truthteller(X_1)) ),
inference(cnfTransformation,[status(thm)],[f_58]) ).
tff(c_58,plain,
! [X_1] :
( a_truth(normal(X_1))
| a_truth(truthteller(X_1)) ),
inference(negUnitSimplification,[status(thm)],[c_56,c_2]) ).
tff(c_64,plain,
! [Y_43,X_44] :
( a_truth(Y_43)
| ~ a_truth(says(X_44,Y_43))
| ~ a_truth(truthteller(X_44)) ),
inference(cnfTransformation,[status(thm)],[f_84]) ).
tff(c_76,plain,
( a_truth(not_normal(c))
| ~ a_truth(truthteller(c)) ),
inference(resolution,[status(thm)],[c_44,c_64]) ).
tff(c_213,plain,
~ a_truth(truthteller(c)),
inference(splitLeft,[status(thm)],[c_76]) ).
tff(c_217,plain,
a_truth(normal(c)),
inference(resolution,[status(thm)],[c_58,c_213]) ).
tff(c_40,plain,
a_truth(says(a,normal(a))),
inference(cnfTransformation,[status(thm)],[f_184]) ).
tff(c_75,plain,
( a_truth(normal(a))
| ~ a_truth(truthteller(a)) ),
inference(resolution,[status(thm)],[c_40,c_64]) ).
tff(c_86,plain,
~ a_truth(truthteller(a)),
inference(splitLeft,[status(thm)],[c_75]) ).
tff(c_90,plain,
a_truth(normal(a)),
inference(resolution,[status(thm)],[c_58,c_86]) ).
tff(c_74,plain,
( a_truth(normal(a))
| ~ a_truth(truthteller(b)) ),
inference(resolution,[status(thm)],[c_42,c_64]) ).
tff(c_77,plain,
~ a_truth(truthteller(b)),
inference(splitLeft,[status(thm)],[c_74]) ).
tff(c_81,plain,
a_truth(normal(b)),
inference(resolution,[status(thm)],[c_58,c_77]) ).
tff(c_82,plain,
! [Y_45,X_46,Z_47] :
( ~ a_truth(normal(Y_45))
| ~ a_truth(normal(X_46))
| ~ people(X_46,Y_45,Z_47) ),
inference(cnfTransformation,[status(thm)],[f_171]) ).
tff(c_173,plain,
! [X_71,Z_72] :
( ~ a_truth(normal(X_71))
| ~ people(X_71,b,Z_72) ),
inference(resolution,[status(thm)],[c_81,c_82]) ).
tff(c_178,plain,
! [Z_72] : ~ people(a,b,Z_72),
inference(resolution,[status(thm)],[c_90,c_173]) ).
tff(c_34,plain,
people(a,b,c),
inference(cnfTransformation,[status(thm)],[f_181]) ).
tff(c_182,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_178,c_34]) ).
tff(c_183,plain,
a_truth(normal(a)),
inference(splitRight,[status(thm)],[c_75]) ).
tff(c_184,plain,
a_truth(truthteller(a)),
inference(splitRight,[status(thm)],[c_75]) ).
tff(c_4,plain,
! [X_2] :
( ~ a_truth(normal(X_2))
| ~ a_truth(truthteller(X_2)) ),
inference(cnfTransformation,[status(thm)],[f_64]) ).
tff(c_196,plain,
~ a_truth(normal(a)),
inference(resolution,[status(thm)],[c_184,c_4]) ).
tff(c_201,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_183,c_196]) ).
tff(c_202,plain,
a_truth(normal(a)),
inference(splitRight,[status(thm)],[c_74]) ).
tff(c_279,plain,
! [Z_104,X_105,Y_106] :
( ~ a_truth(normal(Z_104))
| ~ a_truth(normal(X_105))
| ~ people(X_105,Y_106,Z_104) ),
inference(cnfTransformation,[status(thm)],[f_180]) ).
tff(c_286,plain,
! [X_107,Y_108] :
( ~ a_truth(normal(X_107))
| ~ people(X_107,Y_108,a) ),
inference(resolution,[status(thm)],[c_202,c_279]) ).
tff(c_291,plain,
! [Y_108] : ~ people(c,Y_108,a),
inference(resolution,[status(thm)],[c_217,c_286]) ).
tff(c_38,plain,
people(c,b,a),
inference(cnfTransformation,[status(thm)],[f_183]) ).
tff(c_295,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_291,c_38]) ).
tff(c_297,plain,
a_truth(truthteller(c)),
inference(splitRight,[status(thm)],[c_76]) ).
tff(c_203,plain,
a_truth(truthteller(b)),
inference(splitRight,[status(thm)],[c_74]) ).
tff(c_326,plain,
! [Y_115,X_116,Z_117] :
( ~ a_truth(truthteller(Y_115))
| ~ a_truth(truthteller(X_116))
| ~ people(X_116,Y_115,Z_117) ),
inference(cnfTransformation,[status(thm)],[f_135]) ).
tff(c_338,plain,
! [X_120,Z_121] :
( ~ a_truth(truthteller(X_120))
| ~ people(X_120,b,Z_121) ),
inference(resolution,[status(thm)],[c_203,c_326]) ).
tff(c_345,plain,
! [Z_121] : ~ people(c,b,Z_121),
inference(resolution,[status(thm)],[c_297,c_338]) ).
tff(c_349,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_345,c_38]) ).
tff(c_350,plain,
! [Truthteller_35,Normal_34] :
( ~ a_truth(truthteller(Truthteller_35))
| ~ a_truth(normal(Normal_34)) ),
inference(splitRight,[status(thm)],[c_46]) ).
tff(c_351,plain,
! [Normal_34] : ~ a_truth(normal(Normal_34)),
inference(splitLeft,[status(thm)],[c_350]) ).
tff(c_389,plain,
! [X_128] :
( a_truth(liar(X_128))
| a_truth(truthteller(X_128)) ),
inference(negUnitSimplification,[status(thm)],[c_351,c_2]) ).
tff(c_370,plain,
! [Y_126,X_127] :
( a_truth(Y_126)
| ~ a_truth(says(X_127,Y_126))
| ~ a_truth(truthteller(X_127)) ),
inference(cnfTransformation,[status(thm)],[f_84]) ).
tff(c_373,plain,
( a_truth(normal(a))
| ~ a_truth(truthteller(b)) ),
inference(resolution,[status(thm)],[c_42,c_370]) ).
tff(c_382,plain,
~ a_truth(truthteller(b)),
inference(negUnitSimplification,[status(thm)],[c_351,c_373]) ).
tff(c_400,plain,
a_truth(liar(b)),
inference(resolution,[status(thm)],[c_389,c_382]) ).
tff(c_376,plain,
( a_truth(normal(a))
| ~ a_truth(truthteller(a)) ),
inference(resolution,[status(thm)],[c_40,c_370]) ).
tff(c_385,plain,
~ a_truth(truthteller(a)),
inference(negUnitSimplification,[status(thm)],[c_351,c_376]) ).
tff(c_399,plain,
a_truth(liar(a)),
inference(resolution,[status(thm)],[c_389,c_385]) ).
tff(c_406,plain,
! [Z_132,X_133,Y_134] :
( ~ a_truth(liar(Z_132))
| ~ a_truth(liar(X_133))
| ~ people(X_133,Y_134,Z_132) ),
inference(cnfTransformation,[status(thm)],[f_162]) ).
tff(c_429,plain,
! [X_142,Y_143] :
( ~ a_truth(liar(X_142))
| ~ people(X_142,Y_143,a) ),
inference(resolution,[status(thm)],[c_399,c_406]) ).
tff(c_434,plain,
! [Y_143] : ~ people(b,Y_143,a),
inference(resolution,[status(thm)],[c_400,c_429]) ).
tff(c_437,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_434,c_36]) ).
tff(c_438,plain,
! [Truthteller_35] : ~ a_truth(truthteller(Truthteller_35)),
inference(splitRight,[status(thm)],[c_350]) ).
tff(c_440,plain,
! [X_1] :
( a_truth(normal(X_1))
| a_truth(liar(X_1)) ),
inference(negUnitSimplification,[status(thm)],[c_438,c_2]) ).
tff(c_461,plain,
! [Y_148,X_149,Z_150] :
( ~ a_truth(normal(Y_148))
| ~ a_truth(normal(X_149))
| ~ people(X_149,Y_148,Z_150) ),
inference(cnfTransformation,[status(thm)],[f_171]) ).
tff(c_471,plain,
! [X_160,X_161,Z_162] :
( ~ a_truth(normal(X_160))
| ~ people(X_160,X_161,Z_162)
| a_truth(liar(X_161)) ),
inference(resolution,[status(thm)],[c_440,c_461]) ).
tff(c_479,plain,
! [X_166,X_167,Z_168] :
( ~ people(X_166,X_167,Z_168)
| a_truth(liar(X_167))
| a_truth(liar(X_166)) ),
inference(resolution,[status(thm)],[c_440,c_471]) ).
tff(c_483,plain,
( a_truth(liar(c))
| a_truth(liar(b)) ),
inference(resolution,[status(thm)],[c_36,c_479]) ).
tff(c_492,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_459,c_460,c_483]) ).
tff(c_494,plain,
a_truth(liar(c)),
inference(splitRight,[status(thm)],[c_458]) ).
tff(c_20,plain,
! [X_14] :
( a_truth(normal(X_14))
| a_truth(not_normal(X_14)) ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_493,plain,
~ a_truth(not_normal(c)),
inference(splitRight,[status(thm)],[c_458]) ).
tff(c_502,plain,
a_truth(normal(c)),
inference(resolution,[status(thm)],[c_20,c_493]) ).
tff(c_8,plain,
! [X_4] :
( ~ a_truth(normal(X_4))
| ~ a_truth(liar(X_4)) ),
inference(cnfTransformation,[status(thm)],[f_76]) ).
tff(c_507,plain,
~ a_truth(liar(c)),
inference(resolution,[status(thm)],[c_502,c_8]) ).
tff(c_512,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_494,c_507]) ).
tff(c_514,plain,
a_truth(liar(b)),
inference(splitRight,[status(thm)],[c_456]) ).
tff(c_513,plain,
~ a_truth(normal(a)),
inference(splitRight,[status(thm)],[c_456]) ).
tff(c_518,plain,
a_truth(liar(a)),
inference(resolution,[status(thm)],[c_440,c_513]) ).
tff(c_524,plain,
! [Z_175,X_176,Y_177] :
( ~ a_truth(liar(Z_175))
| ~ a_truth(liar(X_176))
| ~ people(X_176,Y_177,Z_175) ),
inference(cnfTransformation,[status(thm)],[f_162]) ).
tff(c_540,plain,
! [X_182,Y_183] :
( ~ a_truth(liar(X_182))
| ~ people(X_182,Y_183,a) ),
inference(resolution,[status(thm)],[c_518,c_524]) ).
tff(c_546,plain,
! [Y_183] : ~ people(b,Y_183,a),
inference(resolution,[status(thm)],[c_514,c_540]) ).
tff(c_556,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_546,c_36]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : PUZ026-1 : TPTP v9.0.0. Released v1.0.0.
% 0.06/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.34 % Computer : n027.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Tue Apr 8 17:10:21 EDT 2025
% 0.12/0.34 % CPUTime :
% 4.01/2.00 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.01/2.01
% 4.01/2.01 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------