%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : REL007-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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 1.19s 0.54s
% Output : CNFRefutation 1.19s
% 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 : 3 ( 3 ~; 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/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B,C] : join(A,join(B,C)) = join(join(A,B),C),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A,B] : A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A,B] : meet(A,B) = complement(join(complement(A),complement(B))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [A] : composition(A,one) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A] : converse(converse(A)) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A,B] : converse(join(A,B)) = join(converse(A),converse(B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [A,B] : converse(composition(A,B)) = composition(converse(B),converse(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [A,B] : join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [A] : top = join(A,complement(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A] : zero = meet(A,complement(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,negated_conjecture,
meet(sk1,converse(sk2)) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,negated_conjecture,
meet(converse(sk1),sk2) != zero,
file('/export/starexec/sandbox/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(sk1,converse(sk2)) = zero,
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f30,plain,
meet(converse(sk1),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(f98,plain,
sk1 = join(zero,complement(join(complement(sk1),converse(sk2)))),
inference(paramodulation,[status(thm)],[f29,f37]) ).
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(f102,plain,
! [X0] : X0 = join(zero,meet(X0,X0)),
inference(forward_demodulation,[status(thm)],[f19,f99]) ).
fof(f103,plain,
! [X0,X1] : X0 = join(meet(X0,X1),meet(X0,complement(X1))),
inference(forward_demodulation,[status(thm)],[f16,f100]) ).
fof(f106,plain,
! [X0] : X0 = join(zero,meet(X0,complement(complement(X0)))),
inference(paramodulation,[status(thm)],[f28,f103]) ).
fof(f201,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(paramodulation,[status(thm)],[f21,f45]) ).
fof(f203,plain,
! [X0] : X0 = composition(converse(one),X0),
inference(forward_demodulation,[status(thm)],[f23,f201]) ).
fof(f205,plain,
! [X0,X1] : top = join(join(complement(X0),complement(X1)),meet(X0,X1)),
inference(paramodulation,[status(thm)],[f19,f27]) ).
fof(f206,plain,
! [X0,X1] : meet(join(complement(X0),complement(X1)),meet(X0,X1)) = complement(top),
inference(paramodulation,[status(thm)],[f27,f39]) ).
fof(f212,plain,
! [X0,X1] : top = join(complement(X0),join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[status(thm)],[f17,f205]) ).
fof(f213,plain,
zero = complement(top),
inference(forward_demodulation,[status(thm)],[f41,f206]) ).
fof(f236,plain,
one = converse(one),
inference(paramodulation,[status(thm)],[f21,f203]) ).
fof(f242,plain,
! [X0] : join(complement(X0),composition(converse(converse(one)),complement(X0))) = complement(X0),
inference(paramodulation,[status(thm)],[f203,f36]) ).
fof(f243,plain,
! [X0] : X0 = composition(one,X0),
inference(backward_demodulation,[status(thm)],[f236,f203]) ).
fof(f246,plain,
! [X0] : join(complement(X0),composition(one,complement(X0))) = complement(X0),
inference(forward_demodulation,[status(thm)],[f23,f242]) ).
fof(f247,plain,
! [X0] : join(complement(X0),complement(X0)) = complement(X0),
inference(backward_demodulation,[status(thm)],[f243,f246]) ).
fof(f303,plain,
! [X0] : zero = meet(complement(X0),meet(X0,X0)),
inference(paramodulation,[status(thm)],[f247,f41]) ).
fof(f304,plain,
! [X0] : meet(X0,X0) = complement(complement(X0)),
inference(paramodulation,[status(thm)],[f247,f19]) ).
fof(f305,plain,
! [X0] : X0 = join(meet(X0,complement(X0)),complement(complement(X0))),
inference(paramodulation,[status(thm)],[f247,f37]) ).
fof(f322,plain,
! [X0] : X0 = join(complement(complement(X0)),meet(X0,complement(X0))),
inference(forward_demodulation,[status(thm)],[f16,f305]) ).
fof(f323,plain,
! [X0] : X0 = join(complement(complement(X0)),zero),
inference(forward_demodulation,[status(thm)],[f28,f322]) ).
fof(f324,plain,
! [X0] : X0 = join(zero,complement(complement(X0))),
inference(forward_demodulation,[status(thm)],[f16,f323]) ).
fof(f327,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = join(zero,complement(meet(X0,X1))),
inference(paramodulation,[status(thm)],[f19,f324]) ).
fof(f339,plain,
! [X0] : X0 = join(zero,meet(X0,meet(X0,X0))),
inference(paramodulation,[status(thm)],[f304,f106]) ).
fof(f342,plain,
! [X0] : join(meet(X0,X0),complement(complement(X0))) = complement(complement(X0)),
inference(paramodulation,[status(thm)],[f304,f247]) ).
fof(f449,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X1),complement(X0))),
inference(paramodulation,[status(thm)],[f16,f19]) ).
fof(f469,plain,
meet(sk2,converse(sk1)) != zero,
inference(backward_demodulation,[status(thm)],[f477,f30]) ).
fof(f477,plain,
! [X0,X1] : meet(X0,X1) = meet(X1,X0),
inference(forward_demodulation,[status(thm)],[f19,f449]) ).
fof(f487,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(paramodulation,[status(thm)],[f16,f17]) ).
fof(f662,plain,
! [X0,X1] : X0 = join(meet(X0,X1),meet(complement(X1),X0)),
inference(paramodulation,[status(thm)],[f477,f103]) ).
fof(f664,plain,
! [X0,X1] : X0 = join(meet(X1,X0),meet(X0,complement(X1))),
inference(paramodulation,[status(thm)],[f477,f103]) ).
fof(f865,plain,
! [X0] : meet(X0,X0) = join(meet(meet(X0,X0),X0),zero),
inference(paramodulation,[status(thm)],[f303,f662]) ).
fof(f866,plain,
! [X0] : complement(complement(X0)) = join(meet(complement(complement(X0)),X0),zero),
inference(paramodulation,[status(thm)],[f28,f662]) ).
fof(f887,plain,
! [X0] : meet(X0,X0) = join(zero,meet(meet(X0,X0),X0)),
inference(forward_demodulation,[status(thm)],[f16,f865]) ).
fof(f888,plain,
! [X0] : meet(X0,X0) = join(zero,meet(X0,meet(X0,X0))),
inference(forward_demodulation,[status(thm)],[f477,f887]) ).
fof(f894,plain,
! [X0] : X0 = join(zero,X0),
inference(backward_demodulation,[status(thm)],[f912,f102]) ).
fof(f910,plain,
! [X0] : join(X0,complement(complement(X0))) = complement(complement(X0)),
inference(backward_demodulation,[status(thm)],[f912,f342]) ).
fof(f912,plain,
! [X0] : meet(X0,X0) = X0,
inference(forward_demodulation,[status(thm)],[f339,f888]) ).
fof(f913,plain,
! [X0] : complement(complement(X0)) = join(zero,meet(complement(complement(X0)),X0)),
inference(forward_demodulation,[status(thm)],[f16,f866]) ).
fof(f914,plain,
! [X0] : complement(complement(X0)) = join(zero,meet(X0,complement(complement(X0)))),
inference(forward_demodulation,[status(thm)],[f477,f913]) ).
fof(f922,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[status(thm)],[f106,f914]) ).
fof(f931,plain,
sk1 = complement(join(complement(sk1),converse(sk2))),
inference(backward_demodulation,[status(thm)],[f894,f98]) ).
fof(f942,plain,
! [X0,X1] : join(complement(X0),complement(X1)) = complement(meet(X0,X1)),
inference(backward_demodulation,[status(thm)],[f894,f327]) ).
fof(f959,plain,
! [X0] : join(X0,X0) = complement(complement(X0)),
inference(forward_demodulation,[status(thm)],[f922,f910]) ).
fof(f963,plain,
! [X0] : join(X0,X0) = X0,
inference(forward_demodulation,[status(thm)],[f922,f959]) ).
fof(f1038,plain,
! [X0,X1] : join(X0,join(X0,X1)) = join(X0,X1),
inference(paramodulation,[status(thm)],[f963,f17]) ).
fof(f1412,plain,
! [X0,X1] : join(meet(X0,X1),X0) = join(meet(X0,X1),meet(complement(X1),X0)),
inference(paramodulation,[status(thm)],[f662,f1038]) ).
fof(f1413,plain,
! [X0,X1] : join(meet(X0,X1),X1) = join(meet(X0,X1),meet(X1,complement(X0))),
inference(paramodulation,[status(thm)],[f664,f1038]) ).
fof(f1421,plain,
! [X0] : join(X0,top) = join(X0,complement(X0)),
inference(paramodulation,[status(thm)],[f27,f1038]) ).
fof(f1443,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = join(meet(X0,X1),meet(complement(X1),X0)),
inference(forward_demodulation,[status(thm)],[f16,f1412]) ).
fof(f1449,plain,
! [X0,X1] : join(X0,meet(X0,X1)) = X0,
inference(forward_demodulation,[status(thm)],[f662,f1443]) ).
fof(f1450,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = join(meet(X1,X0),meet(X0,complement(X1))),
inference(forward_demodulation,[status(thm)],[f16,f1413]) ).
fof(f1452,plain,
! [X0,X1] : join(X0,meet(X1,X0)) = X0,
inference(forward_demodulation,[status(thm)],[f664,f1450]) ).
fof(f1462,plain,
! [X0] : join(X0,top) = top,
inference(forward_demodulation,[status(thm)],[f27,f1421]) ).
fof(f1475,plain,
! [X0] : join(top,X0) = top,
inference(paramodulation,[status(thm)],[f16,f1462]) ).
fof(f1479,plain,
! [X0] : converse(top) = join(X0,converse(top)),
inference(paramodulation,[status(thm)],[f1462,f42]) ).
fof(f1647,plain,
! [X0,X1] : top = join(X0,join(complement(X1),meet(complement(X0),X1))),
inference(paramodulation,[status(thm)],[f922,f212]) ).
fof(f1663,plain,
! [X0,X1] : X0 = join(meet(X0,join(complement(X1),meet(X0,X1))),complement(top)),
inference(paramodulation,[status(thm)],[f212,f37]) ).
fof(f1703,plain,
! [X0,X1] : X0 = join(complement(top),meet(X0,join(complement(X1),meet(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f16,f1663]) ).
fof(f1704,plain,
! [X0,X1] : X0 = join(zero,meet(X0,join(complement(X1),meet(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f213,f1703]) ).
fof(f1705,plain,
! [X0,X1] : X0 = meet(X0,join(complement(X1),meet(X0,X1))),
inference(forward_demodulation,[status(thm)],[f894,f1704]) ).
fof(f1729,plain,
complement(sk1) = join(complement(sk1),converse(sk2)),
inference(paramodulation,[status(thm)],[f931,f922]) ).
fof(f1765,plain,
converse(complement(sk1)) = join(converse(complement(sk1)),sk2),
inference(paramodulation,[status(thm)],[f1729,f43]) ).
fof(f1771,plain,
converse(complement(sk1)) = join(sk2,converse(complement(sk1))),
inference(forward_demodulation,[status(thm)],[f16,f1765]) ).
fof(f1893,plain,
! [X0,X1] : converse(converse(X0)) = join(X0,converse(meet(X1,converse(X0)))),
inference(paramodulation,[status(thm)],[f1452,f42]) ).
fof(f1907,plain,
! [X0,X1] : X0 = join(X0,converse(meet(X1,converse(X0)))),
inference(forward_demodulation,[status(thm)],[f23,f1893]) ).
fof(f1911,plain,
converse(top) = top,
inference(paramodulation,[status(thm)],[f1475,f1479]) ).
fof(f2664,plain,
! [X0,X1] : join(join(complement(X0),meet(X1,X0)),X1) = join(complement(X0),meet(X1,X0)),
inference(paramodulation,[status(thm)],[f1705,f1452]) ).
fof(f2700,plain,
! [X0,X1] : join(complement(X0),join(meet(X1,X0),X1)) = join(complement(X0),meet(X1,X0)),
inference(forward_demodulation,[status(thm)],[f17,f2664]) ).
fof(f2701,plain,
! [X0,X1] : join(complement(X0),join(X1,meet(X1,X0))) = join(complement(X0),meet(X1,X0)),
inference(forward_demodulation,[status(thm)],[f16,f2700]) ).
fof(f2702,plain,
! [X0,X1] : X0 = meet(X0,join(complement(X1),X0)),
inference(backward_demodulation,[status(thm)],[f2709,f1705]) ).
fof(f2703,plain,
! [X0,X1] : top = join(complement(X0),join(complement(X1),X0)),
inference(backward_demodulation,[status(thm)],[f2709,f212]) ).
fof(f2706,plain,
! [X0,X1] : top = join(X0,join(complement(X1),complement(X0))),
inference(backward_demodulation,[status(thm)],[f2709,f1647]) ).
fof(f2709,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),meet(X1,X0)),
inference(forward_demodulation,[status(thm)],[f1449,f2701]) ).
fof(f2716,plain,
! [X0,X1] : top = join(X0,join(complement(X0),complement(X1))),
inference(forward_demodulation,[status(thm)],[f487,f2703]) ).
fof(f2717,plain,
! [X0,X1] : top = join(X0,complement(meet(X0,X1))),
inference(forward_demodulation,[status(thm)],[f942,f2716]) ).
fof(f2722,plain,
! [X0,X1] : top = join(X0,complement(meet(X1,X0))),
inference(forward_demodulation,[status(thm)],[f942,f2706]) ).
fof(f2746,plain,
! [X0,X1] : X0 = meet(X0,join(X1,X0)),
inference(paramodulation,[status(thm)],[f922,f2702]) ).
fof(f2833,plain,
! [X0,X1] : X0 = meet(X0,join(X0,X1)),
inference(paramodulation,[status(thm)],[f16,f2746]) ).
fof(f2895,plain,
sk2 = meet(sk2,converse(complement(sk1))),
inference(paramodulation,[status(thm)],[f1771,f2833]) ).
fof(f3143,plain,
top = join(converse(complement(sk1)),complement(sk2)),
inference(paramodulation,[status(thm)],[f2895,f2722]) ).
fof(f3177,plain,
top = join(complement(sk2),converse(complement(sk1))),
inference(forward_demodulation,[status(thm)],[f16,f3143]) ).
fof(f4369,plain,
converse(top) = join(converse(complement(sk2)),complement(sk1)),
inference(paramodulation,[status(thm)],[f3177,f43]) ).
fof(f4382,plain,
top = join(converse(complement(sk2)),complement(sk1)),
inference(forward_demodulation,[status(thm)],[f1911,f4369]) ).
fof(f4383,plain,
top = join(complement(sk1),converse(complement(sk2))),
inference(forward_demodulation,[status(thm)],[f16,f4382]) ).
fof(f4396,plain,
sk1 = join(meet(sk1,converse(complement(sk2))),complement(top)),
inference(paramodulation,[status(thm)],[f4383,f37]) ).
fof(f4407,plain,
sk1 = join(complement(top),meet(sk1,converse(complement(sk2)))),
inference(forward_demodulation,[status(thm)],[f16,f4396]) ).
fof(f4408,plain,
sk1 = join(zero,meet(sk1,converse(complement(sk2)))),
inference(forward_demodulation,[status(thm)],[f213,f4407]) ).
fof(f4409,plain,
sk1 = meet(sk1,converse(complement(sk2))),
inference(forward_demodulation,[status(thm)],[f894,f4408]) ).
fof(f4422,plain,
complement(sk2) = join(complement(sk2),converse(sk1)),
inference(paramodulation,[status(thm)],[f4409,f1907]) ).
fof(f4450,plain,
converse(sk1) = meet(converse(sk1),complement(sk2)),
inference(paramodulation,[status(thm)],[f4422,f2746]) ).
fof(f4459,plain,
converse(sk1) = meet(complement(sk2),converse(sk1)),
inference(forward_demodulation,[status(thm)],[f477,f4450]) ).
fof(f4469,plain,
top = join(complement(sk2),complement(converse(sk1))),
inference(paramodulation,[status(thm)],[f4459,f2717]) ).
fof(f4482,plain,
top = complement(meet(sk2,converse(sk1))),
inference(forward_demodulation,[status(thm)],[f942,f4469]) ).
fof(f4666,plain,
complement(top) = meet(sk2,converse(sk1)),
inference(paramodulation,[status(thm)],[f4482,f922]) ).
fof(f4694,plain,
zero = meet(sk2,converse(sk1)),
inference(forward_demodulation,[status(thm)],[f213,f4666]) ).
fof(f4695,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f4694,f469]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : REL007-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Mon Sep 21 03:57:37 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.31 % Drodi V4.1.1
% 1.19/0.54 % Refutation found
% 1.19/0.54 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 1.19/0.54 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.19/0.55 % Elapsed time: 0.243024 seconds
% 1.19/0.55 % CPU time: 1.818732 seconds
% 1.19/0.55 % Total memory used: 66.518 MB
% 1.19/0.55 % Net memory used: 64.239 MB
%------------------------------------------------------------------------------