%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYN037-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 : n013.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:14 PM UTC 2025
% Result : Unsatisfiable 4.22s 2.01s
% Output : CNFRefutation 4.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 35
% Syntax : Number of formulae : 292 ( 195 unt; 0 typ; 0 def)
% Number of atoms : 449 ( 0 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 357 ( 200 ~; 157 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 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 : 13 ( 12 usr; 9 prp; 0-1 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-1 aty)
% Number of variables : 111 ( 111 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ q > p > n5 > n1 > #nlpp > s5 > s1 > s8 > s7 > s6 > s4 > s3 > s2 > n9 > n8 > n7 > n6 > n4 > n3 > n2 > n10
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(n7,type,
n7: $o ).
tff(s7,type,
s7: $i ).
tff(s1,type,
s1: $i > $i ).
tff(n4,type,
n4: $o ).
tff(n10,type,
n10: $o ).
tff(s4,type,
s4: $i ).
tff(q,type,
q: $i > $o ).
tff(s3,type,
s3: $i ).
tff(s2,type,
s2: $i ).
tff(p,type,
p: $i > $o ).
tff(n5,type,
n5: $i > $o ).
tff(n8,type,
n8: $o ).
tff(n9,type,
n9: $o ).
tff(n3,type,
n3: $o ).
tff(s5,type,
s5: $i > $i ).
tff(n6,type,
n6: $o ).
tff(s6,type,
s6: $i ).
tff(n1,type,
n1: $i > $o ).
tff(s8,type,
s8: $i ).
tff(n2,type,
n2: $o ).
tff(f_175,axiom,
! [X4] :
( ~ n1(X4)
| n2 ),
file(unknown,unknown) ).
tff(f_209,axiom,
! [X,X3] :
( ~ n1(X)
| p(X)
| ~ p(X3) ),
file(unknown,unknown) ).
tff(f_144,axiom,
! [W,X7] :
( ~ n5(W)
| ~ q(X7)
| q(W) ),
file(unknown,unknown) ).
tff(f_170,axiom,
( ~ n3
| q(s3) ),
file(unknown,unknown) ).
tff(f_261,axiom,
( n7
| ~ n8
| ~ n10 ),
file(unknown,unknown) ).
tff(f_254,axiom,
( ~ n7
| n8
| ~ n10 ),
file(unknown,unknown) ).
tff(f_109,axiom,
! [X9] :
( ~ p(X9)
| n7 ),
file(unknown,unknown) ).
tff(f_193,axiom,
! [X] :
( p(X)
| p(s1(X))
| n1(X) ),
file(unknown,unknown) ).
tff(f_166,axiom,
! [X5] :
( ~ q(X5)
| n3 ),
file(unknown,unknown) ).
tff(f_161,axiom,
! [X6] :
( ~ n4
| p(X6) ),
file(unknown,unknown) ).
tff(f_221,axiom,
( n3
| n4
| n9 ),
file(unknown,unknown) ).
tff(f_122,axiom,
( ~ n6
| n5(s6) ),
file(unknown,unknown) ).
tff(f_118,axiom,
! [X8] :
( ~ n5(X8)
| n6 ),
file(unknown,unknown) ).
tff(f_136,axiom,
! [W] :
( q(s5(W))
| q(W)
| n5(W) ),
file(unknown,unknown) ).
tff(f_247,axiom,
( n7
| n8
| n10 ),
file(unknown,unknown) ).
tff(f_34,axiom,
( ~ n2
| ~ n9
| ~ n6
| ~ n10 ),
file(unknown,unknown) ).
tff(f_152,axiom,
! [W,X7] :
( ~ n5(W)
| q(X7)
| ~ q(W) ),
file(unknown,unknown) ).
tff(f_228,axiom,
( ~ n3
| n4
| ~ n9 ),
file(unknown,unknown) ).
tff(f_77,axiom,
( ~ n2
| n9
| n6
| ~ n10 ),
file(unknown,unknown) ).
tff(f_99,axiom,
( ~ q(s8)
| n8 ),
file(unknown,unknown) ).
tff(f_113,axiom,
( ~ n7
| p(s7) ),
file(unknown,unknown) ).
tff(f_201,axiom,
! [X,X3] :
( ~ n1(X)
| ~ p(X)
| p(X3) ),
file(unknown,unknown) ).
tff(f_179,axiom,
( ~ n2
| n1(s2) ),
file(unknown,unknown) ).
tff(f_86,axiom,
( n2
| ~ n9
| ~ n6
| n10 ),
file(unknown,unknown) ).
tff(f_156,axiom,
( ~ p(s4)
| n4 ),
file(unknown,unknown) ).
tff(f_59,axiom,
( n2
| n9
| n6
| n10 ),
file(unknown,unknown) ).
tff(f_235,axiom,
( n3
| ~ n4
| ~ n9 ),
file(unknown,unknown) ).
tff(f_187,axiom,
! [X] :
( ~ p(X)
| ~ p(s1(X))
| n1(X) ),
file(unknown,unknown) ).
tff(f_68,axiom,
( ~ n2
| n9
| ~ n6
| n10 ),
file(unknown,unknown) ).
tff(f_216,axiom,
( ~ n3
| ~ n4
| n9 ),
file(unknown,unknown) ).
tff(f_43,axiom,
( ~ n2
| ~ n9
| n6
| n10 ),
file(unknown,unknown) ).
tff(f_242,axiom,
( ~ n7
| ~ n8
| n10 ),
file(unknown,unknown) ).
tff(f_104,axiom,
! [X10] :
( ~ n8
| q(X10) ),
file(unknown,unknown) ).
tff(f_130,axiom,
! [W] :
( ~ q(s5(W))
| ~ q(W)
| n5(W) ),
file(unknown,unknown) ).
tff(f_52,axiom,
( n2
| n9
| ~ n6
| ~ n10 ),
file(unknown,unknown) ).
tff(c_46,plain,
! [X4_12] :
( n2
| ~ n1(X4_12) ),
inference(cnfTransformation,[status(thm)],[f_175]) ).
tff(c_1579,plain,
! [X4_12] : ~ n1(X4_12),
inference(splitLeft,[status(thm)],[c_46]) ).
tff(c_56,plain,
! [X3_18,X_17] :
( ~ p(X3_18)
| p(X_17)
| ~ n1(X_17) ),
inference(cnfTransformation,[status(thm)],[f_209]) ).
tff(c_1546,plain,
! [X3_18] : ~ p(X3_18),
inference(splitLeft,[status(thm)],[c_56]) ).
tff(c_34,plain,
! [W_6,X7_7] :
( q(W_6)
| ~ q(X7_7)
| ~ n5(W_6) ),
inference(cnfTransformation,[status(thm)],[f_144]) ).
tff(c_1088,plain,
! [X7_7] : ~ q(X7_7),
inference(splitLeft,[status(thm)],[c_34]) ).
tff(c_44,plain,
( q(s3)
| ~ n3 ),
inference(cnfTransformation,[status(thm)],[f_170]) ).
tff(c_788,plain,
~ n3,
inference(splitLeft,[status(thm)],[c_44]) ).
tff(c_754,plain,
! [X7_7] : ~ q(X7_7),
inference(splitLeft,[status(thm)],[c_34]) ).
tff(c_590,plain,
! [X3_18] : ~ p(X3_18),
inference(splitLeft,[status(thm)],[c_56]) ).
tff(c_72,plain,
( ~ n10
| ~ n8
| n7 ),
inference(cnfTransformation,[status(thm)],[f_261]) ).
tff(c_73,plain,
~ n8,
inference(splitLeft,[status(thm)],[c_72]) ).
tff(c_70,plain,
( ~ n10
| n8
| ~ n7 ),
inference(cnfTransformation,[status(thm)],[f_254]) ).
tff(c_74,plain,
( ~ n10
| ~ n7 ),
inference(negUnitSimplification,[status(thm)],[c_73,c_70]) ).
tff(c_75,plain,
~ n7,
inference(splitLeft,[status(thm)],[c_74]) ).
tff(c_390,plain,
! [X7_7] : ~ q(X7_7),
inference(splitLeft,[status(thm)],[c_34]) ).
tff(c_22,plain,
! [X9_2] :
( n7
| ~ p(X9_2) ),
inference(cnfTransformation,[status(thm)],[f_109]) ).
tff(c_152,plain,
! [X9_2] : ~ p(X9_2),
inference(negUnitSimplification,[status(thm)],[c_75,c_22]) ).
tff(c_149,plain,
! [X4_12] : ~ n1(X4_12),
inference(splitLeft,[status(thm)],[c_46]) ).
tff(c_52,plain,
! [X_14] :
( n1(X_14)
| p(s1(X_14))
| p(X_14) ),
inference(cnfTransformation,[status(thm)],[f_193]) ).
tff(c_188,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_152,c_152,c_149,c_52]) ).
tff(c_189,plain,
n2,
inference(splitRight,[status(thm)],[c_46]) ).
tff(c_42,plain,
! [X5_11] :
( n3
| ~ q(X5_11) ),
inference(cnfTransformation,[status(thm)],[f_166]) ).
tff(c_76,plain,
! [X5_11] : ~ q(X5_11),
inference(splitLeft,[status(thm)],[c_42]) ).
tff(c_79,plain,
~ n3,
inference(negUnitSimplification,[status(thm)],[c_76,c_44]) ).
tff(c_40,plain,
! [X6_10] :
( p(X6_10)
| ~ n4 ),
inference(cnfTransformation,[status(thm)],[f_161]) ).
tff(c_78,plain,
~ n4,
inference(splitLeft,[status(thm)],[c_40]) ).
tff(c_60,plain,
( n9
| n4
| n3 ),
inference(cnfTransformation,[status(thm)],[f_221]) ).
tff(c_199,plain,
n9,
inference(negUnitSimplification,[status(thm)],[c_79,c_78,c_60]) ).
tff(c_28,plain,
( n5(s6)
| ~ n6 ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_82,plain,
~ n6,
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_26,plain,
! [X8_3] :
( n6
| ~ n5(X8_3) ),
inference(cnfTransformation,[status(thm)],[f_118]) ).
tff(c_111,plain,
! [X8_3] : ~ n5(X8_3),
inference(negUnitSimplification,[status(thm)],[c_82,c_26]) ).
tff(c_32,plain,
! [W_5] :
( n5(W_5)
| q(W_5)
| q(s5(W_5)) ),
inference(cnfTransformation,[status(thm)],[f_136]) ).
tff(c_146,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_76,c_76,c_111,c_32]) ).
tff(c_148,plain,
n6,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_68,plain,
( n10
| n8
| n7 ),
inference(cnfTransformation,[status(thm)],[f_247]) ).
tff(c_200,plain,
n10,
inference(negUnitSimplification,[status(thm)],[c_75,c_73,c_68]) ).
tff(c_2,plain,
( ~ n10
| ~ n6
| ~ n9
| ~ n2 ),
inference(cnfTransformation,[status(thm)],[f_34]) ).
tff(c_215,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_189,c_199,c_148,c_200,c_2]) ).
tff(c_216,plain,
! [X6_10] : p(X6_10),
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_237,plain,
n7,
inference(demodulation,[status(thm),theory(equality)],[c_216,c_22]) ).
tff(c_238,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_75,c_237]) ).
tff(c_239,plain,
n3,
inference(splitRight,[status(thm)],[c_42]) ).
tff(c_243,plain,
q(s3),
inference(demodulation,[status(thm),theory(equality)],[c_239,c_44]) ).
tff(c_392,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_390,c_243]) ).
tff(c_393,plain,
! [W_6] :
( q(W_6)
| ~ n5(W_6) ),
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_36,plain,
! [W_8,X7_9] :
( ~ q(W_8)
| q(X7_9)
| ~ n5(W_8) ),
inference(cnfTransformation,[status(thm)],[f_152]) ).
tff(c_401,plain,
! [W_44] :
( ~ q(W_44)
| ~ n5(W_44) ),
inference(splitLeft,[status(thm)],[c_36]) ).
tff(c_408,plain,
! [W_6] : ~ n5(W_6),
inference(resolution,[status(thm)],[c_393,c_401]) ).
tff(c_240,plain,
~ n4,
inference(splitLeft,[status(thm)],[c_40]) ).
tff(c_62,plain,
( ~ n9
| n4
| ~ n3 ),
inference(cnfTransformation,[status(thm)],[f_228]) ).
tff(c_304,plain,
( ~ n9
| n4 ),
inference(demodulation,[status(thm),theory(equality)],[c_239,c_62]) ).
tff(c_305,plain,
~ n9,
inference(negUnitSimplification,[status(thm)],[c_240,c_304]) ).
tff(c_245,plain,
~ n6,
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_251,plain,
! [X9_2] : ~ p(X9_2),
inference(negUnitSimplification,[status(thm)],[c_75,c_22]) ).
tff(c_248,plain,
! [X4_12] : ~ n1(X4_12),
inference(splitLeft,[status(thm)],[c_46]) ).
tff(c_293,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_251,c_251,c_248,c_52]) ).
tff(c_294,plain,
n2,
inference(splitRight,[status(thm)],[c_46]) ).
tff(c_308,plain,
n10,
inference(negUnitSimplification,[status(thm)],[c_75,c_73,c_68]) ).
tff(c_12,plain,
( ~ n10
| n6
| n9
| ~ n2 ),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_320,plain,
( n6
| n9 ),
inference(demodulation,[status(thm),theory(equality)],[c_294,c_308,c_12]) ).
tff(c_321,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_305,c_245,c_320]) ).
tff(c_322,plain,
n5(s6),
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_411,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_408,c_322]) ).
tff(c_412,plain,
! [X7_9] : q(X7_9),
inference(splitRight,[status(thm)],[c_36]) ).
tff(c_18,plain,
( n8
| ~ q(s8) ),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_369,plain,
~ q(s8),
inference(negUnitSimplification,[status(thm)],[c_73,c_18]) ).
tff(c_417,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_412,c_369]) ).
tff(c_418,plain,
! [X6_10] : p(X6_10),
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_442,plain,
n7,
inference(demodulation,[status(thm),theory(equality)],[c_418,c_22]) ).
tff(c_443,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_75,c_442]) ).
tff(c_445,plain,
n7,
inference(splitRight,[status(thm)],[c_74]) ).
tff(c_24,plain,
( p(s7)
| ~ n7 ),
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_566,plain,
p(s7),
inference(demodulation,[status(thm),theory(equality)],[c_445,c_24]) ).
tff(c_592,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_590,c_566]) ).
tff(c_593,plain,
! [X_17] :
( p(X_17)
| ~ n1(X_17) ),
inference(splitRight,[status(thm)],[c_56]) ).
tff(c_54,plain,
! [X3_16,X_15] :
( p(X3_16)
| ~ p(X_15)
| ~ n1(X_15) ),
inference(cnfTransformation,[status(thm)],[f_201]) ).
tff(c_600,plain,
! [X_54] :
( ~ p(X_54)
| ~ n1(X_54) ),
inference(splitLeft,[status(thm)],[c_54]) ).
tff(c_607,plain,
! [X_17] : ~ n1(X_17),
inference(resolution,[status(thm)],[c_593,c_600]) ).
tff(c_455,plain,
! [X4_12] : ~ n1(X4_12),
inference(splitLeft,[status(thm)],[c_46]) ).
tff(c_48,plain,
( n1(s2)
| ~ n2 ),
inference(cnfTransformation,[status(thm)],[f_179]) ).
tff(c_457,plain,
~ n2,
inference(negUnitSimplification,[status(thm)],[c_455,c_48]) ).
tff(c_444,plain,
~ n10,
inference(splitRight,[status(thm)],[c_74]) ).
tff(c_450,plain,
~ n3,
inference(splitLeft,[status(thm)],[c_44]) ).
tff(c_451,plain,
~ n4,
inference(splitLeft,[status(thm)],[c_40]) ).
tff(c_454,plain,
n9,
inference(negUnitSimplification,[status(thm)],[c_450,c_451,c_60]) ).
tff(c_452,plain,
! [X5_11] : ~ q(X5_11),
inference(negUnitSimplification,[status(thm)],[c_450,c_42]) ).
tff(c_462,plain,
~ n6,
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_466,plain,
! [X8_3] : ~ n5(X8_3),
inference(negUnitSimplification,[status(thm)],[c_462,c_26]) ).
tff(c_498,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_452,c_452,c_466,c_32]) ).
tff(c_500,plain,
n6,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_14,plain,
( n10
| ~ n6
| ~ n9
| n2 ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_521,plain,
( n10
| n2 ),
inference(demodulation,[status(thm),theory(equality)],[c_454,c_500,c_14]) ).
tff(c_522,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_457,c_444,c_521]) ).
tff(c_523,plain,
n2,
inference(splitRight,[status(thm)],[c_46]) ).
tff(c_525,plain,
n1(s2),
inference(demodulation,[status(thm),theory(equality)],[c_523,c_48]) ).
tff(c_610,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_607,c_525]) ).
tff(c_611,plain,
! [X3_16] : p(X3_16),
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_38,plain,
( n4
| ~ p(s4) ),
inference(cnfTransformation,[status(thm)],[f_156]) ).
tff(c_446,plain,
~ p(s4),
inference(splitLeft,[status(thm)],[c_38]) ).
tff(c_615,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_611,c_446]) ).
tff(c_616,plain,
! [X6_10] : p(X6_10),
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_620,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_616,c_446]) ).
tff(c_621,plain,
q(s3),
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_756,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_754,c_621]) ).
tff(c_757,plain,
! [W_6] :
( q(W_6)
| ~ n5(W_6) ),
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_764,plain,
! [W_62] :
( ~ q(W_62)
| ~ n5(W_62) ),
inference(splitLeft,[status(thm)],[c_36]) ).
tff(c_771,plain,
! [W_6] : ~ n5(W_6),
inference(resolution,[status(thm)],[c_757,c_764]) ).
tff(c_689,plain,
! [X3_18] : ~ p(X3_18),
inference(splitLeft,[status(thm)],[c_56]) ).
tff(c_663,plain,
p(s7),
inference(demodulation,[status(thm),theory(equality)],[c_445,c_24]) ).
tff(c_691,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_689,c_663]) ).
tff(c_692,plain,
! [X_17] :
( p(X_17)
| ~ n1(X_17) ),
inference(splitRight,[status(thm)],[c_56]) ).
tff(c_699,plain,
! [X_59] :
( ~ p(X_59)
| ~ n1(X_59) ),
inference(splitLeft,[status(thm)],[c_54]) ).
tff(c_706,plain,
! [X_17] : ~ n1(X_17),
inference(resolution,[status(thm)],[c_692,c_699]) ).
tff(c_627,plain,
! [X4_12] : ~ n1(X4_12),
inference(splitLeft,[status(thm)],[c_46]) ).
tff(c_629,plain,
~ n2,
inference(negUnitSimplification,[status(thm)],[c_627,c_48]) ).
tff(c_623,plain,
~ n4,
inference(splitLeft,[status(thm)],[c_40]) ).
tff(c_622,plain,
n3,
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_631,plain,
( ~ n9
| n4 ),
inference(demodulation,[status(thm),theory(equality)],[c_622,c_62]) ).
tff(c_632,plain,
~ n9,
inference(negUnitSimplification,[status(thm)],[c_623,c_631]) ).
tff(c_626,plain,
~ n6,
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_8,plain,
( n10
| n6
| n9
| n2 ),
inference(cnfTransformation,[status(thm)],[f_59]) ).
tff(c_650,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_629,c_632,c_626,c_444,c_8]) ).
tff(c_651,plain,
n2,
inference(splitRight,[status(thm)],[c_46]) ).
tff(c_653,plain,
n1(s2),
inference(demodulation,[status(thm),theory(equality)],[c_651,c_48]) ).
tff(c_709,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_706,c_653]) ).
tff(c_710,plain,
! [X3_16] : p(X3_16),
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_715,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_710,c_446]) ).
tff(c_716,plain,
n5(s6),
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_774,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_771,c_716]) ).
tff(c_775,plain,
! [X7_9] : q(X7_9),
inference(splitRight,[status(thm)],[c_36]) ).
tff(c_720,plain,
~ q(s8),
inference(negUnitSimplification,[status(thm)],[c_73,c_18]) ).
tff(c_780,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_775,c_720]) ).
tff(c_781,plain,
! [X6_10] : p(X6_10),
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_785,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_781,c_446]) ).
tff(c_786,plain,
n4,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_64,plain,
( ~ n9
| ~ n4
| n3 ),
inference(cnfTransformation,[status(thm)],[f_235]) ).
tff(c_921,plain,
( ~ n9
| n3 ),
inference(demodulation,[status(thm),theory(equality)],[c_786,c_64]) ).
tff(c_922,plain,
~ n9,
inference(negUnitSimplification,[status(thm)],[c_788,c_921]) ).
tff(c_802,plain,
! [X4_12] : ~ n1(X4_12),
inference(splitLeft,[status(thm)],[c_46]) ).
tff(c_797,plain,
! [X6_10] : p(X6_10),
inference(demodulation,[status(thm),theory(equality)],[c_786,c_40]) ).
tff(c_50,plain,
! [X_13] :
( n1(X_13)
| ~ p(s1(X_13))
| ~ p(X_13) ),
inference(cnfTransformation,[status(thm)],[f_187]) ).
tff(c_865,plain,
! [X_13] : n1(X_13),
inference(demodulation,[status(thm),theory(equality)],[c_797,c_797,c_50]) ).
tff(c_866,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_802,c_865]) ).
tff(c_867,plain,
n2,
inference(splitRight,[status(thm)],[c_46]) ).
tff(c_792,plain,
! [X5_11] : ~ q(X5_11),
inference(negUnitSimplification,[status(thm)],[c_788,c_42]) ).
tff(c_868,plain,
! [X8_3] : ~ n5(X8_3),
inference(splitLeft,[status(thm)],[c_26]) ).
tff(c_916,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_792,c_792,c_868,c_32]) ).
tff(c_917,plain,
n6,
inference(splitRight,[status(thm)],[c_26]) ).
tff(c_10,plain,
( n10
| ~ n6
| n9
| ~ n2 ),
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_942,plain,
( n10
| n9 ),
inference(demodulation,[status(thm),theory(equality)],[c_867,c_917,c_10]) ).
tff(c_943,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_922,c_444,c_942]) ).
tff(c_944,plain,
q(s3),
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_1090,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1088,c_944]) ).
tff(c_1096,plain,
! [W_79] :
( q(W_79)
| ~ n5(W_79) ),
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_1082,plain,
! [W_8] :
( ~ q(W_8)
| ~ n5(W_8) ),
inference(splitLeft,[status(thm)],[c_36]) ).
tff(c_1103,plain,
! [W_79] : ~ n5(W_79),
inference(resolution,[status(thm)],[c_1096,c_1082]) ).
tff(c_1007,plain,
~ n6,
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_949,plain,
! [X4_12] : ~ n1(X4_12),
inference(splitLeft,[status(thm)],[c_46]) ).
tff(c_958,plain,
! [X6_10] : p(X6_10),
inference(demodulation,[status(thm),theory(equality)],[c_786,c_40]) ).
tff(c_1000,plain,
! [X_13] : n1(X_13),
inference(demodulation,[status(thm),theory(equality)],[c_958,c_958,c_50]) ).
tff(c_1001,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_949,c_1000]) ).
tff(c_1002,plain,
n2,
inference(splitRight,[status(thm)],[c_46]) ).
tff(c_945,plain,
n3,
inference(splitRight,[status(thm)],[c_44]) ).
tff(c_58,plain,
( n9
| ~ n4
| ~ n3 ),
inference(cnfTransformation,[status(thm)],[f_216]) ).
tff(c_1004,plain,
n9,
inference(demodulation,[status(thm),theory(equality)],[c_945,c_786,c_58]) ).
tff(c_4,plain,
( n10
| n6
| ~ n9
| ~ n2 ),
inference(cnfTransformation,[status(thm)],[f_43]) ).
tff(c_1037,plain,
( n10
| n6 ),
inference(demodulation,[status(thm),theory(equality)],[c_1002,c_1004,c_4]) ).
tff(c_1038,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1007,c_444,c_1037]) ).
tff(c_1039,plain,
n5(s6),
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_1106,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1103,c_1039]) ).
tff(c_1107,plain,
! [X7_9] : q(X7_9),
inference(splitRight,[status(thm)],[c_36]) ).
tff(c_1045,plain,
~ q(s8),
inference(negUnitSimplification,[status(thm)],[c_73,c_18]) ).
tff(c_1111,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1107,c_1045]) ).
tff(c_1112,plain,
( ~ n10
| n7 ),
inference(splitRight,[status(thm)],[c_72]) ).
tff(c_1114,plain,
~ n10,
inference(splitLeft,[status(thm)],[c_1112]) ).
tff(c_1113,plain,
n8,
inference(splitRight,[status(thm)],[c_72]) ).
tff(c_66,plain,
( n10
| ~ n8
| ~ n7 ),
inference(cnfTransformation,[status(thm)],[f_242]) ).
tff(c_1313,plain,
( n10
| ~ n7 ),
inference(demodulation,[status(thm),theory(equality)],[c_1113,c_66]) ).
tff(c_1314,plain,
~ n7,
inference(negUnitSimplification,[status(thm)],[c_1114,c_1313]) ).
tff(c_1115,plain,
~ n4,
inference(splitLeft,[status(thm)],[c_40]) ).
tff(c_1116,plain,
! [X5_11] : ~ q(X5_11),
inference(splitLeft,[status(thm)],[c_42]) ).
tff(c_20,plain,
! [X10_1] :
( q(X10_1)
| ~ n8 ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_1130,plain,
! [X10_1] : q(X10_1),
inference(demodulation,[status(thm),theory(equality)],[c_1113,c_20]) ).
tff(c_1131,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1116,c_1130]) ).
tff(c_1132,plain,
n3,
inference(splitRight,[status(thm)],[c_42]) ).
tff(c_1275,plain,
( ~ n9
| n4 ),
inference(demodulation,[status(thm),theory(equality)],[c_1132,c_62]) ).
tff(c_1276,plain,
~ n9,
inference(negUnitSimplification,[status(thm)],[c_1115,c_1275]) ).
tff(c_1136,plain,
( n10
| ~ n7 ),
inference(demodulation,[status(thm),theory(equality)],[c_1113,c_66]) ).
tff(c_1137,plain,
~ n7,
inference(negUnitSimplification,[status(thm)],[c_1114,c_1136]) ).
tff(c_1181,plain,
! [X9_2] : ~ p(X9_2),
inference(negUnitSimplification,[status(thm)],[c_1137,c_22]) ).
tff(c_1140,plain,
! [X4_12] : ~ n1(X4_12),
inference(splitLeft,[status(thm)],[c_46]) ).
tff(c_1213,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1181,c_1181,c_1140,c_52]) ).
tff(c_1214,plain,
n2,
inference(splitRight,[status(thm)],[c_46]) ).
tff(c_1218,plain,
~ n6,
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_1224,plain,
! [X8_3] : ~ n5(X8_3),
inference(negUnitSimplification,[status(thm)],[c_1218,c_26]) ).
tff(c_1233,plain,
! [X10_1] : q(X10_1),
inference(demodulation,[status(thm),theory(equality)],[c_1113,c_20]) ).
tff(c_30,plain,
! [W_4] :
( n5(W_4)
| ~ q(W_4)
| ~ q(s5(W_4)) ),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_1263,plain,
! [W_4] : n5(W_4),
inference(demodulation,[status(thm),theory(equality)],[c_1233,c_1233,c_30]) ).
tff(c_1264,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1224,c_1263]) ).
tff(c_1266,plain,
n6,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_1293,plain,
( n10
| n9 ),
inference(demodulation,[status(thm),theory(equality)],[c_1214,c_1266,c_10]) ).
tff(c_1294,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1276,c_1114,c_1293]) ).
tff(c_1295,plain,
! [X6_10] : p(X6_10),
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_1320,plain,
n7,
inference(demodulation,[status(thm),theory(equality)],[c_1295,c_22]) ).
tff(c_1321,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1314,c_1320]) ).
tff(c_1322,plain,
n7,
inference(splitRight,[status(thm)],[c_1112]) ).
tff(c_1508,plain,
p(s7),
inference(demodulation,[status(thm),theory(equality)],[c_1322,c_24]) ).
tff(c_1548,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1546,c_1508]) ).
tff(c_1550,plain,
! [X_107] :
( p(X_107)
| ~ n1(X_107) ),
inference(splitRight,[status(thm)],[c_56]) ).
tff(c_1536,plain,
! [X_15] :
( ~ p(X_15)
| ~ n1(X_15) ),
inference(splitLeft,[status(thm)],[c_54]) ).
tff(c_1557,plain,
! [X_107] : ~ n1(X_107),
inference(resolution,[status(thm)],[c_1550,c_1536]) ).
tff(c_1330,plain,
! [X4_12] : ~ n1(X4_12),
inference(splitLeft,[status(thm)],[c_46]) ).
tff(c_1423,plain,
~ n2,
inference(negUnitSimplification,[status(thm)],[c_1330,c_48]) ).
tff(c_1327,plain,
~ n4,
inference(splitLeft,[status(thm)],[c_40]) ).
tff(c_1395,plain,
! [X5_11] : ~ q(X5_11),
inference(splitLeft,[status(thm)],[c_42]) ).
tff(c_1418,plain,
! [X10_1] : q(X10_1),
inference(demodulation,[status(thm),theory(equality)],[c_1113,c_20]) ).
tff(c_1419,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1395,c_1418]) ).
tff(c_1420,plain,
n3,
inference(splitRight,[status(thm)],[c_42]) ).
tff(c_1429,plain,
( ~ n9
| n4 ),
inference(demodulation,[status(thm),theory(equality)],[c_1420,c_62]) ).
tff(c_1430,plain,
~ n9,
inference(negUnitSimplification,[status(thm)],[c_1327,c_1429]) ).
tff(c_1332,plain,
~ n6,
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_1356,plain,
! [X8_3] : ~ n5(X8_3),
inference(negUnitSimplification,[status(thm)],[c_1332,c_26]) ).
tff(c_1352,plain,
! [X10_1] : q(X10_1),
inference(demodulation,[status(thm),theory(equality)],[c_1113,c_20]) ).
tff(c_1391,plain,
! [W_4] : n5(W_4),
inference(demodulation,[status(thm),theory(equality)],[c_1352,c_1352,c_30]) ).
tff(c_1392,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1356,c_1391]) ).
tff(c_1394,plain,
n6,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_1323,plain,
n10,
inference(splitRight,[status(thm)],[c_1112]) ).
tff(c_6,plain,
( ~ n10
| ~ n6
| n9
| n2 ),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_1451,plain,
( n9
| n2 ),
inference(demodulation,[status(thm),theory(equality)],[c_1394,c_1323,c_6]) ).
tff(c_1452,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1423,c_1430,c_1451]) ).
tff(c_1453,plain,
n2,
inference(splitRight,[status(thm)],[c_46]) ).
tff(c_1512,plain,
n1(s2),
inference(demodulation,[status(thm),theory(equality)],[c_1453,c_48]) ).
tff(c_1560,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1557,c_1512]) ).
tff(c_1561,plain,
! [X3_16] : p(X3_16),
inference(splitRight,[status(thm)],[c_54]) ).
tff(c_1324,plain,
~ p(s4),
inference(splitLeft,[status(thm)],[c_38]) ).
tff(c_1565,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1561,c_1324]) ).
tff(c_1566,plain,
! [X6_10] : p(X6_10),
inference(splitRight,[status(thm)],[c_40]) ).
tff(c_1570,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1566,c_1324]) ).
tff(c_1571,plain,
n4,
inference(splitRight,[status(thm)],[c_38]) ).
tff(c_1576,plain,
! [X6_10] : p(X6_10),
inference(demodulation,[status(thm),theory(equality)],[c_1571,c_40]) ).
tff(c_1664,plain,
! [X_13] : n1(X_13),
inference(demodulation,[status(thm),theory(equality)],[c_1576,c_1576,c_50]) ).
tff(c_1665,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1579,c_1664]) ).
tff(c_1666,plain,
n2,
inference(splitRight,[status(thm)],[c_46]) ).
tff(c_1669,plain,
! [X5_11] : ~ q(X5_11),
inference(splitLeft,[status(thm)],[c_42]) ).
tff(c_1685,plain,
! [X10_1] : q(X10_1),
inference(demodulation,[status(thm),theory(equality)],[c_1113,c_20]) ).
tff(c_1686,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1669,c_1685]) ).
tff(c_1687,plain,
n3,
inference(splitRight,[status(thm)],[c_42]) ).
tff(c_1689,plain,
n9,
inference(demodulation,[status(thm),theory(equality)],[c_1687,c_1571,c_58]) ).
tff(c_1690,plain,
~ n6,
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_1710,plain,
! [X8_3] : ~ n5(X8_3),
inference(negUnitSimplification,[status(thm)],[c_1690,c_26]) ).
tff(c_1700,plain,
! [X10_1] : q(X10_1),
inference(demodulation,[status(thm),theory(equality)],[c_1113,c_20]) ).
tff(c_1740,plain,
! [W_4] : n5(W_4),
inference(demodulation,[status(thm),theory(equality)],[c_1700,c_1700,c_30]) ).
tff(c_1741,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1710,c_1740]) ).
tff(c_1743,plain,
n6,
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_1771,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1666,c_1689,c_1743,c_1323,c_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYN037-1 : TPTP v9.0.0. Released v1.0.0.
% 0.07/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 : n013.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 : Wed Apr 9 06:52:17 EDT 2025
% 0.12/0.34 % CPUTime :
% 4.22/2.01 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.22/2.04
% 4.22/2.04 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------