%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYN100-1.005 : TPTP v9.0.0. Bugfixed v1.2.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 : n014.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 10:02:37 PM UTC 2025
% Result : Unsatisfiable 6.56s 2.80s
% Output : CNFRefutation 6.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 18
% Syntax : Number of formulae : 81 ( 37 unt; 0 typ; 0 def)
% Number of atoms : 153 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 152 ( 80 ~; 72 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 45 ( 44 usr; 1 prp; 0-1 aty)
% Number of functors : 1 ( 1 usr; 1 con; 0-0 aty)
% Number of variables : 30 ( 30 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ sym_q_9 > sym_q_8 > sym_q_7 > sym_q_6 > sym_q_5 > sym_q_4 > sym_q_3 > sym_q_2 > sym_q_10 > sym_q_1 > sym_q_0 > sym_p_9 > sym_p_8 > sym_p_7 > sym_p_6 > sym_p_5 > sym_p_4 > sym_p_3 > sym_p_2 > sym_p_10 > sym_p_1 > sym_p_0 > q_9 > q_8 > q_7 > q_6 > q_5 > q_4 > q_3 > q_2 > q_10 > q_1 > q_0 > p_9 > p_8 > p_7 > p_6 > p_5 > p_4 > p_3 > p_2 > p_10 > p_1 > p_0 > #nlpp > a
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(q_8,type,
q_8: $i > $o ).
tff(q_10,type,
q_10: $i > $o ).
tff(q_6,type,
q_6: $i > $o ).
tff(a,type,
a: $i ).
tff(sym_p_7,type,
sym_p_7: $i > $o ).
tff(sym_p_4,type,
sym_p_4: $i > $o ).
tff(q_1,type,
q_1: $i > $o ).
tff(sym_p_10,type,
sym_p_10: $i > $o ).
tff(sym_q_9,type,
sym_q_9: $i > $o ).
tff(q_2,type,
q_2: $i > $o ).
tff(sym_q_7,type,
sym_q_7: $i > $o ).
tff(p_5,type,
p_5: $i > $o ).
tff(p_8,type,
p_8: $i > $o ).
tff(sym_q_8,type,
sym_q_8: $i > $o ).
tff(q_7,type,
q_7: $i > $o ).
tff(sym_p_9,type,
sym_p_9: $i > $o ).
tff(sym_p_3,type,
sym_p_3: $i > $o ).
tff(sym_q_0,type,
sym_q_0: $i > $o ).
tff(sym_p_1,type,
sym_p_1: $i > $o ).
tff(q_0,type,
q_0: $i > $o ).
tff(sym_p_8,type,
sym_p_8: $i > $o ).
tff(p_1,type,
p_1: $i > $o ).
tff(p_10,type,
p_10: $i > $o ).
tff(p_0,type,
p_0: $i > $o ).
tff(sym_q_2,type,
sym_q_2: $i > $o ).
tff(p_9,type,
p_9: $i > $o ).
tff(sym_p_0,type,
sym_p_0: $i > $o ).
tff(q_4,type,
q_4: $i > $o ).
tff(q_5,type,
q_5: $i > $o ).
tff(p_2,type,
p_2: $i > $o ).
tff(sym_q_1,type,
sym_q_1: $i > $o ).
tff(sym_q_4,type,
sym_q_4: $i > $o ).
tff(sym_q_5,type,
sym_q_5: $i > $o ).
tff(p_6,type,
p_6: $i > $o ).
tff(p_4,type,
p_4: $i > $o ).
tff(sym_q_10,type,
sym_q_10: $i > $o ).
tff(sym_p_2,type,
sym_p_2: $i > $o ).
tff(p_7,type,
p_7: $i > $o ).
tff(q_3,type,
q_3: $i > $o ).
tff(sym_q_6,type,
sym_q_6: $i > $o ).
tff(q_9,type,
q_9: $i > $o ).
tff(p_3,type,
p_3: $i > $o ).
tff(sym_q_3,type,
sym_q_3: $i > $o ).
tff(sym_p_5,type,
sym_p_5: $i > $o ).
tff(sym_p_6,type,
sym_p_6: $i > $o ).
tff(f_309,axiom,
q_8(a),
file(unknown,unknown) ).
tff(f_142,axiom,
! [X] :
( p_6(X)
| ~ q_7(X)
| ~ q_8(X) ),
file(unknown,unknown) ).
tff(f_307,axiom,
p_8(a),
file(unknown,unknown) ).
tff(f_310,axiom,
q_9(a),
file(unknown,unknown) ).
tff(f_278,axiom,
! [X] :
( q_7(X)
| ~ p_8(X)
| ~ q_9(X) ),
file(unknown,unknown) ).
tff(f_126,axiom,
! [X] :
( p_5(X)
| ~ q_6(X)
| ~ q_7(X) ),
file(unknown,unknown) ).
tff(f_270,axiom,
! [X] :
( q_6(X)
| ~ q_7(X)
| ~ p_8(X) ),
file(unknown,unknown) ).
tff(f_110,axiom,
! [X] :
( p_4(X)
| ~ q_5(X)
| ~ q_6(X) ),
file(unknown,unknown) ).
tff(f_246,axiom,
! [X] :
( q_5(X)
| ~ p_6(X)
| ~ q_7(X) ),
file(unknown,unknown) ).
tff(f_94,axiom,
! [X] :
( p_3(X)
| ~ q_4(X)
| ~ q_5(X) ),
file(unknown,unknown) ).
tff(f_230,axiom,
! [X] :
( q_4(X)
| ~ p_5(X)
| ~ q_6(X) ),
file(unknown,unknown) ).
tff(f_198,axiom,
! [X] :
( q_2(X)
| ~ p_3(X)
| ~ q_4(X) ),
file(unknown,unknown) ).
tff(f_166,axiom,
! [X] :
( q_0(X)
| ~ p_1(X)
| ~ q_2(X) ),
file(unknown,unknown) ).
tff(f_214,axiom,
! [X] :
( q_3(X)
| ~ p_4(X)
| ~ q_5(X) ),
file(unknown,unknown) ).
tff(f_62,axiom,
! [X] :
( p_1(X)
| ~ q_2(X)
| ~ q_3(X) ),
file(unknown,unknown) ).
tff(f_30,axiom,
! [X] :
( ~ p_0(X)
| ~ q_0(X) ),
file(unknown,unknown) ).
tff(f_70,axiom,
! [X] :
( p_2(X)
| ~ p_3(X)
| ~ p_4(X) ),
file(unknown,unknown) ).
tff(f_38,axiom,
! [X] :
( p_0(X)
| ~ p_1(X)
| ~ p_2(X) ),
file(unknown,unknown) ).
tff(c_80,plain,
q_8(a),
inference(cnfTransformation,[status(thm)],[f_309]) ).
tff(c_175,plain,
! [X_85] :
( ~ q_8(X_85)
| ~ q_7(X_85)
| p_6(X_85) ),
inference(cnfTransformation,[status(thm)],[f_142]) ).
tff(c_179,plain,
( ~ q_7(a)
| p_6(a) ),
inference(resolution,[status(thm)],[c_80,c_175]) ).
tff(c_191,plain,
~ q_7(a),
inference(splitLeft,[status(thm)],[c_179]) ).
tff(c_76,plain,
p_8(a),
inference(cnfTransformation,[status(thm)],[f_307]) ).
tff(c_82,plain,
q_9(a),
inference(cnfTransformation,[status(thm)],[f_310]) ).
tff(c_262,plain,
! [X_111] :
( ~ q_9(X_111)
| ~ p_8(X_111)
| q_7(X_111) ),
inference(cnfTransformation,[status(thm)],[f_278]) ).
tff(c_268,plain,
( ~ p_8(a)
| q_7(a) ),
inference(resolution,[status(thm)],[c_82,c_262]) ).
tff(c_272,plain,
q_7(a),
inference(demodulation,[status(thm),theory(equality)],[c_76,c_268]) ).
tff(c_274,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_191,c_272]) ).
tff(c_276,plain,
q_7(a),
inference(splitRight,[status(thm)],[c_179]) ).
tff(c_291,plain,
! [X_116] :
( ~ q_7(X_116)
| ~ q_6(X_116)
| p_5(X_116) ),
inference(cnfTransformation,[status(thm)],[f_126]) ).
tff(c_295,plain,
( ~ q_6(a)
| p_5(a) ),
inference(resolution,[status(thm)],[c_276,c_291]) ).
tff(c_296,plain,
~ q_6(a),
inference(splitLeft,[status(thm)],[c_295]) ).
tff(c_337,plain,
! [X_135] :
( ~ p_8(X_135)
| ~ q_7(X_135)
| q_6(X_135) ),
inference(cnfTransformation,[status(thm)],[f_270]) ).
tff(c_340,plain,
( ~ p_8(a)
| q_6(a) ),
inference(resolution,[status(thm)],[c_276,c_337]) ).
tff(c_343,plain,
q_6(a),
inference(demodulation,[status(thm),theory(equality)],[c_76,c_340]) ).
tff(c_345,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_296,c_343]) ).
tff(c_347,plain,
q_6(a),
inference(splitRight,[status(thm)],[c_295]) ).
tff(c_22,plain,
! [X_11] :
( ~ q_6(X_11)
| ~ q_5(X_11)
| p_4(X_11) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_355,plain,
( ~ q_5(a)
| p_4(a) ),
inference(resolution,[status(thm)],[c_347,c_22]) ).
tff(c_356,plain,
~ q_5(a),
inference(splitLeft,[status(thm)],[c_355]) ).
tff(c_275,plain,
p_6(a),
inference(splitRight,[status(thm)],[c_179]) ).
tff(c_406,plain,
! [X_152] :
( ~ q_7(X_152)
| ~ p_6(X_152)
| q_5(X_152) ),
inference(cnfTransformation,[status(thm)],[f_246]) ).
tff(c_409,plain,
( ~ p_6(a)
| q_5(a) ),
inference(resolution,[status(thm)],[c_276,c_406]) ).
tff(c_412,plain,
q_5(a),
inference(demodulation,[status(thm),theory(equality)],[c_275,c_409]) ).
tff(c_414,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_356,c_412]) ).
tff(c_416,plain,
q_5(a),
inference(splitRight,[status(thm)],[c_355]) ).
tff(c_18,plain,
! [X_9] :
( ~ q_5(X_9)
| ~ q_4(X_9)
| p_3(X_9) ),
inference(cnfTransformation,[status(thm)],[f_94]) ).
tff(c_423,plain,
( ~ q_4(a)
| p_3(a) ),
inference(resolution,[status(thm)],[c_416,c_18]) ).
tff(c_425,plain,
~ q_4(a),
inference(splitLeft,[status(thm)],[c_423]) ).
tff(c_346,plain,
p_5(a),
inference(splitRight,[status(thm)],[c_295]) ).
tff(c_474,plain,
! [X_164] :
( ~ q_6(X_164)
| ~ p_5(X_164)
| q_4(X_164) ),
inference(cnfTransformation,[status(thm)],[f_230]) ).
tff(c_477,plain,
( ~ p_5(a)
| q_4(a) ),
inference(resolution,[status(thm)],[c_347,c_474]) ).
tff(c_480,plain,
q_4(a),
inference(demodulation,[status(thm),theory(equality)],[c_346,c_477]) ).
tff(c_482,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_425,c_480]) ).
tff(c_483,plain,
p_3(a),
inference(splitRight,[status(thm)],[c_423]) ).
tff(c_484,plain,
q_4(a),
inference(splitRight,[status(thm)],[c_423]) ).
tff(c_497,plain,
! [X_171] :
( ~ q_4(X_171)
| ~ p_3(X_171)
| q_2(X_171) ),
inference(cnfTransformation,[status(thm)],[f_198]) ).
tff(c_500,plain,
( ~ p_3(a)
| q_2(a) ),
inference(resolution,[status(thm)],[c_484,c_497]) ).
tff(c_503,plain,
q_2(a),
inference(demodulation,[status(thm),theory(equality)],[c_483,c_500]) ).
tff(c_36,plain,
! [X_18] :
( ~ q_2(X_18)
| ~ p_1(X_18)
| q_0(X_18) ),
inference(cnfTransformation,[status(thm)],[f_166]) ).
tff(c_514,plain,
( ~ p_1(a)
| q_0(a) ),
inference(resolution,[status(thm)],[c_503,c_36]) ).
tff(c_519,plain,
~ p_1(a),
inference(splitLeft,[status(thm)],[c_514]) ).
tff(c_415,plain,
p_4(a),
inference(splitRight,[status(thm)],[c_355]) ).
tff(c_523,plain,
! [X_175] :
( ~ q_5(X_175)
| ~ p_4(X_175)
| q_3(X_175) ),
inference(cnfTransformation,[status(thm)],[f_214]) ).
tff(c_526,plain,
( ~ p_4(a)
| q_3(a) ),
inference(resolution,[status(thm)],[c_416,c_523]) ).
tff(c_529,plain,
q_3(a),
inference(demodulation,[status(thm),theory(equality)],[c_415,c_526]) ).
tff(c_693,plain,
! [X_193] :
( ~ q_3(X_193)
| ~ q_2(X_193)
| p_1(X_193) ),
inference(cnfTransformation,[status(thm)],[f_62]) ).
tff(c_696,plain,
( ~ q_2(a)
| p_1(a) ),
inference(resolution,[status(thm)],[c_529,c_693]) ).
tff(c_699,plain,
p_1(a),
inference(demodulation,[status(thm),theory(equality)],[c_503,c_696]) ).
tff(c_701,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_519,c_699]) ).
tff(c_702,plain,
q_0(a),
inference(splitRight,[status(thm)],[c_514]) ).
tff(c_2,plain,
! [X_1] :
( ~ q_0(X_1)
| ~ p_0(X_1) ),
inference(cnfTransformation,[status(thm)],[f_30]) ).
tff(c_707,plain,
~ p_0(a),
inference(resolution,[status(thm)],[c_702,c_2]) ).
tff(c_703,plain,
p_1(a),
inference(splitRight,[status(thm)],[c_514]) ).
tff(c_892,plain,
! [X_218] :
( ~ p_4(X_218)
| ~ p_3(X_218)
| p_2(X_218) ),
inference(cnfTransformation,[status(thm)],[f_70]) ).
tff(c_895,plain,
( ~ p_3(a)
| p_2(a) ),
inference(resolution,[status(thm)],[c_415,c_892]) ).
tff(c_898,plain,
p_2(a),
inference(demodulation,[status(thm),theory(equality)],[c_483,c_895]) ).
tff(c_4,plain,
! [X_2] :
( ~ p_2(X_2)
| ~ p_1(X_2)
| p_0(X_2) ),
inference(cnfTransformation,[status(thm)],[f_38]) ).
tff(c_901,plain,
( ~ p_1(a)
| p_0(a) ),
inference(resolution,[status(thm)],[c_898,c_4]) ).
tff(c_904,plain,
p_0(a),
inference(demodulation,[status(thm),theory(equality)],[c_703,c_901]) ).
tff(c_906,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_707,c_904]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.09 % Problem : SYN100-1.005 : TPTP v9.0.0. Bugfixed v1.2.1.
% 0.04/0.09 % 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.08/0.30 % Computer : n014.cluster.edu
% 0.08/0.30 % Model : x86_64 x86_64
% 0.08/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.30 % Memory : 8042.1875MB
% 0.08/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.30 % CPULimit : 300
% 0.08/0.30 % WCLimit : 300
% 0.08/0.30 % DateTime : Wed Apr 9 06:57:19 EDT 2025
% 0.08/0.30 % CPUTime :
% 6.56/2.80 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.56/2.81
% 6.56/2.81 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------