%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : LCL192-1 : TPTP v9.3.1. Released v1.1.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 : n014.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:27 AM UTC 2026
% Result : Unsatisfiable 92.34s 74.57s
% Output : CNFRefutation 92.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 9
% Syntax : Number of formulae : 43 ( 23 unt; 0 typ; 0 def)
% Number of atoms : 73 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 63 ( 33 ~; 30 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Maximal term depth : 6 ( 2 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-1 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 104 ( 104 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ theorem > axiom > or > #nlpp > not > r > q > p
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(r,type,
r: $i ).
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(f_58,axiom,
! [A,B] : axiom(or(not(or(A,B)),or(B,A))),
file(unknown,unknown) ).
tff(f_56,axiom,
! [A,B] : axiom(or(not(A),or(B,A))),
file(unknown,unknown) ).
tff(f_60,axiom,
! [A,B,C] : axiom(or(not(or(A,or(B,C))),or(B,or(A,C)))),
file(unknown,unknown) ).
tff(f_67,axiom,
! [X] :
( theorem(X)
| ~ axiom(X) ),
file(unknown,unknown) ).
tff(f_83,axiom,
! [X,Z,Y] :
( theorem(or(not(X),Z))
| ~ axiom(or(not(X),Y))
| ~ theorem(or(not(Y),Z)) ),
file(unknown,unknown) ).
tff(f_75,axiom,
! [X,Y] :
( theorem(X)
| ~ axiom(or(not(Y),X))
| ~ theorem(Y) ),
file(unknown,unknown) ).
tff(f_54,axiom,
! [A] : axiom(or(not(or(A,A)),A)),
file(unknown,unknown) ).
tff(f_62,axiom,
! [A,B,C] : axiom(or(not(or(not(A),B)),or(not(or(C,A)),or(C,B)))),
file(unknown,unknown) ).
tff(f_87,axiom,
~ theorem(or(not(or(or(p,q),r)),or(p,or(q,r)))),
file(unknown,unknown) ).
tff(c_6,plain,
! [A_4,B_5] : axiom(or(not(or(A_4,B_5)),or(B_5,A_4))),
inference(cnfTransformation,[status(thm)],[f_58]) ).
tff(c_4,plain,
! [A_2,B_3] : axiom(or(not(A_2),or(B_3,A_2))),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_8,plain,
! [A_6,B_7,C_8] : axiom(or(not(or(A_6,or(B_7,C_8))),or(B_7,or(A_6,C_8)))),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_12,plain,
! [X_12] :
( ~ axiom(X_12)
| theorem(X_12) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_118,plain,
! [Y_37,Z_38,X_39] :
( ~ theorem(or(not(Y_37),Z_38))
| ~ axiom(or(not(X_39),Y_37))
| theorem(or(not(X_39),Z_38)) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_482,plain,
! [X_84,Y_85,Z_86] :
( ~ axiom(or(not(X_84),Y_85))
| theorem(or(not(X_84),Z_86))
| ~ axiom(or(not(Y_85),Z_86)) ),
inference(resolution,[status(thm)],[c_12,c_118]) ).
tff(c_1015,plain,
! [A_167,B_168,C_169,Z_170] :
( theorem(or(not(or(A_167,or(B_168,C_169))),Z_170))
| ~ axiom(or(not(or(B_168,or(A_167,C_169))),Z_170)) ),
inference(resolution,[status(thm)],[c_8,c_482]) ).
tff(c_16,plain,
! [Y_17,Z_16,X_15] :
( ~ theorem(or(not(Y_17),Z_16))
| ~ axiom(or(not(X_15),Y_17))
| theorem(or(not(X_15),Z_16)) ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_7233,plain,
! [B_884,A_883,C_881,Z_882,X_885] :
( ~ axiom(or(not(X_885),or(A_883,or(B_884,C_881))))
| theorem(or(not(X_885),Z_882))
| ~ axiom(or(not(or(B_884,or(A_883,C_881))),Z_882)) ),
inference(resolution,[status(thm)],[c_1015,c_16]) ).
tff(c_13050,plain,
! [B_1389,C_1390,Z_1391,B_1392] :
( theorem(or(not(or(B_1389,C_1390)),Z_1391))
| ~ axiom(or(not(or(B_1389,or(B_1392,C_1390))),Z_1391)) ),
inference(resolution,[status(thm)],[c_4,c_7233]) ).
tff(c_13078,plain,
! [A_1393,C_1394,B_1395] : theorem(or(not(or(A_1393,C_1394)),or(or(B_1395,C_1394),A_1393))),
inference(resolution,[status(thm)],[c_6,c_13050]) ).
tff(c_105,plain,
! [A_34,B_35,C_36] : axiom(or(not(or(A_34,or(B_35,C_36))),or(B_35,or(A_34,C_36)))),
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_14,plain,
! [Y_14,X_13] :
( ~ theorem(Y_14)
| ~ axiom(or(not(Y_14),X_13))
| theorem(X_13) ),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_109,plain,
! [A_34,B_35,C_36] :
( ~ theorem(or(A_34,or(B_35,C_36)))
| theorem(or(B_35,or(A_34,C_36))) ),
inference(resolution,[status(thm)],[c_105,c_14]) ).
tff(c_13092,plain,
! [B_1396,C_1397,A_1398] : theorem(or(or(B_1396,C_1397),or(not(or(A_1398,C_1397)),A_1398))),
inference(resolution,[status(thm)],[c_13078,c_109]) ).
tff(c_36,plain,
! [A_25,B_26] : axiom(or(not(or(A_25,B_26)),or(B_26,A_25))),
inference(cnfTransformation,[status(thm)],[f_58]) ).
tff(c_40,plain,
! [A_25,B_26] :
( ~ theorem(or(A_25,B_26))
| theorem(or(B_26,A_25)) ),
inference(resolution,[status(thm)],[c_36,c_14]) ).
tff(c_13149,plain,
! [A_1405,C_1406,B_1407] : theorem(or(or(not(or(A_1405,C_1406)),A_1405),or(B_1407,C_1406))),
inference(resolution,[status(thm)],[c_13092,c_40]) ).
tff(c_13189,plain,
! [B_1408,A_1409,C_1410] : theorem(or(B_1408,or(or(not(or(A_1409,C_1410)),A_1409),C_1410))),
inference(resolution,[status(thm)],[c_13149,c_109]) ).
tff(c_2,plain,
! [A_1] : axiom(or(not(or(A_1,A_1)),A_1)),
inference(cnfTransformation,[status(thm)],[f_54]) ).
tff(c_22,plain,
! [Y_22,X_23] :
( ~ theorem(Y_22)
| ~ axiom(or(not(Y_22),X_23))
| theorem(X_23) ),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_29,plain,
! [A_1] :
( ~ theorem(or(A_1,A_1))
| theorem(A_1) ),
inference(resolution,[status(thm)],[c_2,c_22]) ).
tff(c_13240,plain,
! [A_1411,C_1412] : theorem(or(or(not(or(A_1411,C_1412)),A_1411),C_1412)),
inference(resolution,[status(thm)],[c_13189,c_29]) ).
tff(c_13265,plain,
! [C_1413,A_1414] : theorem(or(C_1413,or(not(or(A_1414,C_1413)),A_1414))),
inference(resolution,[status(thm)],[c_13240,c_40]) ).
tff(c_13282,plain,
! [A_1414,C_1413] : theorem(or(not(or(A_1414,C_1413)),or(C_1413,A_1414))),
inference(resolution,[status(thm)],[c_13265,c_109]) ).
tff(c_135,plain,
! [A_40,B_41,C_42] : axiom(or(not(or(not(A_40),B_41)),or(not(or(C_42,A_40)),or(C_42,B_41)))),
inference(cnfTransformation,[status(thm)],[f_62]) ).
tff(c_373,plain,
! [A_74,B_75,C_76] :
( ~ theorem(or(not(A_74),B_75))
| theorem(or(not(or(C_76,A_74)),or(C_76,B_75))) ),
inference(resolution,[status(thm)],[c_135,c_14]) ).
tff(c_1152,plain,
! [X_191,C_192,A_193,B_194] :
( ~ axiom(or(not(X_191),or(C_192,A_193)))
| theorem(or(not(X_191),or(C_192,B_194)))
| ~ theorem(or(not(A_193),B_194)) ),
inference(resolution,[status(thm)],[c_373,c_16]) ).
tff(c_5333,plain,
! [A_640,B_641,C_642,B_643] :
( theorem(or(not(or(A_640,or(B_641,C_642))),or(B_641,B_643)))
| ~ theorem(or(not(or(A_640,C_642)),B_643)) ),
inference(resolution,[status(thm)],[c_8,c_1152]) ).
tff(c_23334,plain,
! [X_2417,C_2414,A_2413,B_2415,B_2416] :
( ~ axiom(or(not(X_2417),or(A_2413,or(B_2415,C_2414))))
| theorem(or(not(X_2417),or(B_2415,B_2416)))
| ~ theorem(or(not(or(A_2413,C_2414)),B_2416)) ),
inference(resolution,[status(thm)],[c_5333,c_16]) ).
tff(c_79782,plain,
! [B_5245,C_5246,B_5247,B_5248] :
( theorem(or(not(or(or(B_5245,C_5246),B_5247)),or(B_5245,B_5248)))
| ~ theorem(or(not(or(B_5247,C_5246)),B_5248)) ),
inference(resolution,[status(thm)],[c_6,c_23334]) ).
tff(c_18,plain,
~ theorem(or(not(or(or(p,q),r)),or(p,or(q,r)))),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_79806,plain,
~ theorem(or(not(or(r,q)),or(q,r))),
inference(resolution,[status(thm)],[c_79782,c_18]) ).
tff(c_79821,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_13282,c_79806]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL192-1 : TPTP v9.3.1. Released v1.1.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.10/0.35 % Computer : n014.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 5 03:34:42 UTC 2026
% 0.10/0.36 % CPUTime :
% 92.34/74.57 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 92.34/74.58
% 92.34/74.58 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------