%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : REL006-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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 : Thu Sep 24 02:03:12 PM UTC 2026
% Result : Unsatisfiable 0.23s 5.82s
% Output : CNFRefutation 0.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 13
% Syntax : Number of formulae : 133 ( 133 unt; 0 def)
% Number of atoms : 133 ( 132 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 167 ( 167 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B] : join(A,B) = join(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B,C] : join(A,join(B,C)) = join(join(A,B),C),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A,B] : A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A,B] : meet(A,B) = complement(join(complement(A),complement(B))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] : composition(A,one) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A] : converse(converse(A)) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A,B] : converse(join(A,B)) = join(converse(A),converse(B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [A,B] : converse(composition(A,B)) = composition(converse(B),converse(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [A,B] : join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [A] : top = join(A,complement(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A] : zero = meet(A,complement(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,negated_conjecture,
meet(converse(sk1),sk2) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,negated_conjecture,
meet(sk1,converse(sk2)) != zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f17,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f18,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f19,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f21,plain,
! [X0] : composition(X0,one) = X0,
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f23,plain,
! [X0] : converse(converse(X0)) = X0,
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f24,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f25,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f26,plain,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f27,plain,
! [X0] : top = join(X0,complement(X0)),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f28,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f29,plain,
meet(converse(sk1),sk2) = zero,
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f30,plain,
meet(sk1,converse(sk2)) != zero,
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f34,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))),
inference(forward_demodulation,[status(thm)],[f16,f18]) ).
fof(f35,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),X1)),meet(X0,X1)),
inference(backward_demodulation,[status(thm)],[f19,f34]) ).
fof(f36,plain,
! [X0,X1] : join(complement(X0),composition(converse(X1),complement(composition(X1,X0)))) = complement(X0),
inference(forward_demodulation,[status(thm)],[f16,f26]) ).
fof(f37,plain,
! [X0,X1] : X0 = join(meet(X0,X1),complement(join(complement(X0),X1))),
inference(forward_demodulation,[status(thm)],[f16,f35]) ).
fof(f39,plain,
! [X0,X1,X2] : meet(join(complement(X0),complement(X1)),X2) = complement(join(meet(X0,X1),complement(X2))),
inference(paramodulation,[status(thm)],[f19,f19]) ).
fof(f41,plain,
! [X0,X1] : zero = meet(join(complement(X0),complement(X1)),meet(X0,X1)),
inference(paramodulation,[status(thm)],[f19,f28]) ).
fof(f42,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(paramodulation,[status(thm)],[f23,f24]) ).
fof(f43,plain,
! [X0,X1] : converse(join(X0,converse(X1))) = join(converse(X0),X1),
inference(paramodulation,[status(thm)],[f23,f24]) ).
fof(f45,plain,
! [X0,X1] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(paramodulation,[status(thm)],[f23,f25]) ).
fof(f99,plain,
! [X0] : X0 = join(zero,complement(join(complement(X0),complement(X0)))),
inference(paramodulation,[status(thm)],[f28,f37]) ).
fof(f100,plain,
! [X0,X1] : X0 = join(meet(X0,complement(X1)),meet(X0,X1)),
inference(paramodulation,[status(thm)],[f19,f37]) ).
fof(f103,plain,
! [X0] : X0 = join(zero,meet(X0,X0)),
inference(forward_demodulation,[status(thm)],[f19,f99]) ).
fof(f104,plain,
! [X0,X1] : X0 = join(meet(X0,X1),meet(X0,complement(X1))),
inference(forward_demodulation,[status(thm)],[f16,f100]) ).
fof(f106,plain,
converse(sk1) = join(zero,meet(converse(sk1),complement(sk2))),
inference(paramodulation,[status(thm)],[f29,f104]) ).
fof(f107,plain,
! [X0] : X0 = join(zero,meet(X0,complement(complement(X0)))),
inference(paramodulation,[status(thm)],[f28,f104]) ).
fof(f204,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(paramodulation,[status(thm)],[f21,f45]) ).
fof(f206,plain,
! [X0] : X0 = composition(converse(one),X0),
inference(forward_demodulation,[status(thm)],[f23,f204]) ).
fof(f208,plain,
! [X0,X1] : top = join(join(complement(X0),complement(X1)),meet(X0,X1)),
inference(paramodulation,[status(thm)],[f19,f27]) ).
fof(f209,plain,
! [X0,X1] : meet(join(complement(X0),complement(X1)),meet(X0,X1)) = complement(top),
inference(paramodulation,[status(thm)],[f27,f39]) ).
fof(f215,plain,
! [X0,X1] : top = join(complement(X0),join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[status(thm)],[f17,f208]) ).
fof(f216,plain,
zero = complement(top),
inference(forward_demodulation,[status(thm)],[f41,f209]) ).
fof(f239,plain,
one = converse(one),
inference(paramodulation,[status(thm)],[f21,f206]) ).
fof(f245,plain,
! [X0] : join(complement(X0),composition(converse(converse(one)),complement(X0))) = complement(X0),
inference(paramodulation,[status(thm)],[f206,f36]) ).
fof(f246,plain,
! [X0] : X0 = composition(one,X0),
inference(backward_demodulation,[status(thm)],[f239,f206]) ).
fof(f249,plain,
! [X0] : join(complement(X0),composition(one,complement(X0))) = complement(X0),
inference(forward_demodulation,[status(thm)],[f23,f245]) ).
fof(f250,plain,
! [X0] : join(complement(X0),complement(X0)) = complement(X0),
inference(backward_demodulation,[status(thm)],[f246,f249]) ).
fof(f306,plain,
! [X0] : zero = meet(complement(X0),meet(X0,X0)),
inference(paramodulation,[status(thm)],[f250,f41]) ).
fof(f307,plain,
! [X0] : meet(X0,X0) = complement(complement(X0)),
inference(paramodulation,[status(thm)],[f250,f19]) ).
fof(f308,plain,
! [X0] : X0 = join(meet(X0,complement(X0)),complement(complement(X0))),
inference(paramodulation,[status(thm)],[f250,f37]) ).
fof(f325,plain,
! [X0] : X0 = join(complement(complement(X0)),meet(X0,complement(X0))),
inference(forward_demodulation,[status(thm)],[f16,f308]) ).
fof(f326,plain,
! [X0] : X0 = join(complement(complement(X0)),zero),
inference(forward_demodulation,[status(thm)],[f28,f325]) ).
fof(f327,plain,
! [X0] : X0 = join(zero,complement(complement(X0))),
inference(forward_demodulation,[status(thm)],[f16,f326]) ).
fof(f330,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(zero,complement(meet(X0,X1))),
inference(paramodulation,[status(thm)],[f19,f327]) ).
fof(f342,plain,
! [X0] : X0 = join(zero,meet(X0,meet(X0,X0))),
inference(paramodulation,[status(thm)],[f307,f107]) ).
fof(f345,plain,
! [X0] : join(meet(X0,X0),complement(complement(X0))) = complement(complement(X0)),
inference(paramodulation,[status(thm)],[f307,f250]) ).
fof(f452,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X1),complement(X0))),
inference(paramodulation,[status(thm)],[f16,f19]) ).
fof(f474,plain,
converse(sk1) = join(zero,meet(complement(sk2),converse(sk1))),
inference(backward_demodulation,[status(thm)],[f481,f106]) ).
fof(f481,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
inference(forward_demodulation,[status(thm)],[f19,f452]) ).
fof(f491,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(paramodulation,[status(thm)],[f16,f17]) ).
fof(f649,plain,
! [X0,X1] : X0 = join(meet(X0,X1),meet(complement(X1),X0)),
inference(paramodulation,[status(thm)],[f481,f104]) ).
fof(f651,plain,
! [X0,X1] : X0 = join(meet(X1,X0),meet(X0,complement(X1))),
inference(paramodulation,[status(thm)],[f481,f104]) ).
fof(f852,plain,
! [X0] : meet(X0,X0) = join(meet(meet(X0,X0),X0),zero),
inference(paramodulation,[status(thm)],[f306,f649]) ).
fof(f853,plain,
! [X0] : complement(complement(X0)) = join(meet(complement(complement(X0)),X0),zero),
inference(paramodulation,[status(thm)],[f28,f649]) ).
fof(f874,plain,
! [X0] : meet(X0,X0) = join(zero,meet(meet(X0,X0),X0)),
inference(forward_demodulation,[status(thm)],[f16,f852]) ).
fof(f875,plain,
! [X0] : meet(X0,X0) = join(zero,meet(X0,meet(X0,X0))),
inference(forward_demodulation,[status(thm)],[f481,f874]) ).
fof(f881,plain,
! [X0] : X0 = join(zero,X0),
inference(backward_demodulation,[status(thm)],[f899,f103]) ).
fof(f897,plain,
! [X0] : join(X0,complement(complement(X0))) = complement(complement(X0)),
inference(backward_demodulation,[status(thm)],[f899,f345]) ).
fof(f899,plain,
! [X0] : meet(X0,X0) = X0,
inference(forward_demodulation,[status(thm)],[f342,f875]) ).
fof(f900,plain,
! [X0] : complement(complement(X0)) = join(zero,meet(complement(complement(X0)),X0)),
inference(forward_demodulation,[status(thm)],[f16,f853]) ).
fof(f901,plain,
! [X0] : complement(complement(X0)) = join(zero,meet(X0,complement(complement(X0)))),
inference(forward_demodulation,[status(thm)],[f481,f900]) ).
fof(f908,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f107,f901]) ).
fof(f920,plain,
converse(sk1) = meet(complement(sk2),converse(sk1)),
inference(backward_demodulation,[status(thm)],[f881,f474]) ).
fof(f931,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = complement(meet(X0,X1)),
inference(backward_demodulation,[status(thm)],[f881,f330]) ).
fof(f948,plain,
! [X0] : join(X0,X0) = complement(complement(X0)),
inference(forward_demodulation,[status(thm)],[f908,f897]) ).
fof(f952,plain,
! [X0] : join(X0,X0) = X0,
inference(forward_demodulation,[status(thm)],[f908,f948]) ).
fof(f1025,plain,
! [X0,X1] : join(X0,join(X0,X1)) = join(X0,X1),
inference(paramodulation,[status(thm)],[f952,f17]) ).
fof(f1370,plain,
! [X0,X1] : join(meet(X0,X1),X0) = join(meet(X0,X1),meet(complement(X1),X0)),
inference(paramodulation,[status(thm)],[f649,f1025]) ).
fof(f1371,plain,
! [X0,X1] : join(meet(X0,X1),X1) = join(meet(X0,X1),meet(X1,complement(X0))),
inference(paramodulation,[status(thm)],[f651,f1025]) ).
fof(f1379,plain,
! [X0] : join(X0,top) = join(X0,complement(X0)),
inference(paramodulation,[status(thm)],[f27,f1025]) ).
fof(f1396,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = join(meet(X0,X1),meet(complement(X1),X0)),
inference(forward_demodulation,[status(thm)],[f16,f1370]) ).
fof(f1402,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
inference(forward_demodulation,[status(thm)],[f649,f1396]) ).
fof(f1403,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = join(meet(X1,X0),meet(X0,complement(X1))),
inference(forward_demodulation,[status(thm)],[f16,f1371]) ).
fof(f1405,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = X0,
inference(forward_demodulation,[status(thm)],[f651,f1403]) ).
fof(f1415,plain,
! [X0] : join(X0,top) = top,
inference(forward_demodulation,[status(thm)],[f27,f1379]) ).
fof(f1427,plain,
! [X0] : join(top,X0) = top,
inference(paramodulation,[status(thm)],[f16,f1415]) ).
fof(f1431,plain,
! [X0] : converse(top) = join(X0,converse(top)),
inference(paramodulation,[status(thm)],[f1415,f42]) ).
fof(f1607,plain,
! [X0,X1] : top = join(X0,join(complement(X1),meet(complement(X0),X1))),
inference(paramodulation,[status(thm)],[f908,f215]) ).
fof(f1624,plain,
! [X0,X1] : X0 = join(meet(X0,join(complement(X1),meet(X0,X1))),complement(top)),
inference(paramodulation,[status(thm)],[f215,f37]) ).
fof(f1665,plain,
! [X0,X1] : X0 = join(complement(top),meet(X0,join(complement(X1),meet(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f16,f1624]) ).
fof(f1666,plain,
! [X0,X1] : X0 = join(zero,meet(X0,join(complement(X1),meet(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f216,f1665]) ).
fof(f1667,plain,
! [X0,X1] : X0 = meet(X0,join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[status(thm)],[f881,f1666]) ).
fof(f1675,plain,
join(complement(sk2),converse(sk1)) = complement(sk2),
inference(paramodulation,[status(thm)],[f920,f1402]) ).
fof(f1691,plain,
converse(complement(sk2)) = join(converse(complement(sk2)),sk1),
inference(paramodulation,[status(thm)],[f1675,f43]) ).
fof(f1696,plain,
converse(complement(sk2)) = join(sk1,converse(complement(sk2))),
inference(forward_demodulation,[status(thm)],[f16,f1691]) ).
fof(f1771,plain,
! [X0,X1] : converse(converse(X0)) = join(X0,converse(meet(X1,converse(X0)))),
inference(paramodulation,[status(thm)],[f1405,f42]) ).
fof(f1778,plain,
! [X0,X1] : X0 = join(X0,converse(meet(X1,converse(X0)))),
inference(forward_demodulation,[status(thm)],[f23,f1771]) ).
fof(f1782,plain,
converse(top) = top,
inference(paramodulation,[status(thm)],[f1427,f1431]) ).
fof(f2538,plain,
! [X0,X1] : join(join(complement(X0),meet(X1,X0)),X1) = join(complement(X0),meet(X1,X0)),
inference(paramodulation,[status(thm)],[f1667,f1405]) ).
fof(f2573,plain,
! [X0,X1] : join(complement(X0),join(meet(X1,X0),X1)) = join(complement(X0),meet(X1,X0)),
inference(forward_demodulation,[status(thm)],[f17,f2538]) ).
fof(f2574,plain,
! [X0,X1] : join(complement(X0),join(X1,meet(X1,X0))) = join(complement(X0),meet(X1,X0)),
inference(forward_demodulation,[status(thm)],[f16,f2573]) ).
fof(f2575,plain,
! [X0,X1] : X0 = meet(X0,join(complement(X1),X0)),
inference(backward_demodulation,[status(thm)],[f2582,f1667]) ).
fof(f2576,plain,
! [X0,X1] : top = join(complement(X0),join(complement(X1),X0)),
inference(backward_demodulation,[status(thm)],[f2582,f215]) ).
fof(f2579,plain,
! [X0,X1] : top = join(X0,join(complement(X1),complement(X0))),
inference(backward_demodulation,[status(thm)],[f2582,f1607]) ).
fof(f2582,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),meet(X1,X0)),
inference(forward_demodulation,[status(thm)],[f1402,f2574]) ).
fof(f2589,plain,
! [X0,X1] : top = join(X0,join(complement(X0),complement(X1))),
inference(forward_demodulation,[status(thm)],[f491,f2576]) ).
fof(f2590,plain,
! [X0,X1] : top = join(X0,complement(meet(X0,X1))),
inference(forward_demodulation,[status(thm)],[f931,f2589]) ).
fof(f2595,plain,
! [X0,X1] : top = join(X0,complement(meet(X1,X0))),
inference(forward_demodulation,[status(thm)],[f931,f2579]) ).
fof(f2819,plain,
! [X0,X1] : X0 = meet(X0,join(X1,X0)),
inference(paramodulation,[status(thm)],[f908,f2575]) ).
fof(f2916,plain,
! [X0,X1] : X0 = meet(X0,join(X0,X1)),
inference(paramodulation,[status(thm)],[f16,f2819]) ).
fof(f2984,plain,
sk1 = meet(sk1,converse(complement(sk2))),
inference(paramodulation,[status(thm)],[f1696,f2916]) ).
fof(f3185,plain,
top = join(converse(complement(sk2)),complement(sk1)),
inference(paramodulation,[status(thm)],[f2984,f2595]) ).
fof(f3196,plain,
top = join(complement(sk1),converse(complement(sk2))),
inference(forward_demodulation,[status(thm)],[f16,f3185]) ).
fof(f4257,plain,
converse(top) = join(converse(complement(sk1)),complement(sk2)),
inference(paramodulation,[status(thm)],[f3196,f43]) ).
fof(f4270,plain,
top = join(converse(complement(sk1)),complement(sk2)),
inference(forward_demodulation,[status(thm)],[f1782,f4257]) ).
fof(f4271,plain,
top = join(complement(sk2),converse(complement(sk1))),
inference(forward_demodulation,[status(thm)],[f16,f4270]) ).
fof(f4284,plain,
sk2 = join(meet(sk2,converse(complement(sk1))),complement(top)),
inference(paramodulation,[status(thm)],[f4271,f37]) ).
fof(f4295,plain,
sk2 = join(complement(top),meet(sk2,converse(complement(sk1)))),
inference(forward_demodulation,[status(thm)],[f16,f4284]) ).
fof(f4296,plain,
sk2 = join(zero,meet(sk2,converse(complement(sk1)))),
inference(forward_demodulation,[status(thm)],[f216,f4295]) ).
fof(f4297,plain,
sk2 = meet(sk2,converse(complement(sk1))),
inference(forward_demodulation,[status(thm)],[f881,f4296]) ).
fof(f4310,plain,
complement(sk1) = join(complement(sk1),converse(sk2)),
inference(paramodulation,[status(thm)],[f4297,f1778]) ).
fof(f4336,plain,
converse(sk2) = meet(converse(sk2),complement(sk1)),
inference(paramodulation,[status(thm)],[f4310,f2819]) ).
fof(f4345,plain,
converse(sk2) = meet(complement(sk1),converse(sk2)),
inference(forward_demodulation,[status(thm)],[f481,f4336]) ).
fof(f4356,plain,
top = join(complement(sk1),complement(converse(sk2))),
inference(paramodulation,[status(thm)],[f4345,f2590]) ).
fof(f4370,plain,
top = complement(meet(sk1,converse(sk2))),
inference(forward_demodulation,[status(thm)],[f931,f4356]) ).
fof(f4435,plain,
complement(top) = meet(sk1,converse(sk2)),
inference(paramodulation,[status(thm)],[f4370,f908]) ).
fof(f4462,plain,
zero = meet(sk1,converse(sk2)),
inference(forward_demodulation,[status(thm)],[f216,f4435]) ).
fof(f4463,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f4462,f30]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : REL006-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/5.45 % Computer : n020.cluster.edu
% 0.18/5.45 % Model : x86_64 x86_64
% 0.18/5.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/5.45 % Memory : 8046.5625MB
% 0.18/5.45 % OS : Linux 6.8.0-71-generic
% 0.18/5.45 % CPULimit : 300
% 0.18/5.45 % WCLimit : 300
% 0.18/5.45 % DateTime : Mon Sep 21 03:58:53 UTC 2026
% 0.18/5.46 % CPUTime :
% 0.18/5.46 % Drodi V4.1.1
% 0.23/5.82 % Refutation found
% 0.23/5.82 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.23/5.82 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.23/5.85 % Elapsed time: 0.392712 seconds
% 0.23/5.85 % CPU time: 2.573801 seconds
% 0.23/5.85 % Total memory used: 48.885 MB
% 0.23/5.85 % Net memory used: 47.566 MB
%------------------------------------------------------------------------------