%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL128-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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 01:09:25 PM UTC 2026
% Result : Unsatisfiable 247.98s 31.78s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL128-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n017.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 00:01:42 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.13/0.36 % Drodi V4.1.1
% 247.98/31.78 % Refutation found
% 247.98/31.78 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 247.98/31.78 % SZS output start CNFRefutation for theBenchmark
% 247.98/31.78 fof(f1,axiom,(
% 247.98/31.78 (![X,Y]: (( ~ is_a_theorem(equivalent(X,Y))| ~ is_a_theorem(X)| is_a_theorem(Y) ) ))),
% 247.98/31.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 247.98/31.78 fof(f2,axiom,(
% 247.98/31.78 (![X,Y,Z,U]: (is_a_theorem(equivalent(X,equivalent(X,equivalent(equivalent(equivalent(Y,Z),equivalent(U,Z)),equivalent(Y,U))))) ))),
% 247.98/31.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 247.98/31.78 fof(f3,negated_conjecture,(
% 247.98/31.78 ~ is_a_theorem(equivalent(a,equivalent(a,equivalent(equivalent(b,c),equivalent(equivalent(b,e),equivalent(c,e)))))) ),
% 247.98/31.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 247.98/31.78 fof(f4,plain,(
% 247.98/31.78 ![Y]: ((![X]: (~is_a_theorem(equivalent(X,Y))|~is_a_theorem(X)))|is_a_theorem(Y))),
% 247.98/31.78 inference(miniscoping,[status(thm)],[f1])).
% 247.98/31.78 fof(f5,plain,(
% 247.98/31.78 ![X0,X1]: (~is_a_theorem(equivalent(X0,X1))|~is_a_theorem(X0)|is_a_theorem(X1))),
% 247.98/31.78 inference(cnf_transformation,[status(thm)],[f4])).
% 247.98/31.78 fof(f6,plain,(
% 247.98/31.78 ![X0,X1,X2,X3]: (is_a_theorem(equivalent(X0,equivalent(X0,equivalent(equivalent(equivalent(X1,X2),equivalent(X3,X2)),equivalent(X1,X3))))))),
% 247.98/31.78 inference(cnf_transformation,[status(thm)],[f2])).
% 247.98/31.78 fof(f7,plain,(
% 247.98/31.78 ~is_a_theorem(equivalent(a,equivalent(a,equivalent(equivalent(b,c),equivalent(equivalent(b,e),equivalent(c,e))))))),
% 247.98/31.78 inference(cnf_transformation,[status(thm)],[f3])).
% 247.98/31.78 fof(f8,plain,(
% 247.98/31.78 ![X0,X1,X2,X3]: (~is_a_theorem(X0)|is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X1,X2),equivalent(X3,X2)),equivalent(X1,X3)))))),
% 247.98/31.78 inference(resolution,[status(thm)],[f6,f5])).
% 247.98/31.78 fof(f9,plain,(
% 247.98/31.78 ![X0,X1,X2,X3]: (~is_a_theorem(X0)|~is_a_theorem(X0)|is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(X3,X2)),equivalent(X1,X3))))),
% 247.98/31.78 inference(resolution,[status(thm)],[f8,f5])).
% 247.98/31.78 fof(f10,definition,(
% 247.98/31.78 ![X0]: (sQ0_spl <=> (~is_a_theorem(X0)|~is_a_theorem(X0)))),
% 247.98/31.78 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 247.98/31.78 fof(f11,plain,(
% 247.98/31.78 ![X0]: (~is_a_theorem(X0)|~is_a_theorem(X0)|~sQ0_spl)),
% 247.98/31.78 inference(component_clause,[status(thm)],[f10])).
% 247.98/31.78 fof(f13,definition,(
% 247.98/31.78 ![X1,X2,X3]: (sQ1_spl <=> (is_a_theorem(equivalent(equivalent(equivalent(X1,X2),equivalent(X3,X2)),equivalent(X1,X3)))))),
% 247.98/31.78 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 247.98/31.78 fof(f14,plain,(
% 247.98/31.78 ![X0,X1,X2]: (is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(X2,X1)),equivalent(X0,X2)))|~sQ1_spl)),
% 247.98/31.78 inference(component_clause,[status(thm)],[f13])).
% 247.98/31.78 fof(f16,plain,(
% 247.98/31.78 sQ0_spl|sQ1_spl),
% 247.98/31.78 inference(split_clause,[status(thm)],[f9,f10,f13])).
% 247.98/31.78 fof(f17,plain,(
% 247.98/31.78 ![X0]: (~is_a_theorem(X0)|~sQ0_spl)),
% 247.98/31.78 inference(duplicate_literals_removal,[status(thm)],[f11])).
% 247.98/31.78 fof(f18,plain,(
% 247.98/31.78 $false|~sQ0_spl),
% 247.98/31.78 inference(backward_subsumption_resolution,[status(thm)],[f6,f17])).
% 247.98/31.78 fof(f19,plain,(
% 247.98/31.78 ~sQ0_spl),
% 247.98/31.78 inference(contradiction_clause,[status(thm)],[f18])).
% 247.98/31.78 fof(f20,plain,(
% 247.98/31.78 ![X0,X1,X2]: (~is_a_theorem(equivalent(equivalent(X0,X1),equivalent(X2,X1)))|is_a_theorem(equivalent(X0,X2))|~sQ1_spl)),
% 247.98/31.78 inference(resolution,[status(thm)],[f14,f5])).
% 247.98/31.78 fof(f21,plain,(
% 247.98/31.78 ![X0,X1,X2,X3,X4,X5]: (is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,X1),equivalent(X2,X1)),equivalent(X0,X2)),equivalent(equivalent(equivalent(X3,X4),equivalent(X5,X4)),equivalent(X3,X5))))|~sQ1_spl)),
% 247.98/31.78 inference(resolution,[status(thm)],[f8,f14])).
% 247.98/31.78 fof(f25,plain,(
% 247.98/31.78 ![X0,X1,X2,X3]: (is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(X2,X1)),equivalent(equivalent(X0,X3),equivalent(X2,X3))))|~sQ1_spl)),
% 247.98/31.78 inference(resolution,[status(thm)],[f21,f20])).
% 247.98/31.78 fof(f28,definition,(
% 247.98/31.78 ![X0,X1,X2]: (sQ2_spl <=> (~is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(X2,X1)),equivalent(X0,X2)))))),
% 247.98/31.78 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 247.98/31.78 fof(f29,plain,(
% 247.98/31.78 ![X0,X1,X2]: (~is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(X2,X1)),equivalent(X0,X2)))|~sQ2_spl)),
% 247.98/31.78 inference(component_clause,[status(thm)],[f28])).
% 247.98/31.78 fof(f32,plain,(
% 247.98/31.78 ![X0,X1]: (is_a_theorem(equivalent(equivalent(X0,X1),equivalent(X0,X1)))|~sQ1_spl)),
% 247.98/31.78 inference(resolution,[status(thm)],[f25,f20])).
% 247.98/31.78 fof(f33,plain,(
% 247.98/31.78 ![X0,X1,X2,X3]: (~is_a_theorem(equivalent(equivalent(X0,X1),equivalent(X2,X1)))|is_a_theorem(equivalent(equivalent(X0,X3),equivalent(X2,X3)))|~sQ1_spl)),
% 247.98/31.78 inference(resolution,[status(thm)],[f25,f5])).
% 247.98/31.78 fof(f35,plain,(
% 247.98/31.78 ![X0]: (is_a_theorem(equivalent(X0,X0))|~sQ1_spl)),
% 247.98/31.78 inference(resolution,[status(thm)],[f32,f20])).
% 247.98/31.78 fof(f40,plain,(
% 247.98/31.78 ![X0,X1,X2,X3]: (is_a_theorem(equivalent(equivalent(X0,X0),equivalent(equivalent(equivalent(X1,X2),equivalent(X3,X2)),equivalent(X1,X3))))|~sQ1_spl)),
% 247.98/31.78 inference(resolution,[status(thm)],[f35,f8])).
% 247.98/31.78 fof(f44,plain,(
% 247.98/31.78 ![X0,X1,X2]: (is_a_theorem(equivalent(equivalent(X0,X1),equivalent(equivalent(X0,X2),equivalent(X1,X2))))|~sQ1_spl)),
% 247.98/31.78 inference(resolution,[status(thm)],[f40,f20])).
% 247.98/31.78 fof(f51,plain,(
% 247.98/31.78 ![X0,X1,X2]: (~is_a_theorem(equivalent(X0,X1))|is_a_theorem(equivalent(equivalent(X0,X2),equivalent(X1,X2)))|~sQ1_spl)),
% 247.98/31.78 inference(resolution,[status(thm)],[f44,f5])).
% 247.98/31.78 fof(f54,plain,(
% 247.98/31.78 ![X0,X1,X2]: (~is_a_theorem(equivalent(X0,X1))|~is_a_theorem(equivalent(X0,X2))|is_a_theorem(equivalent(X1,X2))|~sQ1_spl)),
% 247.98/31.78 inference(resolution,[status(thm)],[f51,f5])).
% 247.98/31.78 fof(f59,definition,(
% 247.98/31.78 ![X0,X1,X2,X3]: (sQ4_spl <=> (~is_a_theorem(equivalent(X0,equivalent(X0,equivalent(equivalent(equivalent(X1,X2),equivalent(X3,X2)),equivalent(X1,X3)))))))),
% 247.98/31.78 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 247.98/31.78 fof(f60,plain,(
% 247.98/31.78 ![X0,X1,X2,X3]: (~is_a_theorem(equivalent(X0,equivalent(X0,equivalent(equivalent(equivalent(X1,X2),equivalent(X3,X2)),equivalent(X1,X3)))))|~sQ4_spl)),
% 247.98/31.78 inference(component_clause,[status(thm)],[f59])).
% 247.98/31.78 fof(f72,plain,(
% 247.98/31.78 ![X0,X1,X2]: (~is_a_theorem(equivalent(X0,X1))|~is_a_theorem(equivalent(X0,X2))|~is_a_theorem(X1)|is_a_theorem(X2)|~sQ1_spl)),
% 247.98/31.78 inference(resolution,[status(thm)],[f54,f5])).
% 247.98/31.78 fof(f77,plain,(
% 247.98/31.78 ![X0,X1,X2,X3]: (~is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(X2,X1)),X3))|~is_a_theorem(X3)|is_a_theorem(equivalent(X0,X2))|~sQ1_spl)),
% 247.98/31.78 inference(resolution,[status(thm)],[f72,f14])).
% 247.98/31.78 fof(f85,plain,(
% 247.98/31.78 ![X0,X1]: (~is_a_theorem(equivalent(X0,X1))|~is_a_theorem(X1)|is_a_theorem(X0)|~sQ1_spl)),
% 247.98/31.78 inference(resolution,[status(thm)],[f72,f35])).
% 247.98/31.78 fof(f109,plain,(
% 247.98/31.78 ![X0,X1,X2]: (~is_a_theorem(equivalent(X0,X1))|is_a_theorem(equivalent(X2,X1))|~is_a_theorem(equivalent(X2,X0))|~sQ1_spl)),
% 247.98/31.78 inference(resolution,[status(thm)],[f85,f51])).
% 247.98/31.78 fof(f111,plain,(
% 247.98/31.78 ![X0,X1,X2,X3]: (~is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X1,X2),equivalent(X3,X2)),equivalent(X1,X3))))|is_a_theorem(X0)|~sQ1_spl)),
% 247.98/31.78 inference(resolution,[status(thm)],[f85,f6])).
% 247.98/31.78 fof(f127,plain,(
% 247.98/31.78 $false|~sQ1_spl|~sQ2_spl),
% 247.98/31.78 inference(forward_subsumption_resolution,[status(thm)],[f29,f14])).
% 247.98/31.78 fof(f128,plain,(
% 247.98/31.78 ~sQ1_spl|~sQ2_spl),
% 247.98/31.78 inference(contradiction_clause,[status(thm)],[f127])).
% 247.98/31.78 fof(f129,plain,(
% 247.98/31.78 ![X0,X1,X2,X3]: (~is_a_theorem(equivalent(X0,equivalent(X1,X2)))|~is_a_theorem(equivalent(equivalent(X3,X2),X0))|is_a_theorem(equivalent(X3,X1))|~sQ1_spl)),
% 247.98/31.78 inference(resolution,[status(thm)],[f109,f20])).
% 247.98/31.78 fof(f132,plain,(
% 247.98/31.78 ![X0,X1,X2,X3]: (~is_a_theorem(equivalent(X0,X1))|~is_a_theorem(equivalent(X2,X0))|~is_a_theorem(equivalent(X2,X3))|~is_a_theorem(X3)|is_a_theorem(X1)|~sQ1_spl)),
% 247.98/31.78 inference(resolution,[status(thm)],[f109,f72])).
% 247.98/31.78 fof(f321,plain,(
% 247.98/31.78 ![X0,X1,X2,X3]: (is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,X1),equivalent(X2,X1)),X3),equivalent(equivalent(X0,X2),X3)))|~sQ1_spl)),
% 247.98/31.78 inference(resolution,[status(thm)],[f111,f14])).
% 247.98/31.78 fof(f325,plain,(
% 247.98/31.78 ![X0,X1,X2,X3]: (is_a_theorem(equivalent(X0,equivalent(X1,X2)))|~is_a_theorem(equivalent(X0,equivalent(equivalent(X1,X3),equivalent(X2,X3))))|~sQ1_spl)),
% 247.98/31.78 inference(resolution,[status(thm)],[f111,f51])).
% 247.98/31.78 fof(f337,plain,(
% 247.98/31.78 ![X0,X1]: (~is_a_theorem(equivalent(X0,equivalent(equivalent(a,equivalent(equivalent(b,c),equivalent(equivalent(b,e),equivalent(c,e)))),X1)))|~is_a_theorem(equivalent(equivalent(a,X1),X0))|~sQ1_spl)),
% 247.98/31.78 inference(resolution,[status(thm)],[f129,f7])).
% 247.98/31.85 fof(f392,plain,(
% 247.98/31.85 ![X0,X1,X2,X3,X4,X5]: (~is_a_theorem(equivalent(X0,X1))|~is_a_theorem(equivalent(equivalent(X2,X2),X0))|~is_a_theorem(equivalent(equivalent(equivalent(X3,X4),equivalent(X5,X4)),equivalent(X3,X5)))|is_a_theorem(X1)|~sQ1_spl)),
% 247.98/31.85 inference(resolution,[status(thm)],[f132,f40])).
% 247.98/31.85 fof(f423,definition,(
% 247.98/31.85 ![X0,X1,X2]: (sQ25_spl <=> (~is_a_theorem(equivalent(X0,X1))|~is_a_theorem(equivalent(equivalent(X2,X2),X0))|is_a_theorem(X1)))),
% 247.98/31.85 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 247.98/31.85 fof(f424,plain,(
% 247.98/31.85 ![X0,X1,X2]: (~is_a_theorem(equivalent(X0,X1))|~is_a_theorem(equivalent(equivalent(X2,X2),X0))|is_a_theorem(X1)|~sQ25_spl)),
% 247.98/31.85 inference(component_clause,[status(thm)],[f423])).
% 247.98/31.85 fof(f426,plain,(
% 247.98/31.85 sQ25_spl|sQ2_spl|~sQ1_spl),
% 247.98/31.85 inference(split_clause,[status(thm)],[f392,f423,f28,f13])).
% 247.98/31.85 fof(f428,plain,(
% 247.98/31.85 ![X0,X1]: (~is_a_theorem(equivalent(equivalent(X0,X0),X1))|is_a_theorem(X1)|~sQ25_spl|~sQ1_spl)),
% 247.98/31.85 inference(resolution,[status(thm)],[f424,f14])).
% 112.96/31.85 fof(f449,plain,(
% 112.96/31.85 ![X0,X1,X2]: (is_a_theorem(equivalent(X0,X1))|~is_a_theorem(equivalent(equivalent(X1,X2),equivalent(X0,X2)))|~sQ25_spl|~sQ1_spl)),
% 112.96/31.85 inference(resolution,[status(thm)],[f428,f33])).
% 112.96/31.85 fof(f565,plain,(
% 112.96/31.85 $false|~sQ4_spl),
% 112.96/31.85 inference(forward_subsumption_resolution,[status(thm)],[f60,f6])).
% 112.96/31.85 fof(f566,plain,(
% 112.96/31.85 ~sQ4_spl),
% 112.96/31.85 inference(contradiction_clause,[status(thm)],[f565])).
% 112.96/31.85 fof(f1594,plain,(
% 112.96/31.85 ![X0]: (~is_a_theorem(equivalent(equivalent(a,equivalent(X0,equivalent(equivalent(b,c),equivalent(equivalent(b,e),equivalent(c,e))))),equivalent(a,X0)))|~sQ1_spl)),
% 112.96/31.85 inference(resolution,[status(thm)],[f337,f44])).
% 112.96/31.85 fof(f1614,plain,(
% 112.96/31.85 ![X0,X1]: (~is_a_theorem(equivalent(X0,equivalent(a,equivalent(X1,equivalent(equivalent(b,c),equivalent(equivalent(b,e),equivalent(c,e)))))))|~is_a_theorem(equivalent(X0,equivalent(a,X1)))|~sQ1_spl)),
% 112.96/31.85 inference(resolution,[status(thm)],[f1594,f54])).
% 112.96/31.85 fof(f2167,plain,(
% 112.96/31.85 ![X0,X1,X2,X3]: (~is_a_theorem(equivalent(equivalent(X0,X1),equivalent(X2,equivalent(X1,X3))))|is_a_theorem(equivalent(equivalent(X0,X3),X2))|~sQ1_spl)),
% 112.96/31.85 inference(resolution,[status(thm)],[f321,f77])).
% 112.96/31.85 fof(f2228,plain,(
% 112.96/31.85 ![X0,X1,X2,X3]: (is_a_theorem(equivalent(equivalent(X0,equivalent(X1,X2)),equivalent(X0,equivalent(equivalent(X1,X3),equivalent(X2,X3)))))|~sQ1_spl)),
% 112.96/31.85 inference(resolution,[status(thm)],[f325,f6])).
% 112.96/31.85 fof(f8609,plain,(
% 112.96/31.85 ![X0,X1]: (is_a_theorem(equivalent(equivalent(X0,equivalent(X1,X1)),X0))|~sQ1_spl)),
% 112.96/31.85 inference(resolution,[status(thm)],[f2228,f2167])).
% 112.96/31.85 fof(f8635,plain,(
% 112.96/31.85 ![X0]: (~is_a_theorem(equivalent(equivalent(a,equivalent(X0,equivalent(b,c))),equivalent(a,equivalent(X0,equivalent(equivalent(b,e),equivalent(c,e))))))|~sQ1_spl)),
% 112.96/31.85 inference(resolution,[status(thm)],[f2228,f1614])).
% 112.96/31.85 fof(f8761,plain,(
% 112.96/31.85 ![X0,X1]: (is_a_theorem(equivalent(X0,equivalent(X0,equivalent(X1,X1))))|~sQ25_spl|~sQ1_spl)),
% 112.96/31.85 inference(resolution,[status(thm)],[f8609,f449])).
% 112.96/31.85 fof(f9784,plain,(
% 112.96/31.85 ![X0,X1]: (~is_a_theorem(equivalent(X0,equivalent(a,equivalent(X1,equivalent(b,c)))))|~is_a_theorem(equivalent(X0,equivalent(a,equivalent(X1,equivalent(equivalent(b,e),equivalent(c,e))))))|~sQ1_spl)),
% 112.96/31.85 inference(resolution,[status(thm)],[f8635,f54])).
% 112.96/31.85 fof(f20929,plain,(
% 112.96/31.85 ~is_a_theorem(equivalent(a,equivalent(a,equivalent(equivalent(equivalent(b,e),equivalent(c,e)),equivalent(b,c)))))|~sQ25_spl|~sQ1_spl),
% 112.96/31.85 inference(resolution,[status(thm)],[f9784,f8761])).
% 112.96/31.85 fof(f20931,plain,(
% 112.96/31.85 $false|~sQ25_spl|~sQ1_spl),
% 112.96/31.85 inference(forward_subsumption_resolution,[status(thm)],[f20929,f6])).
% 112.96/31.85 fof(f20932,plain,(
% 112.96/31.85 ~sQ25_spl|~sQ1_spl),
% 112.96/31.85 inference(contradiction_clause,[status(thm)],[f20931])).
% 112.96/31.85 fof(f20933,plain,(
% 112.96/31.85 $false),
% 112.96/31.85 inference(sat_refutation,[status(thm)],[f16,f19,f128,f426,f566,f20932])).
% 112.96/31.85 % SZS output end CNFRefutation for theBenchmark.p
% 19.76/31.94 % Elapsed time: 31.557839 seconds
% 19.76/31.94 % CPU time: 249.289096 seconds
% 19.76/31.94 % Total memory used: 632.968 MB
% 19.76/31.94 % Net memory used: 574.422 MB
%------------------------------------------------------------------------------