%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL416-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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:10:01 PM UTC 2026
% Result : Unsatisfiable 61.16s 8.17s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL416-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n019.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 : Mon Sep 21 00:29:49 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 61.16/8.17 % Refutation found
% 61.16/8.17 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 61.16/8.17 % SZS output start CNFRefutation for theBenchmark
% 61.16/8.17 fof(f1,axiom,(
% 61.16/8.17 (![A,B]: (( ~ is_a_theorem(equivalent(A,B))| ~ is_a_theorem(A)| is_a_theorem(B) ) ))),
% 61.16/8.17 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 61.16/8.17 fof(f2,axiom,(
% 61.16/8.17 (![A,B,C]: (is_a_theorem(equivalent(A,equivalent(equivalent(equivalent(A,B),equivalent(C,B)),C))) ))),
% 61.16/8.17 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 61.16/8.17 fof(f3,negated_conjecture,(
% 61.16/8.17 ~ is_a_theorem(equivalent(a,a)) ),
% 61.16/8.17 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 61.16/8.17 fof(f4,plain,(
% 61.16/8.17 ![B]: ((![A]: (~is_a_theorem(equivalent(A,B))|~is_a_theorem(A)))|is_a_theorem(B))),
% 61.16/8.17 inference(miniscoping,[status(thm)],[f1])).
% 61.16/8.17 fof(f5,plain,(
% 61.16/8.17 ![X0,X1]: (~is_a_theorem(equivalent(X0,X1))|~is_a_theorem(X0)|is_a_theorem(X1))),
% 61.16/8.17 inference(cnf_transformation,[status(thm)],[f4])).
% 61.16/8.17 fof(f6,plain,(
% 61.16/8.17 ![X0,X1,X2]: (is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X0,X1),equivalent(X2,X1)),X2))))),
% 61.16/8.17 inference(cnf_transformation,[status(thm)],[f2])).
% 61.16/8.17 fof(f7,plain,(
% 61.16/8.17 ~is_a_theorem(equivalent(a,a))),
% 61.16/8.17 inference(cnf_transformation,[status(thm)],[f3])).
% 61.16/8.17 fof(f8,plain,(
% 61.16/8.17 ![X0,X1,X2]: (~is_a_theorem(X0)|is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(X2,X1)),X2)))),
% 61.16/8.17 inference(resolution,[status(thm)],[f6,f5])).
% 61.16/8.17 fof(f9,plain,(
% 61.16/8.17 ![X0,X1,X2]: (~is_a_theorem(X0)|~is_a_theorem(equivalent(equivalent(X0,X1),equivalent(X2,X1)))|is_a_theorem(X2))),
% 61.16/8.17 inference(resolution,[status(thm)],[f8,f5])).
% 61.16/8.17 fof(f11,plain,(
% 61.16/8.17 ![X0,X1,X2,X3,X4]: (~is_a_theorem(equivalent(equivalent(equivalent(X0,equivalent(equivalent(equivalent(X0,X1),equivalent(X2,X1)),X2)),X3),equivalent(X4,X3)))|is_a_theorem(X4))),
% 61.16/8.17 inference(resolution,[status(thm)],[f9,f6])).
% 61.16/8.17 fof(f14,plain,(
% 61.16/8.17 ![X0,X1,X2,X3,X4]: (is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,equivalent(equivalent(equivalent(X0,X1),equivalent(X2,X1)),X2)),X3),X4),equivalent(X3,X4))))),
% 61.16/8.17 inference(resolution,[status(thm)],[f11,f6])).
% 61.16/8.17 fof(f15,plain,(
% 61.16/8.17 ![X0,X1,X2,X3,X4]: (is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,equivalent(equivalent(equivalent(X0,X1),equivalent(X2,X1)),X2)),X3),equivalent(X4,X3)),X4)))),
% 61.16/8.17 inference(resolution,[status(thm)],[f14,f11])).
% 61.16/8.17 fof(f16,plain,(
% 61.16/8.17 ![X0,X1,X2,X3,X4]: (~is_a_theorem(equivalent(equivalent(equivalent(X0,equivalent(equivalent(equivalent(X0,X1),equivalent(X2,X1)),X2)),X3),X4))|is_a_theorem(equivalent(X3,X4)))),
% 61.16/8.17 inference(resolution,[status(thm)],[f14,f5])).
% 61.16/8.17 fof(f24,plain,(
% 61.16/8.17 ![X0,X1,X2,X3]: (is_a_theorem(equivalent(equivalent(X0,equivalent(equivalent(equivalent(X1,X2),equivalent(X3,X2)),X3)),X0))|~is_a_theorem(X1))),
% 61.16/8.17 inference(resolution,[status(thm)],[f16,f8])).
% 61.16/8.17 fof(f28,plain,(
% 61.16/8.17 ![X0,X1,X2,X3]: (~is_a_theorem(X0)|~is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X0,X2),equivalent(X3,X2)),X3)))|is_a_theorem(X1))),
% 61.16/8.17 inference(resolution,[status(thm)],[f24,f5])).
% 61.16/8.17 fof(f33,plain,(
% 61.16/8.17 ![X0,X1,X2,X3,X4]: (~is_a_theorem(X0)|is_a_theorem(equivalent(equivalent(X1,X2),equivalent(equivalent(equivalent(equivalent(X0,X3),equivalent(X4,X3)),X4),X2)))|~is_a_theorem(X1))),
% 61.16/8.17 inference(resolution,[status(thm)],[f28,f8])).
% 61.16/8.17 fof(f38,plain,(
% 61.16/8.17 ![X0,X1,X2,X3,X4]: (~is_a_theorem(X0)|~is_a_theorem(X1)|~is_a_theorem(equivalent(X1,X2))|is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,X3),equivalent(X4,X3)),X4),X2)))),
% 61.16/8.17 inference(resolution,[status(thm)],[f33,f5])).
% 61.16/8.17 fof(f44,definition,(
% 61.16/8.17 ![X1,X2,X3]: (sQ1_spl <=> (~is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X1,X2),equivalent(X3,X2)),X3)))))),
% 61.16/8.17 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 61.16/8.17 fof(f45,plain,(
% 61.16/8.17 ![X0,X1,X2]: (~is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X0,X1),equivalent(X2,X1)),X2)))|~sQ1_spl)),
% 61.16/8.17 inference(component_clause,[status(thm)],[f44])).
% 61.16/8.17 fof(f52,plain,(
% 61.16/8.17 $false|~sQ1_spl),
% 61.16/8.17 inference(forward_subsumption_resolution,[status(thm)],[f45,f6])).
% 61.16/8.17 fof(f53,plain,(
% 61.16/8.17 ~sQ1_spl),
% 61.16/8.17 inference(contradiction_clause,[status(thm)],[f52])).
% 61.16/8.17 fof(f61,plain,(
% 61.16/8.17 ![X0,X1,X2,X3,X4]: (~is_a_theorem(X0)|~is_a_theorem(X1)|~is_a_theorem(equivalent(X1,X2))|is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,X3),X4),equivalent(X3,X4)),X2)))),
% 61.16/8.17 inference(resolution,[status(thm)],[f38,f16])).
% 61.16/8.17 fof(f63,plain,(
% 61.16/8.17 ![X0,X1,X2,X3,X4]: (~is_a_theorem(X0)|~is_a_theorem(X1)|~is_a_theorem(equivalent(X1,X2))|~is_a_theorem(equivalent(equivalent(equivalent(X0,X3),equivalent(X4,X3)),X4))|is_a_theorem(X2))),
% 61.16/8.17 inference(resolution,[status(thm)],[f38,f5])).
% 61.16/8.17 fof(f67,definition,(
% 61.16/8.17 ![X1,X2,X3,X4]: (sQ3_spl <=> (~is_a_theorem(X1)|~is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X3),equivalent(X4,X3)),X4)))|~is_a_theorem(X2)))),
% 61.16/8.17 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 61.16/8.17 fof(f68,plain,(
% 61.16/8.17 ![X0,X1,X2,X3]: (~is_a_theorem(X0)|~is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X1,X2),equivalent(X3,X2)),X3)))|~is_a_theorem(X1)|~sQ3_spl)),
% 61.16/8.17 inference(component_clause,[status(thm)],[f67])).
% 61.16/8.17 fof(f71,definition,(
% 61.16/8.17 ![X0,X3,X4]: (sQ4_spl <=> (~is_a_theorem(X0)|~is_a_theorem(equivalent(equivalent(equivalent(X0,X3),equivalent(X4,X3)),X4))))),
% 61.16/8.17 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 61.16/8.17 fof(f72,plain,(
% 61.16/8.17 ![X0,X1,X2]: (~is_a_theorem(X0)|~is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(X2,X1)),X2))|~sQ4_spl)),
% 61.16/8.17 inference(component_clause,[status(thm)],[f71])).
% 61.16/8.17 fof(f74,definition,(
% 61.16/8.17 ![X1,X2]: (sQ5_spl <=> (~is_a_theorem(X1)|~is_a_theorem(equivalent(X1,X2))|is_a_theorem(X2)))),
% 61.16/8.17 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 61.16/8.17 fof(f75,plain,(
% 61.16/8.17 ![X0,X1]: (~is_a_theorem(X0)|~is_a_theorem(equivalent(X0,X1))|is_a_theorem(X1)|~sQ5_spl)),
% 61.16/8.17 inference(component_clause,[status(thm)],[f74])).
% 61.16/8.17 fof(f77,plain,(
% 61.16/8.17 sQ4_spl|sQ5_spl),
% 61.16/8.17 inference(split_clause,[status(thm)],[f63,f71,f74])).
% 61.16/8.17 fof(f78,plain,(
% 61.16/8.17 ![X0]: (~is_a_theorem(X0)|~sQ4_spl)),
% 61.16/8.17 inference(forward_subsumption_resolution,[status(thm)],[f72,f8])).
% 61.16/8.17 fof(f79,plain,(
% 61.16/8.17 $false|~sQ4_spl),
% 61.16/8.17 inference(backward_subsumption_resolution,[status(thm)],[f15,f78])).
% 61.16/8.17 fof(f82,plain,(
% 61.16/8.17 ~sQ4_spl),
% 61.16/8.17 inference(contradiction_clause,[status(thm)],[f79])).
% 61.16/8.17 fof(f86,plain,(
% 61.16/8.17 ![X0,X1,X2,X3,X4]: (~is_a_theorem(equivalent(equivalent(equivalent(X0,equivalent(equivalent(equivalent(X0,X1),equivalent(X2,X1)),X2)),X3),equivalent(X4,X3)))|is_a_theorem(X4))),
% 61.16/8.17 inference(resolution,[status(thm)],[f9,f6])).
% 61.16/8.17 fof(f98,plain,(
% 61.16/8.17 ![X0,X1,X2,X3,X4,X5,X6]: (~is_a_theorem(X0)|~is_a_theorem(X1)|~is_a_theorem(equivalent(X1,equivalent(equivalent(equivalent(X2,X3),equivalent(X4,X3)),X4)))|~is_a_theorem(X2)|is_a_theorem(equivalent(equivalent(equivalent(X0,X5),X6),equivalent(X5,X6))))),
% 61.16/8.17 inference(resolution,[status(thm)],[f61,f28])).
% 61.16/8.17 fof(f103,definition,(
% 61.16/8.17 ![X0,X5,X6]: (sQ6_spl <=> (~is_a_theorem(X0)|is_a_theorem(equivalent(equivalent(equivalent(X0,X5),X6),equivalent(X5,X6)))))),
% 61.16/8.17 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 61.16/8.17 fof(f104,plain,(
% 61.16/8.17 ![X0,X1,X2]: (~is_a_theorem(X0)|is_a_theorem(equivalent(equivalent(equivalent(X0,X1),X2),equivalent(X1,X2)))|~sQ6_spl)),
% 61.16/8.17 inference(component_clause,[status(thm)],[f103])).
% 61.16/8.17 fof(f106,plain,(
% 61.16/8.17 sQ6_spl|sQ3_spl),
% 61.16/8.17 inference(split_clause,[status(thm)],[f98,f103,f67])).
% 61.16/8.17 fof(f115,plain,(
% 61.16/8.17 ![X0,X1,X2,X3]: (~is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X1,X2),equivalent(X3,X2)),X3)))|~is_a_theorem(X1)|~sQ3_spl)),
% 61.16/8.17 inference(forward_subsumption_resolution,[status(thm)],[f68,f28])).
% 61.16/8.17 fof(f121,plain,(
% 61.16/8.17 ![X0,X1]: (~is_a_theorem(X0)|~is_a_theorem(X1)|~sQ3_spl)),
% 61.16/8.17 inference(resolution,[status(thm)],[f115,f8])).
% 61.16/8.17 fof(f124,definition,(
% 61.16/8.17 ![X1]: (sQ9_spl <=> (~is_a_theorem(X1)))),
% 61.16/8.17 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 61.16/8.17 fof(f125,plain,(
% 61.16/8.17 ![X0]: (~is_a_theorem(X0)|~sQ9_spl)),
% 61.16/8.17 inference(component_clause,[status(thm)],[f124])).
% 61.16/8.17 fof(f128,plain,(
% 61.16/8.17 sQ9_spl|~sQ3_spl),
% 61.16/8.17 inference(split_clause,[status(thm)],[f121,f124,f67])).
% 61.16/8.17 fof(f131,plain,(
% 61.16/8.17 $false|~sQ9_spl),
% 61.16/8.17 inference(backward_subsumption_resolution,[status(thm)],[f6,f125])).
% 61.16/8.17 fof(f132,plain,(
% 61.16/8.17 ~sQ9_spl),
% 61.16/8.17 inference(contradiction_clause,[status(thm)],[f131])).
% 61.16/8.17 fof(f135,plain,(
% 61.16/8.17 ![X0,X1,X2,X3,X4]: (is_a_theorem(equivalent(equivalent(equivalent(equivalent(X0,equivalent(equivalent(equivalent(X0,X1),equivalent(X2,X1)),X2)),X3),equivalent(X4,X3)),X4)))),
% 61.16/8.17 inference(resolution,[status(thm)],[f8,f6])).
% 61.16/8.17 fof(f139,plain,(
% 61.16/8.17 ![X0,X1,X2]: (~is_a_theorem(X0)|~is_a_theorem(equivalent(equivalent(X0,X1),X2))|is_a_theorem(equivalent(X1,X2))|~sQ6_spl|~sQ5_spl)),
% 61.16/8.17 inference(resolution,[status(thm)],[f104,f75])).
% 61.16/8.17 fof(f141,plain,(
% 61.16/8.17 ![X0,X1,X2]: (~is_a_theorem(equivalent(X0,X1))|is_a_theorem(equivalent(X2,equivalent(X1,X2)))|~is_a_theorem(X0)|~sQ5_spl|~sQ6_spl)),
% 61.16/8.17 inference(resolution,[status(thm)],[f139,f104])).
% 61.16/8.17 fof(f144,plain,(
% 61.16/8.17 ![X0,X1,X2]: (~is_a_theorem(equivalent(X0,X1))|~is_a_theorem(X0)|~is_a_theorem(X2)|is_a_theorem(equivalent(X1,X2))|~sQ6_spl|~sQ5_spl)),
% 61.16/8.17 inference(resolution,[status(thm)],[f141,f75])).
% 61.16/8.17 fof(f161,definition,(
% 61.16/8.17 ![X0,X1]: (sQ12_spl <=> (~is_a_theorem(equivalent(X0,X1))|~is_a_theorem(X0)|~is_a_theorem(X1)))),
% 61.16/8.17 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 61.16/8.17 fof(f162,plain,(
% 61.16/8.17 ![X0,X1]: (~is_a_theorem(equivalent(X0,X1))|~is_a_theorem(X0)|~is_a_theorem(X1)|~sQ12_spl)),
% 61.16/8.17 inference(component_clause,[status(thm)],[f161])).
% 61.16/8.17 fof(f168,plain,(
% 61.16/8.17 ![X0,X1]: (~is_a_theorem(equivalent(X0,X1))|~is_a_theorem(X0)|~sQ5_spl|~sQ12_spl)),
% 61.16/8.17 inference(forward_subsumption_resolution,[status(thm)],[f162,f75])).
% 61.16/8.17 fof(f186,plain,(
% 61.16/8.17 ![X0]: (~is_a_theorem(X0)|~sQ5_spl|~sQ12_spl)),
% 61.16/8.17 inference(resolution,[status(thm)],[f168,f6])).
% 61.16/8.17 fof(f187,plain,(
% 61.16/8.17 sQ9_spl|~sQ5_spl|~sQ12_spl),
% 61.16/8.17 inference(split_clause,[status(thm)],[f186,f124,f74,f161])).
% 61.16/8.17 fof(f201,plain,(
% 61.16/8.17 ![X0,X1,X2,X3]: (is_a_theorem(equivalent(X0,equivalent(X1,X0)))|~is_a_theorem(X2)|~is_a_theorem(equivalent(X3,X2))|~is_a_theorem(X3)|~is_a_theorem(X1)|~sQ6_spl|~sQ5_spl)),
% 61.16/8.17 inference(resolution,[status(thm)],[f141,f144])).
% 61.16/8.17 fof(f202,definition,(
% 61.16/8.17 ![X0,X1]: (sQ15_spl <=> (is_a_theorem(equivalent(X0,equivalent(X1,X0)))|~is_a_theorem(X1)))),
% 61.16/8.17 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 61.16/8.17 fof(f203,plain,(
% 61.16/8.17 ![X0,X1]: (is_a_theorem(equivalent(X0,equivalent(X1,X0)))|~is_a_theorem(X1)|~sQ15_spl)),
% 61.16/8.17 inference(component_clause,[status(thm)],[f202])).
% 61.16/8.17 fof(f205,plain,(
% 61.16/8.17 sQ15_spl|sQ12_spl|~sQ6_spl|~sQ5_spl),
% 61.16/8.17 inference(split_clause,[status(thm)],[f201,f202,f161,f103,f74])).
% 61.16/8.17 fof(f207,plain,(
% 61.16/8.17 ![X0,X1,X2]: (~is_a_theorem(X0)|is_a_theorem(equivalent(X1,equivalent(equivalent(X0,X2),X1)))|~is_a_theorem(X2)|~sQ15_spl|~sQ5_spl|~sQ6_spl)),
% 61.16/8.17 inference(resolution,[status(thm)],[f203,f141])).
% 61.16/8.17 fof(f217,definition,(
% 61.16/8.17 ![X0]: (sQ16_spl <=> (~is_a_theorem(X0)|~is_a_theorem(X0)))),
% 61.16/8.17 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 61.16/8.17 fof(f218,plain,(
% 61.16/8.17 ![X0]: (~is_a_theorem(X0)|~is_a_theorem(X0)|~sQ16_spl)),
% 61.16/8.17 inference(component_clause,[status(thm)],[f217])).
% 61.16/8.17 fof(f240,plain,(
% 61.16/8.17 ![X0,X1,X2]: (~is_a_theorem(X0)|~is_a_theorem(X1)|~is_a_theorem(X2)|is_a_theorem(equivalent(equivalent(X0,X1),X2))|~sQ15_spl|~sQ6_spl|~sQ5_spl)),
% 61.16/8.17 inference(resolution,[status(thm)],[f207,f75])).
% 61.16/8.17 fof(f276,plain,(
% 61.16/8.17 ![X0,X1,X2,X3,X4]: (~is_a_theorem(equivalent(X0,equivalent(equivalent(equivalent(X0,X1),equivalent(X2,X1)),X2)))|~is_a_theorem(X3)|~is_a_theorem(equivalent(X4,X3))|is_a_theorem(X4)|~sQ15_spl|~sQ6_spl|~sQ5_spl)),
% 61.16/8.17 inference(resolution,[status(thm)],[f240,f11])).
% 61.16/8.17 fof(f287,definition,(
% 61.16/8.17 ![X3,X4]: (sQ18_spl <=> (~is_a_theorem(X3)|~is_a_theorem(equivalent(X4,X3))|is_a_theorem(X4)))),
% 61.16/8.17 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 61.16/8.17 fof(f288,plain,(
% 61.16/8.17 ![X0,X1]: (~is_a_theorem(X0)|~is_a_theorem(equivalent(X1,X0))|is_a_theorem(X1)|~sQ18_spl)),
% 61.16/8.17 inference(component_clause,[status(thm)],[f287])).
% 61.16/8.17 fof(f290,plain,(
% 61.16/8.17 sQ1_spl|sQ18_spl|~sQ15_spl|~sQ6_spl|~sQ5_spl),
% 61.16/8.17 inference(split_clause,[status(thm)],[f276,f44,f287,f202,f103,f74])).
% 61.16/8.17 fof(f302,plain,(
% 61.16/8.17 ![X0,X1,X2]: (~is_a_theorem(equivalent(X0,X1))|is_a_theorem(equivalent(equivalent(X2,X0),X1))|~is_a_theorem(X2)|~sQ18_spl|~sQ6_spl)),
% 61.16/8.18 inference(resolution,[status(thm)],[f288,f104])).
% 61.16/8.18 fof(f304,plain,(
% 61.16/8.18 ![X0,X1,X2]: (~is_a_theorem(equivalent(equivalent(equivalent(X0,X1),equivalent(X2,X1)),X2))|is_a_theorem(X0)|~sQ18_spl)),
% 61.16/8.18 inference(resolution,[status(thm)],[f288,f6])).
% 61.16/8.18 fof(f343,plain,(
% 61.16/8.18 ![X0]: (~is_a_theorem(X0)|~sQ16_spl)),
% 61.16/8.18 inference(duplicate_literals_removal,[status(thm)],[f218])).
% 61.16/8.18 fof(f344,plain,(
% 61.16/8.18 $false|~sQ16_spl),
% 61.16/8.18 inference(backward_subsumption_resolution,[status(thm)],[f135,f343])).
% 61.16/8.18 fof(f346,plain,(
% 61.16/8.18 ~sQ16_spl),
% 61.16/8.18 inference(contradiction_clause,[status(thm)],[f344])).
% 61.16/8.18 fof(f376,plain,(
% 61.16/8.18 ![X0,X1,X2]: (~is_a_theorem(equivalent(equivalent(X0,X1),X0))|~is_a_theorem(equivalent(X2,X1))|is_a_theorem(X2)|~sQ6_spl|~sQ18_spl)),
% 61.16/8.18 inference(resolution,[status(thm)],[f302,f304])).
% 61.16/8.18 fof(f529,plain,(
% 61.16/8.18 ![X0,X1,X2,X3,X4]: (is_a_theorem(X0)|~is_a_theorem(equivalent(X1,equivalent(X0,X1)))|~is_a_theorem(equivalent(X2,equivalent(equivalent(equivalent(X2,X3),equivalent(X4,X3)),X4)))|~sQ18_spl|~sQ6_spl)),
% 61.16/8.18 inference(resolution,[status(thm)],[f86,f302])).
% 61.16/8.18 fof(f534,definition,(
% 61.16/8.18 ![X0,X1]: (sQ23_spl <=> (is_a_theorem(X0)|~is_a_theorem(equivalent(X1,equivalent(X0,X1)))))),
% 61.16/8.18 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 61.16/8.18 fof(f535,plain,(
% 61.16/8.18 ![X0,X1]: (is_a_theorem(X0)|~is_a_theorem(equivalent(X1,equivalent(X0,X1)))|~sQ23_spl)),
% 61.16/8.18 inference(component_clause,[status(thm)],[f534])).
% 61.16/8.18 fof(f537,plain,(
% 61.16/8.18 sQ23_spl|sQ1_spl|~sQ18_spl|~sQ6_spl),
% 61.16/8.18 inference(split_clause,[status(thm)],[f529,f534,f44,f287,f103])).
% 61.16/8.18 fof(f540,plain,(
% 61.16/8.18 ![X0,X1]: (is_a_theorem(equivalent(equivalent(X0,X1),equivalent(X0,X1)))|~sQ23_spl)),
% 61.16/8.18 inference(resolution,[status(thm)],[f535,f6])).
% 61.16/8.18 fof(f959,plain,(
% 61.16/8.18 ![X0,X1,X2]: (~is_a_theorem(equivalent(equivalent(X0,equivalent(X1,X2)),X0))|is_a_theorem(equivalent(X1,X2))|~sQ6_spl|~sQ18_spl|~sQ23_spl)),
% 61.16/8.18 inference(resolution,[status(thm)],[f376,f540])).
% 61.16/8.18 fof(f2026,plain,(
% 61.16/8.18 ![X0,X1]: (is_a_theorem(equivalent(equivalent(X0,X1),X1))|~is_a_theorem(X0)|~sQ6_spl|~sQ18_spl|~sQ23_spl)),
% 61.16/8.18 inference(resolution,[status(thm)],[f959,f8])).
% 61.16/8.18 fof(f2050,plain,(
% 61.16/8.18 ![X0,X1]: (~is_a_theorem(X0)|~is_a_theorem(X0)|is_a_theorem(equivalent(X1,X1))|~sQ18_spl|~sQ23_spl|~sQ6_spl|~sQ5_spl)),
% 61.16/8.18 inference(resolution,[status(thm)],[f2026,f139])).
% 61.16/8.18 fof(f2117,definition,(
% 61.16/8.18 ![X1]: (sQ56_spl <=> (is_a_theorem(equivalent(X1,X1))))),
% 61.16/8.18 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 61.16/8.18 fof(f2118,plain,(
% 61.16/8.18 ![X0]: (is_a_theorem(equivalent(X0,X0))|~sQ56_spl)),
% 61.16/8.18 inference(component_clause,[status(thm)],[f2117])).
% 61.16/8.18 fof(f2120,plain,(
% 61.16/8.18 sQ16_spl|sQ56_spl|~sQ18_spl|~sQ23_spl|~sQ6_spl|~sQ5_spl),
% 61.16/8.18 inference(split_clause,[status(thm)],[f2050,f217,f2117,f287,f534,f103,f74])).
% 61.16/8.18 fof(f2423,plain,(
% 61.16/8.18 $false|~sQ56_spl),
% 61.16/8.18 inference(backward_subsumption_resolution,[status(thm)],[f7,f2118])).
% 61.16/8.18 fof(f2513,plain,(
% 61.16/8.18 ~sQ56_spl),
% 61.16/8.18 inference(contradiction_clause,[status(thm)],[f2423])).
% 61.16/8.18 fof(f2514,plain,(
% 61.16/8.18 $false),
% 61.16/8.18 inference(sat_refutation,[status(thm)],[f53,f77,f82,f106,f128,f132,f187,f205,f290,f346,f537,f2120,f2513])).
% 61.16/8.18 % SZS output end CNFRefutation for theBenchmark.p
% 13.85/8.28 % Elapsed time: 7.877905 seconds
% 13.85/8.28 % CPU time: 61.905964 seconds
% 13.85/8.28 % Total memory used: 542.531 MB
% 13.85/8.28 % Net memory used: 501.528 MB
%------------------------------------------------------------------------------