%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : LCL209-3 : TPTP v9.3.1. Released v2.3.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 : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 11:11:31 AM UTC 2026
% Result : Unsatisfiable 22.33s 8.15s
% Output : CNFRefutation 22.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 9
% Syntax : Number of formulae : 81 ( 39 unt; 0 typ; 0 def)
% Number of atoms : 136 ( 3 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 113 ( 58 ~; 55 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 180 ( 180 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ theorem > axiom > or > implies > #nlpp > not > q > p
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(theorem,type,
theorem: $i > $o ).
tff(or,type,
or: ( $i * $i ) > $i ).
tff(not,type,
not: $i > $i ).
tff(q,type,
q: $i ).
tff(axiom,type,
axiom: $i > $o ).
tff(p,type,
p: $i ).
tff(implies,type,
implies: ( $i * $i ) > $i ).
tff(f_48,axiom,
! [A,B] : axiom(implies(A,or(B,A))),
file(unknown,unknown) ).
tff(f_61,axiom,
! [X] :
( theorem(X)
| ~ axiom(X) ),
file(unknown,unknown) ).
tff(f_56,axiom,
! [X,Y] : ( implies(X,Y) = or(not(X),Y) ),
file(unknown,unknown) ).
tff(f_52,axiom,
! [A,B,C] : axiom(implies(or(A,or(B,C)),or(B,or(A,C)))),
file(unknown,unknown) ).
tff(f_69,axiom,
! [X,Y] :
( theorem(X)
| ~ theorem(implies(Y,X))
| ~ theorem(Y) ),
file(unknown,unknown) ).
tff(f_50,axiom,
! [A,B] : axiom(implies(or(A,B),or(B,A))),
file(unknown,unknown) ).
tff(f_46,axiom,
! [A] : axiom(implies(or(A,A),A)),
file(unknown,unknown) ).
tff(f_54,axiom,
! [A,B,C] : axiom(implies(implies(A,B),implies(or(C,A),or(C,B)))),
file(unknown,unknown) ).
tff(f_77,axiom,
~ theorem(implies(implies(not(p),q),or(p,q))),
file(unknown,unknown) ).
tff(c_4,plain,
! [A_2,B_3] : axiom(implies(A_2,or(B_3,A_2))),
inference(cnfTransformation,[status(thm)],[f_48]) ).
tff(c_14,plain,
! [X_14] :
( ~ axiom(X_14)
| theorem(X_14) ),
inference(cnfTransformation,[status(thm)],[f_61]) ).
tff(c_12,plain,
! [X_12,Y_13] : ( or(not(X_12),Y_13) = implies(X_12,Y_13) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_102,plain,
! [A_36,B_37,C_38] : axiom(implies(or(A_36,or(B_37,C_38)),or(B_37,or(A_36,C_38)))),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_115,plain,
! [X_12,B_37,Y_13] : axiom(implies(or(not(X_12),or(B_37,Y_13)),or(B_37,implies(X_12,Y_13)))),
inference(superposition,[status(thm),theory(equality)],[c_12,c_102]) ).
tff(c_358,plain,
! [X_78,B_79,Y_80] : axiom(implies(implies(X_78,or(B_79,Y_80)),or(B_79,implies(X_78,Y_80)))),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_115]) ).
tff(c_39,plain,
! [Y_25,X_26] :
( ~ theorem(Y_25)
| ~ theorem(implies(Y_25,X_26))
| theorem(X_26) ),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_43,plain,
! [Y_25,X_26] :
( ~ theorem(Y_25)
| theorem(X_26)
| ~ axiom(implies(Y_25,X_26)) ),
inference(resolution,[status(thm)],[c_14,c_39]) ).
tff(c_562,plain,
! [X_116,B_117,Y_118] :
( ~ theorem(implies(X_116,or(B_117,Y_118)))
| theorem(or(B_117,implies(X_116,Y_118))) ),
inference(resolution,[status(thm)],[c_358,c_43]) ).
tff(c_6,plain,
! [A_4,B_5] : axiom(implies(or(A_4,B_5),or(B_5,A_4))),
inference(cnfTransformation,[status(thm)],[f_50]) ).
tff(c_52,plain,
! [Y_30,X_31] :
( ~ theorem(Y_30)
| theorem(X_31)
| ~ axiom(implies(Y_30,X_31)) ),
inference(resolution,[status(thm)],[c_14,c_39]) ).
tff(c_69,plain,
! [A_4,B_5] :
( ~ theorem(or(A_4,B_5))
| theorem(or(B_5,A_4)) ),
inference(resolution,[status(thm)],[c_6,c_52]) ).
tff(c_1566,plain,
! [X_216,Y_217,B_218] :
( theorem(or(implies(X_216,Y_217),B_218))
| ~ theorem(implies(X_216,or(B_218,Y_217))) ),
inference(resolution,[status(thm)],[c_562,c_69]) ).
tff(c_72,plain,
! [A_2,B_3] :
( ~ theorem(A_2)
| theorem(or(B_3,A_2)) ),
inference(resolution,[status(thm)],[c_4,c_52]) ).
tff(c_459,plain,
! [A_98,B_99,C_100] :
( ~ theorem(or(A_98,or(B_99,C_100)))
| theorem(or(B_99,or(A_98,C_100))) ),
inference(resolution,[status(thm)],[c_102,c_43]) ).
tff(c_603,plain,
! [B_122,B_123,C_124] :
( theorem(or(B_122,or(B_123,C_124)))
| ~ theorem(or(B_122,C_124)) ),
inference(resolution,[status(thm)],[c_72,c_459]) ).
tff(c_623,plain,
! [B_125,X_126,Y_127] :
( theorem(or(B_125,implies(X_126,Y_127)))
| ~ theorem(or(B_125,Y_127)) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_603]) ).
tff(c_2,plain,
! [A_1] : axiom(implies(or(A_1,A_1),A_1)),
inference(cnfTransformation,[status(thm)],[f_46]) ).
tff(c_71,plain,
! [A_1] :
( ~ theorem(or(A_1,A_1))
| theorem(A_1) ),
inference(resolution,[status(thm)],[c_2,c_52]) ).
tff(c_639,plain,
! [X_126,Y_127] :
( theorem(implies(X_126,Y_127))
| ~ theorem(or(implies(X_126,Y_127),Y_127)) ),
inference(resolution,[status(thm)],[c_623,c_71]) ).
tff(c_1606,plain,
! [X_219,B_220] :
( theorem(implies(X_219,B_220))
| ~ theorem(implies(X_219,or(B_220,B_220))) ),
inference(resolution,[status(thm)],[c_1566,c_639]) ).
tff(c_1736,plain,
! [X_227,B_228] :
( theorem(implies(X_227,B_228))
| ~ axiom(implies(X_227,or(B_228,B_228))) ),
inference(resolution,[status(thm)],[c_14,c_1606]) ).
tff(c_1770,plain,
! [A_2] : theorem(implies(A_2,A_2)),
inference(resolution,[status(thm)],[c_4,c_1736]) ).
tff(c_108,plain,
! [A_36,X_12,Y_13] : axiom(implies(or(A_36,implies(X_12,Y_13)),or(not(X_12),or(A_36,Y_13)))),
inference(superposition,[status(thm),theory(equality)],[c_12,c_102]) ).
tff(c_407,plain,
! [A_86,X_87,Y_88] : axiom(implies(or(A_86,implies(X_87,Y_88)),implies(X_87,or(A_86,Y_88)))),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_108]) ).
tff(c_434,plain,
! [A_95,X_96,Y_97] :
( ~ theorem(or(A_95,implies(X_96,Y_97)))
| theorem(implies(X_96,or(A_95,Y_97))) ),
inference(resolution,[status(thm)],[c_407,c_43]) ).
tff(c_450,plain,
! [X_12,X_96,Y_97] :
( ~ theorem(implies(X_12,implies(X_96,Y_97)))
| theorem(implies(X_96,or(not(X_12),Y_97))) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_434]) ).
tff(c_1989,plain,
! [X_242,X_243,Y_244] :
( ~ theorem(implies(X_242,implies(X_243,Y_244)))
| theorem(implies(X_243,implies(X_242,Y_244))) ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_450]) ).
tff(c_2018,plain,
! [X_243,Y_244] : theorem(implies(X_243,implies(implies(X_243,Y_244),Y_244))),
inference(resolution,[status(thm)],[c_1770,c_1989]) ).
tff(c_44,plain,
! [A_27,B_28] : axiom(implies(or(A_27,B_28),or(B_28,A_27))),
inference(cnfTransformation,[status(thm)],[f_50]) ).
tff(c_47,plain,
! [X_12,Y_13] : axiom(implies(implies(X_12,Y_13),or(Y_13,not(X_12)))),
inference(superposition,[status(thm),theory(equality)],[c_12,c_44]) ).
tff(c_22,plain,
! [X_21,Y_22] : ( or(not(X_21),Y_22) = implies(X_21,Y_22) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_32,plain,
! [Y_22,X_21] : axiom(implies(Y_22,implies(X_21,Y_22))),
inference(superposition,[status(thm),theory(equality)],[c_22,c_4]) ).
tff(c_139,plain,
! [A_40,B_41,C_42] : axiom(implies(implies(A_40,B_41),implies(or(C_42,A_40),or(C_42,B_41)))),
inference(cnfTransformation,[status(thm)],[f_54]) ).
tff(c_148,plain,
! [A_40,Y_13,X_12] : axiom(implies(implies(A_40,Y_13),implies(or(not(X_12),A_40),implies(X_12,Y_13)))),
inference(superposition,[status(thm),theory(equality)],[c_12,c_139]) ).
tff(c_305,plain,
! [A_66,Y_67,X_68] : axiom(implies(implies(A_66,Y_67),implies(implies(X_68,A_66),implies(X_68,Y_67)))),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_148]) ).
tff(c_429,plain,
! [A_92,Y_93,X_94] :
( ~ theorem(implies(A_92,Y_93))
| theorem(implies(implies(X_94,A_92),implies(X_94,Y_93))) ),
inference(resolution,[status(thm)],[c_305,c_43]) ).
tff(c_16,plain,
! [Y_16,X_15] :
( ~ theorem(Y_16)
| ~ theorem(implies(Y_16,X_15))
| theorem(X_15) ),
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_2295,plain,
! [X_263,A_264,Y_265] :
( ~ theorem(implies(X_263,A_264))
| theorem(implies(X_263,Y_265))
| ~ theorem(implies(A_264,Y_265)) ),
inference(resolution,[status(thm)],[c_429,c_16]) ).
tff(c_6295,plain,
! [X_501,Y_502,A_503] :
( theorem(implies(X_501,Y_502))
| ~ theorem(implies(A_503,Y_502))
| ~ axiom(implies(X_501,A_503)) ),
inference(resolution,[status(thm)],[c_14,c_2295]) ).
tff(c_17969,plain,
! [X_900,Y_901,A_902] :
( theorem(implies(X_900,Y_901))
| ~ axiom(implies(X_900,A_902))
| ~ axiom(implies(A_902,Y_901)) ),
inference(resolution,[status(thm)],[c_14,c_6295]) ).
tff(c_18012,plain,
! [Y_903,Y_904,X_905] :
( theorem(implies(Y_903,Y_904))
| ~ axiom(implies(implies(X_905,Y_903),Y_904)) ),
inference(resolution,[status(thm)],[c_32,c_17969]) ).
tff(c_18243,plain,
! [Y_910,B_911,X_912] : theorem(implies(Y_910,or(B_911,implies(X_912,Y_910)))),
inference(resolution,[status(thm)],[c_4,c_18012]) ).
tff(c_578,plain,
! [X_116,Y_118] :
( theorem(implies(X_116,Y_118))
| ~ theorem(implies(X_116,or(implies(X_116,Y_118),Y_118))) ),
inference(resolution,[status(thm)],[c_562,c_71]) ).
tff(c_18369,plain,
! [Y_913,X_914] : theorem(implies(Y_913,implies(X_914,Y_913))),
inference(resolution,[status(thm)],[c_18243,c_578]) ).
tff(c_457,plain,
! [X_12,X_96,Y_97] :
( ~ theorem(implies(X_12,implies(X_96,Y_97)))
| theorem(implies(X_96,implies(X_12,Y_97))) ),
inference(demodulation,[status(thm),theory(equality)],[c_12,c_450]) ).
tff(c_18477,plain,
! [X_915,Y_916] : theorem(implies(X_915,implies(Y_916,Y_916))),
inference(resolution,[status(thm)],[c_18369,c_457]) ).
tff(c_393,plain,
! [A_83,B_84,C_85] :
( ~ theorem(implies(A_83,B_84))
| theorem(implies(or(C_85,A_83),or(C_85,B_84))) ),
inference(resolution,[status(thm)],[c_139,c_43]) ).
tff(c_1272,plain,
! [C_183,A_184,B_185] :
( ~ theorem(or(C_183,A_184))
| theorem(or(C_183,B_185))
| ~ theorem(implies(A_184,B_185)) ),
inference(resolution,[status(thm)],[c_393,c_16]) ).
tff(c_1328,plain,
! [B_3,B_185,A_2] :
( theorem(or(B_3,B_185))
| ~ theorem(implies(A_2,B_185))
| ~ theorem(A_2) ),
inference(resolution,[status(thm)],[c_72,c_1272]) ).
tff(c_18598,plain,
! [B_3,Y_916,X_915] :
( theorem(or(B_3,implies(Y_916,Y_916)))
| ~ theorem(X_915) ),
inference(resolution,[status(thm)],[c_18477,c_1328]) ).
tff(c_19350,plain,
! [X_915] : ~ theorem(X_915),
inference(splitLeft,[status(thm)],[c_18598]) ).
tff(c_18599,plain,
! [Y_917,X_918,X_919] : theorem(implies(Y_917,implies(X_918,implies(X_919,Y_917)))),
inference(resolution,[status(thm)],[c_32,c_18012]) ).
tff(c_18703,plain,
! [X_918,Y_917,X_919] : theorem(implies(X_918,implies(Y_917,implies(X_919,Y_917)))),
inference(resolution,[status(thm)],[c_18599,c_457]) ).
tff(c_19653,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_19350,c_18703]) ).
tff(c_19655,plain,
! [B_931,Y_932] : theorem(or(B_931,implies(Y_932,Y_932))),
inference(splitRight,[status(thm)],[c_18598]) ).
tff(c_149,plain,
! [A_40,B_41,C_42] :
( ~ theorem(implies(A_40,B_41))
| theorem(implies(or(C_42,A_40),or(C_42,B_41))) ),
inference(resolution,[status(thm)],[c_139,c_43]) ).
tff(c_2185,plain,
! [B_254,A_255] :
( theorem(implies(or(B_254,A_255),B_254))
| ~ theorem(implies(A_255,B_254)) ),
inference(resolution,[status(thm)],[c_149,c_1606]) ).
tff(c_2026,plain,
! [X_245,Y_246] : theorem(implies(X_245,implies(implies(X_245,Y_246),Y_246))),
inference(resolution,[status(thm)],[c_1770,c_1989]) ).
tff(c_2042,plain,
! [X_247,Y_248] :
( ~ theorem(X_247)
| theorem(implies(implies(X_247,Y_248),Y_248)) ),
inference(resolution,[status(thm)],[c_2026,c_16]) ).
tff(c_2069,plain,
! [X_247,Y_248] :
( ~ theorem(implies(X_247,Y_248))
| theorem(Y_248)
| ~ theorem(X_247) ),
inference(resolution,[status(thm)],[c_2042,c_16]) ).
tff(c_2206,plain,
! [B_254,A_255] :
( theorem(B_254)
| ~ theorem(or(B_254,A_255))
| ~ theorem(implies(A_255,B_254)) ),
inference(resolution,[status(thm)],[c_2185,c_2069]) ).
tff(c_21655,plain,
! [B_988,Y_989] :
( theorem(B_988)
| ~ theorem(implies(implies(Y_989,Y_989),B_988)) ),
inference(resolution,[status(thm)],[c_19655,c_2206]) ).
tff(c_22199,plain,
! [B_996,Y_997] :
( theorem(B_996)
| ~ axiom(implies(implies(Y_997,Y_997),B_996)) ),
inference(resolution,[status(thm)],[c_14,c_21655]) ).
tff(c_22246,plain,
! [Y_998] : theorem(or(Y_998,not(Y_998))),
inference(resolution,[status(thm)],[c_47,c_22199]) ).
tff(c_403,plain,
! [C_85,A_83,B_84] :
( ~ theorem(or(C_85,A_83))
| theorem(or(C_85,B_84))
| ~ theorem(implies(A_83,B_84)) ),
inference(resolution,[status(thm)],[c_393,c_16]) ).
tff(c_26268,plain,
! [Y_1108,B_1109] :
( theorem(or(Y_1108,B_1109))
| ~ theorem(implies(not(Y_1108),B_1109)) ),
inference(resolution,[status(thm)],[c_22246,c_403]) ).
tff(c_32580,plain,
! [Y_1271,Y_1272] : theorem(or(Y_1271,implies(implies(not(Y_1271),Y_1272),Y_1272))),
inference(resolution,[status(thm)],[c_2018,c_26268]) ).
tff(c_418,plain,
! [A_86,X_87,Y_88] :
( ~ theorem(or(A_86,implies(X_87,Y_88)))
| theorem(implies(X_87,or(A_86,Y_88))) ),
inference(resolution,[status(thm)],[c_407,c_43]) ).
tff(c_32605,plain,
! [Y_1271,Y_1272] : theorem(implies(implies(not(Y_1271),Y_1272),or(Y_1271,Y_1272))),
inference(resolution,[status(thm)],[c_32580,c_418]) ).
tff(c_18,plain,
~ theorem(implies(implies(not(p),q),or(p,q))),
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_34058,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_32605,c_18]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL209-3 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.04 % 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.11/0.37 % Computer : n008.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Fri Sep 4 16:32:08 UTC 2026
% 0.11/0.37 % CPUTime :
% 22.33/8.15 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.43/8.16
% 22.43/8.16 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------