%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL093-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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:20 PM UTC 2026
% Result : Unsatisfiable 82.64s 10.89s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL093-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n007.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 00:02:06 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 82.64/10.89 % Refutation found
% 82.64/10.89 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 82.64/10.89 % SZS output start CNFRefutation for theBenchmark
% 82.64/10.89 fof(f1,axiom,(
% 82.64/10.89 (![X,Y]: (( ~ is_a_theorem(implies(X,Y))| ~ is_a_theorem(X)| is_a_theorem(Y) ) ))),
% 82.64/10.89 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 82.64/10.89 fof(f2,axiom,(
% 82.64/10.89 (![P,Q,R,S,T]: (is_a_theorem(implies(implies(implies(P,Q),implies(R,S)),implies(implies(S,P),implies(T,implies(R,P))))) ))),
% 82.64/10.89 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 82.64/10.89 fof(f3,negated_conjecture,(
% 82.64/10.89 ~ is_a_theorem(implies(implies(a,b),implies(implies(b,c),implies(a,c)))) ),
% 82.64/10.89 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 82.64/10.89 fof(f4,plain,(
% 82.64/10.89 ![Y]: ((![X]: (~is_a_theorem(implies(X,Y))|~is_a_theorem(X)))|is_a_theorem(Y))),
% 82.64/10.89 inference(miniscoping,[status(thm)],[f1])).
% 82.64/10.89 fof(f5,plain,(
% 82.64/10.89 ![X0,X1]: (~is_a_theorem(implies(X0,X1))|~is_a_theorem(X0)|is_a_theorem(X1))),
% 82.64/10.89 inference(cnf_transformation,[status(thm)],[f4])).
% 82.64/10.89 fof(f6,plain,(
% 82.64/10.89 ![X0,X1,X2,X3,X4]: (is_a_theorem(implies(implies(implies(X0,X1),implies(X2,X3)),implies(implies(X3,X0),implies(X4,implies(X2,X0))))))),
% 82.64/10.89 inference(cnf_transformation,[status(thm)],[f2])).
% 82.64/10.89 fof(f7,plain,(
% 82.64/10.89 ~is_a_theorem(implies(implies(a,b),implies(implies(b,c),implies(a,c))))),
% 82.64/10.89 inference(cnf_transformation,[status(thm)],[f3])).
% 82.64/10.89 fof(f8,plain,(
% 82.64/10.89 ![X0,X1,X2,X3,X4]: (~is_a_theorem(implies(implies(X0,X1),implies(X2,X3)))|is_a_theorem(implies(implies(X3,X0),implies(X4,implies(X2,X0)))))),
% 82.64/10.89 inference(resolution,[status(thm)],[f6,f5])).
% 82.64/10.89 fof(f9,plain,(
% 82.64/10.89 ![X0,X1,X2,X3,X4]: (~is_a_theorem(implies(implies(X0,X1),implies(X2,X3)))|~is_a_theorem(implies(X3,X0))|is_a_theorem(implies(X4,implies(X2,X0))))),
% 82.64/10.89 inference(resolution,[status(thm)],[f8,f5])).
% 82.64/10.89 fof(f10,plain,(
% 82.64/10.89 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~is_a_theorem(implies(implies(implies(implies(X0,X1),implies(X2,implies(X3,X1))),X4),implies(X5,implies(implies(X1,X6),implies(X3,X0)))))|is_a_theorem(implies(X7,implies(X5,implies(implies(X0,X1),implies(X2,implies(X3,X1)))))))),
% 82.64/10.89 inference(resolution,[status(thm)],[f9,f6])).
% 82.64/10.89 fof(f11,plain,(
% 82.64/10.89 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~is_a_theorem(implies(implies(implies(X0,implies(X1,X2)),X3),implies(X4,implies(X5,X2))))|is_a_theorem(implies(X6,implies(X4,implies(X0,implies(X1,X2)))))|~is_a_theorem(implies(implies(X2,X7),implies(X1,X5))))),
% 82.64/10.89 inference(resolution,[status(thm)],[f9,f8])).
% 82.64/10.89 fof(f12,plain,(
% 82.64/10.89 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~is_a_theorem(implies(implies(implies(X0,implies(implies(X1,X2),implies(X2,X3))),X4),implies(X5,implies(implies(X6,implies(X7,X2)),implies(X2,X3)))))|is_a_theorem(implies(X8,implies(X5,implies(X0,implies(implies(X1,X2),implies(X2,X3)))))))),
% 82.64/10.89 inference(resolution,[status(thm)],[f11,f6])).
% 82.64/10.89 fof(f16,plain,(
% 82.64/10.89 ![X0,X1,X2,X3,X4,X5,X6,X7]: (is_a_theorem(implies(X0,implies(X1,implies(implies(X2,X3),implies(X4,implies(X5,X3))))))|~is_a_theorem(implies(implies(implies(X5,X2),X6),implies(implies(X3,X7),implies(implies(X2,X3),implies(X4,implies(X5,X3)))))))),
% 82.64/10.89 inference(resolution,[status(thm)],[f10,f8])).
% 82.64/10.89 fof(f17,plain,(
% 82.64/10.89 ![X0,X1,X2,X3,X4]: (is_a_theorem(implies(X0,implies(implies(X1,X2),implies(X2,implies(implies(X3,X4),implies(X4,X2)))))))),
% 82.64/10.89 inference(resolution,[status(thm)],[f12,f6])).
% 82.64/10.89 fof(f24,plain,(
% 82.64/10.89 ![X0,X1,X2,X3,X4]: (~is_a_theorem(X0)|is_a_theorem(implies(implies(X1,X2),implies(X2,implies(implies(X3,X4),implies(X4,X2))))))),
% 82.64/10.89 inference(resolution,[status(thm)],[f17,f5])).
% 82.64/10.89 fof(f25,definition,(
% 82.64/10.89 ![X0]: (sQ0_spl <=> (~is_a_theorem(X0)))),
% 82.64/10.89 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 82.64/10.89 fof(f26,plain,(
% 82.64/10.89 ![X0]: (~is_a_theorem(X0)|~sQ0_spl)),
% 82.64/10.89 inference(component_clause,[status(thm)],[f25])).
% 82.64/10.89 fof(f28,definition,(
% 82.64/10.89 ![X1,X2,X3,X4]: (sQ1_spl <=> (is_a_theorem(implies(implies(X1,X2),implies(X2,implies(implies(X3,X4),implies(X4,X2)))))))),
% 82.64/10.89 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 82.64/10.89 fof(f29,plain,(
% 82.64/10.89 ![X0,X1,X2,X3]: (is_a_theorem(implies(implies(X0,X1),implies(X1,implies(implies(X2,X3),implies(X3,X1)))))|~sQ1_spl)),
% 82.64/10.89 inference(component_clause,[status(thm)],[f28])).
% 82.64/10.89 fof(f31,plain,(
% 82.64/10.89 sQ0_spl|sQ1_spl),
% 82.64/10.89 inference(split_clause,[status(thm)],[f24,f25,f28])).
% 82.64/10.89 fof(f32,plain,(
% 82.64/10.89 $false|~sQ0_spl),
% 82.64/10.89 inference(backward_subsumption_resolution,[status(thm)],[f6,f26])).
% 82.64/10.89 fof(f34,plain,(
% 82.64/10.89 ~sQ0_spl),
% 82.64/10.89 inference(contradiction_clause,[status(thm)],[f32])).
% 82.64/10.89 fof(f46,plain,(
% 82.64/10.89 ![X0,X1,X2,X3,X4]: (~is_a_theorem(implies(implies(X0,X1),implies(X2,X3)))|~is_a_theorem(implies(X3,X0))|~is_a_theorem(X4)|is_a_theorem(implies(X2,X0)))),
% 82.64/10.89 inference(resolution,[status(thm)],[f9,f5])).
% 82.64/10.89 fof(f47,definition,(
% 82.64/10.89 ![X0,X1,X2,X3]: (sQ2_spl <=> (~is_a_theorem(implies(implies(X0,X1),implies(X2,X3)))|~is_a_theorem(implies(X3,X0))|is_a_theorem(implies(X2,X0))))),
% 82.64/10.89 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 82.64/10.89 fof(f48,plain,(
% 82.64/10.89 ![X0,X1,X2,X3]: (~is_a_theorem(implies(implies(X0,X1),implies(X2,X3)))|~is_a_theorem(implies(X3,X0))|is_a_theorem(implies(X2,X0))|~sQ2_spl)),
% 82.64/10.89 inference(component_clause,[status(thm)],[f47])).
% 82.64/10.89 fof(f50,plain,(
% 82.64/10.89 sQ2_spl|sQ0_spl),
% 82.64/10.89 inference(split_clause,[status(thm)],[f46,f47,f25])).
% 82.64/10.89 fof(f115,plain,(
% 82.64/10.89 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~is_a_theorem(implies(implies(implies(X0,X1),X2),implies(implies(X3,X4),implies(implies(X1,X3),implies(X5,implies(X0,X3))))))|~is_a_theorem(X6)|is_a_theorem(implies(X7,implies(implies(X1,X3),implies(X5,implies(X0,X3))))))),
% 82.64/10.89 inference(resolution,[status(thm)],[f16,f5])).
% 82.64/10.89 fof(f116,definition,(
% 82.64/10.89 ![X0,X1,X2,X3,X4,X5,X7]: (sQ9_spl <=> (~is_a_theorem(implies(implies(implies(X0,X1),X2),implies(implies(X3,X4),implies(implies(X1,X3),implies(X5,implies(X0,X3))))))|is_a_theorem(implies(X7,implies(implies(X1,X3),implies(X5,implies(X0,X3)))))))),
% 82.64/10.89 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 82.64/10.89 fof(f117,plain,(
% 82.64/10.89 ![X0,X1,X2,X3,X4,X5,X6]: (~is_a_theorem(implies(implies(implies(X0,X1),X2),implies(implies(X3,X4),implies(implies(X1,X3),implies(X5,implies(X0,X3))))))|is_a_theorem(implies(X6,implies(implies(X1,X3),implies(X5,implies(X0,X3)))))|~sQ9_spl)),
% 82.64/10.89 inference(component_clause,[status(thm)],[f116])).
% 82.64/10.89 fof(f119,plain,(
% 82.64/10.89 sQ9_spl|sQ0_spl),
% 82.64/10.89 inference(split_clause,[status(thm)],[f115,f116,f25])).
% 82.64/10.89 fof(f283,definition,(
% 82.64/10.89 ![X3,X4]: (sQ26_spl <=> (~is_a_theorem(implies(X3,X4))))),
% 82.64/10.89 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 82.64/10.89 fof(f284,plain,(
% 82.64/10.89 ![X0,X1]: (~is_a_theorem(implies(X0,X1))|~sQ26_spl)),
% 82.64/10.89 inference(component_clause,[status(thm)],[f283])).
% 82.64/10.89 fof(f380,plain,(
% 82.64/10.89 $false|~sQ26_spl),
% 82.64/10.89 inference(backward_subsumption_resolution,[status(thm)],[f6,f284])).
% 82.64/10.89 fof(f388,plain,(
% 82.64/10.89 ~sQ26_spl),
% 82.64/10.89 inference(contradiction_clause,[status(thm)],[f380])).
% 82.64/10.89 fof(f397,plain,(
% 82.64/10.89 ![X0,X1,X2,X3,X4,X5]: (is_a_theorem(implies(implies(implies(X0,implies(X1,X2)),implies(X2,X3)),implies(X4,implies(implies(X5,X2),implies(X2,X3))))))),
% 82.64/10.89 inference(resolution,[status(thm)],[f8,f6])).
% 82.64/10.89 fof(f403,plain,(
% 82.64/10.89 ![X0,X1,X2,X3,X4]: (is_a_theorem(implies(implies(implies(implies(X0,X1),implies(X1,X2)),X3),implies(X4,implies(X2,X3))))|~sQ1_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f29,f8])).
% 82.64/10.89 fof(f422,plain,(
% 82.64/10.89 ![X0,X1,X2,X3,X4,X5]: (~is_a_theorem(implies(implies(X0,implies(X1,X2)),implies(X2,X3)))|is_a_theorem(implies(X4,implies(implies(X5,X2),implies(X2,X3)))))),
% 82.64/10.89 inference(resolution,[status(thm)],[f397,f5])).
% 82.64/10.89 fof(f603,plain,(
% 82.64/10.89 ![X0,X1,X2,X3,X4]: (is_a_theorem(implies(X0,implies(implies(X1,X2),implies(X2,implies(X3,implies(X4,X2))))))|~sQ1_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f422,f403])).
% 82.64/10.89 fof(f922,plain,(
% 82.64/10.89 ![X0,X1,X2,X3,X4]: (~is_a_theorem(X0)|is_a_theorem(implies(implies(X1,X2),implies(X2,implies(X3,implies(X4,X2)))))|~sQ1_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f603,f5])).
% 82.64/10.89 fof(f938,definition,(
% 82.64/10.89 ![X1,X2,X3,X4]: (sQ46_spl <=> (is_a_theorem(implies(implies(X1,X2),implies(X2,implies(X3,implies(X4,X2)))))))),
% 82.64/10.89 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 82.64/10.89 fof(f939,plain,(
% 82.64/10.89 ![X0,X1,X2,X3]: (is_a_theorem(implies(implies(X0,X1),implies(X1,implies(X2,implies(X3,X1)))))|~sQ46_spl)),
% 82.64/10.89 inference(component_clause,[status(thm)],[f938])).
% 82.64/10.89 fof(f941,plain,(
% 82.64/10.89 sQ0_spl|sQ46_spl|~sQ1_spl),
% 82.64/10.89 inference(split_clause,[status(thm)],[f922,f25,f938,f28])).
% 82.64/10.89 fof(f960,plain,(
% 82.64/10.89 ![X0,X1,X2,X3]: (~is_a_theorem(implies(X0,X1))|is_a_theorem(implies(X1,implies(X2,implies(X3,X1))))|~sQ46_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f939,f5])).
% 82.64/10.89 fof(f1481,plain,(
% 82.64/10.89 ![X0,X1,X2,X3]: (is_a_theorem(implies(X0,implies(implies(X1,X2),implies(X3,implies(X2,X2)))))|~sQ9_spl|~sQ46_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f117,f939])).
% 82.64/10.89 fof(f1536,plain,(
% 82.64/10.89 ![X0,X1,X2,X3]: (~is_a_theorem(X0)|is_a_theorem(implies(implies(X1,X2),implies(X3,implies(X2,X2))))|~sQ9_spl|~sQ46_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f1481,f5])).
% 82.64/10.89 fof(f1555,definition,(
% 82.64/10.89 ![X1,X2,X3]: (sQ64_spl <=> (is_a_theorem(implies(implies(X1,X2),implies(X3,implies(X2,X2))))))),
% 82.64/10.89 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 82.64/10.89 fof(f1556,plain,(
% 82.64/10.89 ![X0,X1,X2]: (is_a_theorem(implies(implies(X0,X1),implies(X2,implies(X1,X1))))|~sQ64_spl)),
% 82.64/10.89 inference(component_clause,[status(thm)],[f1555])).
% 82.64/10.89 fof(f1558,plain,(
% 82.64/10.89 sQ0_spl|sQ64_spl|~sQ9_spl|~sQ46_spl),
% 82.64/10.89 inference(split_clause,[status(thm)],[f1536,f25,f1555,f116,f938])).
% 82.64/10.89 fof(f1572,plain,(
% 82.64/10.89 ![X0,X1,X2,X3]: (is_a_theorem(implies(implies(implies(X0,X0),X1),implies(X2,implies(X3,X1))))|~sQ64_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f1556,f8])).
% 82.64/10.89 fof(f1702,plain,(
% 82.64/10.89 ![X0,X1,X2,X3]: (is_a_theorem(implies(X0,implies(implies(X1,X2),implies(X3,implies(X1,X2)))))|~sQ64_spl|~sQ9_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f1572,f117])).
% 82.64/10.89 fof(f1717,plain,(
% 82.64/10.89 ![X0,X1,X2,X3]: (~is_a_theorem(implies(implies(X0,X0),X1))|is_a_theorem(implies(X2,implies(X3,X1)))|~sQ64_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f1572,f5])).
% 82.64/10.89 fof(f1918,plain,(
% 82.64/10.89 ![X0,X1,X2,X3]: (~is_a_theorem(X0)|is_a_theorem(implies(implies(X1,X2),implies(X3,implies(X1,X2))))|~sQ64_spl|~sQ9_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f1702,f5])).
% 82.64/10.89 fof(f1937,definition,(
% 82.64/10.89 ![X1,X2,X3]: (sQ71_spl <=> (is_a_theorem(implies(implies(X1,X2),implies(X3,implies(X1,X2))))))),
% 82.64/10.89 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 82.64/10.89 fof(f1938,plain,(
% 82.64/10.89 ![X0,X1,X2]: (is_a_theorem(implies(implies(X0,X1),implies(X2,implies(X0,X1))))|~sQ71_spl)),
% 82.64/10.89 inference(component_clause,[status(thm)],[f1937])).
% 82.64/10.89 fof(f1940,plain,(
% 82.64/10.89 sQ0_spl|sQ71_spl|~sQ64_spl|~sQ9_spl),
% 82.64/10.89 inference(split_clause,[status(thm)],[f1918,f25,f1937,f1555,f116])).
% 82.64/10.89 fof(f1954,plain,(
% 82.64/10.89 ![X0,X1,X2,X3]: (is_a_theorem(implies(implies(implies(X0,X1),X0),implies(X2,implies(X3,X0))))|~sQ71_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f1938,f8])).
% 82.64/10.89 fof(f2015,plain,(
% 82.64/10.89 ![X0,X1,X2,X3]: (is_a_theorem(implies(X0,implies(X1,implies(X2,implies(X3,X3)))))|~sQ64_spl|~sQ71_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f1717,f1938])).
% 82.64/10.89 fof(f2118,plain,(
% 82.64/10.89 ![X0,X1,X2,X3]: (~is_a_theorem(X0)|is_a_theorem(implies(X1,implies(X2,implies(X3,X3))))|~sQ64_spl|~sQ71_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f2015,f5])).
% 82.64/10.89 fof(f2136,definition,(
% 82.64/10.89 ![X1,X2,X3]: (sQ74_spl <=> (is_a_theorem(implies(X1,implies(X2,implies(X3,X3))))))),
% 82.64/10.89 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 82.64/10.89 fof(f2137,plain,(
% 82.64/10.89 ![X0,X1,X2]: (is_a_theorem(implies(X0,implies(X1,implies(X2,X2))))|~sQ74_spl)),
% 82.64/10.89 inference(component_clause,[status(thm)],[f2136])).
% 82.64/10.89 fof(f2139,plain,(
% 82.64/10.89 sQ0_spl|sQ74_spl|~sQ64_spl|~sQ71_spl),
% 82.64/10.89 inference(split_clause,[status(thm)],[f2118,f25,f2136,f1555,f1937])).
% 82.64/10.89 fof(f2169,plain,(
% 82.64/10.89 ![X0,X1,X2]: (~is_a_theorem(X0)|is_a_theorem(implies(X1,implies(X2,X2)))|~sQ74_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f2137,f5])).
% 82.64/10.89 fof(f2180,definition,(
% 82.64/10.89 ![X1,X2]: (sQ75_spl <=> (is_a_theorem(implies(X1,implies(X2,X2)))))),
% 82.64/10.89 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 82.64/10.89 fof(f2181,plain,(
% 82.64/10.89 ![X0,X1]: (is_a_theorem(implies(X0,implies(X1,X1)))|~sQ75_spl)),
% 82.64/10.89 inference(component_clause,[status(thm)],[f2180])).
% 82.64/10.89 fof(f2183,plain,(
% 82.64/10.89 sQ0_spl|sQ75_spl|~sQ74_spl),
% 82.64/10.89 inference(split_clause,[status(thm)],[f2169,f25,f2180,f2136])).
% 82.64/10.89 fof(f2232,plain,(
% 82.64/10.89 ![X0,X1]: (~is_a_theorem(X0)|is_a_theorem(implies(X1,X1))|~sQ75_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f2181,f5])).
% 82.64/10.89 fof(f2242,definition,(
% 82.64/10.89 ![X1]: (sQ76_spl <=> (is_a_theorem(implies(X1,X1))))),
% 82.64/10.89 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 82.64/10.89 fof(f2243,plain,(
% 82.64/10.89 ![X0]: (is_a_theorem(implies(X0,X0))|~sQ76_spl)),
% 82.64/10.89 inference(component_clause,[status(thm)],[f2242])).
% 82.64/10.89 fof(f2245,plain,(
% 82.64/10.89 sQ0_spl|sQ76_spl|~sQ75_spl),
% 82.64/10.89 inference(split_clause,[status(thm)],[f2232,f25,f2242,f2180])).
% 82.64/10.89 fof(f2277,plain,(
% 82.64/10.89 ![X0,X1,X2]: (is_a_theorem(implies(X0,implies(X1,implies(X2,X0))))|~sQ76_spl|~sQ46_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f2243,f960])).
% 82.64/10.89 fof(f2278,plain,(
% 82.64/10.89 ![X0,X1,X2]: (~is_a_theorem(implies(implies(X0,X1),implies(X2,X0)))|is_a_theorem(implies(X2,X0))|~sQ76_spl|~sQ2_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f2243,f48])).
% 82.64/10.89 fof(f2355,plain,(
% 82.64/10.89 ![X0,X1,X2,X3]: (is_a_theorem(implies(X0,implies(implies(X1,X2),implies(implies(X3,X1),implies(X3,X2)))))|~sQ76_spl|~sQ46_spl|~sQ9_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f2277,f117])).
% 82.64/10.89 fof(f6310,plain,(
% 82.64/10.89 ![X0,X1,X2]: (is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X0),implies(X2,X1))))|~sQ46_spl|~sQ9_spl|~sQ76_spl|~sQ2_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f2355,f2278])).
% 82.64/10.89 fof(f6670,plain,(
% 82.64/10.89 ![X0,X1]: (is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1)))|~sQ46_spl|~sQ9_spl|~sQ76_spl|~sQ2_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f6310,f2278])).
% 82.64/10.89 fof(f6671,plain,(
% 82.64/10.89 ![X0,X1,X2,X3]: (is_a_theorem(implies(implies(implies(X0,X1),X2),implies(X3,implies(implies(X0,X2),X2))))|~sQ46_spl|~sQ9_spl|~sQ76_spl|~sQ2_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f6310,f8])).
% 82.64/10.89 fof(f6682,plain,(
% 82.64/10.89 ![X0,X1,X2]: (~is_a_theorem(implies(X0,X1))|is_a_theorem(implies(implies(X2,X0),implies(X2,X1)))|~sQ46_spl|~sQ9_spl|~sQ76_spl|~sQ2_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f6310,f5])).
% 82.64/10.89 fof(f6750,plain,(
% 82.64/10.89 ![X0,X1]: (~is_a_theorem(implies(X0,implies(X0,X1)))|is_a_theorem(implies(X0,X1))|~sQ46_spl|~sQ9_spl|~sQ76_spl|~sQ2_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f6670,f5])).
% 82.64/10.89 fof(f6768,plain,(
% 82.64/10.89 ![X0,X1,X2]: (is_a_theorem(implies(implies(implies(X0,X1),X0),implies(X2,X0)))|~sQ46_spl|~sQ9_spl|~sQ76_spl|~sQ2_spl|~sQ71_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f6750,f1954])).
% 82.64/10.89 fof(f6926,plain,(
% 82.64/10.89 ![X0,X1]: (is_a_theorem(implies(implies(implies(X0,X1),X0),X0))|~sQ71_spl|~sQ46_spl|~sQ9_spl|~sQ76_spl|~sQ2_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f6768,f6750])).
% 82.64/10.89 fof(f6990,plain,(
% 82.64/10.89 ![X0,X1]: (~is_a_theorem(implies(implies(X0,X1),X0))|is_a_theorem(X0)|~sQ71_spl|~sQ46_spl|~sQ9_spl|~sQ76_spl|~sQ2_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f6926,f5])).
% 82.64/10.89 fof(f16302,plain,(
% 82.64/10.89 ![X0,X1]: (is_a_theorem(implies(X0,implies(implies(X0,X1),X1)))|~sQ71_spl|~sQ46_spl|~sQ9_spl|~sQ76_spl|~sQ2_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f6671,f6990])).
% 82.64/10.89 fof(f16410,plain,(
% 82.64/10.89 ![X0,X1,X2]: (is_a_theorem(implies(implies(X0,X1),implies(X0,implies(implies(X1,X2),X2))))|~sQ71_spl|~sQ46_spl|~sQ9_spl|~sQ76_spl|~sQ2_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f16302,f6682])).
% 82.64/10.89 fof(f16417,plain,(
% 82.64/10.89 ![X0,X1]: (~is_a_theorem(X0)|is_a_theorem(implies(implies(X0,X1),X1))|~sQ71_spl|~sQ46_spl|~sQ9_spl|~sQ76_spl|~sQ2_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f16302,f5])).
% 82.64/10.89 fof(f16511,plain,(
% 82.64/10.89 ![X0,X1,X2]: (is_a_theorem(implies(implies(implies(X0,implies(implies(X0,X1),X1)),X2),X2))|~sQ71_spl|~sQ46_spl|~sQ9_spl|~sQ76_spl|~sQ2_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f16417,f16302])).
% 82.64/10.89 fof(f17660,plain,(
% 82.64/10.89 ![X0,X1,X2]: (~is_a_theorem(implies(X0,X1))|is_a_theorem(implies(X0,implies(implies(X1,X2),X2)))|~sQ71_spl|~sQ46_spl|~sQ9_spl|~sQ76_spl|~sQ2_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f16410,f5])).
% 82.64/10.89 fof(f18244,plain,(
% 82.64/10.89 ![X0,X1,X2]: (~is_a_theorem(implies(implies(X0,implies(implies(X0,X1),X1)),X2))|is_a_theorem(X2)|~sQ71_spl|~sQ46_spl|~sQ9_spl|~sQ76_spl|~sQ2_spl)),
% 82.64/10.89 inference(resolution,[status(thm)],[f16511,f5])).
% 82.64/10.89 fof(f19593,plain,(
% 82.64/10.89 ![X0,X1,X2]: (~is_a_theorem(implies(X0,X1))|~is_a_theorem(X0)|is_a_theorem(implies(implies(X1,X2),X2))|~sQ71_spl|~sQ46_spl|~sQ9_spl|~sQ76_spl|~sQ2_spl)),
% 62.54/10.93 inference(resolution,[status(thm)],[f17660,f5])).
% 62.54/10.93 fof(f20263,plain,(
% 62.54/10.93 ![X0,X1,X2]: (is_a_theorem(implies(X0,implies(implies(implies(implies(X0,X1),X1),X2),X2)))|~sQ71_spl|~sQ46_spl|~sQ9_spl|~sQ76_spl|~sQ2_spl)),
% 62.54/10.93 inference(resolution,[status(thm)],[f18244,f16410])).
% 62.54/10.93 fof(f22365,plain,(
% 62.54/10.93 ![X0,X1,X2]: (~is_a_theorem(X0)|is_a_theorem(implies(implies(implies(implies(X0,X1),X1),X2),X2))|~sQ71_spl|~sQ46_spl|~sQ9_spl|~sQ76_spl|~sQ2_spl)),
% 62.54/10.93 inference(resolution,[status(thm)],[f19593,f16302])).
% 62.54/10.93 fof(f23431,plain,(
% 62.54/10.93 ![X0,X1,X2]: (~is_a_theorem(X0)|~is_a_theorem(implies(implies(implies(X0,X1),X1),X2))|is_a_theorem(X2)|~sQ71_spl|~sQ46_spl|~sQ9_spl|~sQ76_spl|~sQ2_spl)),
% 62.54/10.93 inference(resolution,[status(thm)],[f22365,f5])).
% 62.54/10.93 fof(f23733,plain,(
% 62.54/10.93 ![X0,X1,X2]: (~is_a_theorem(X0)|is_a_theorem(implies(implies(X1,implies(X0,X2)),implies(X1,X2)))|~sQ71_spl|~sQ46_spl|~sQ9_spl|~sQ76_spl|~sQ2_spl)),
% 62.54/10.93 inference(resolution,[status(thm)],[f23431,f6310])).
% 62.54/10.93 fof(f24629,plain,(
% 62.54/10.93 ![X0,X1,X2]: (~is_a_theorem(X0)|~is_a_theorem(implies(X1,implies(X0,X2)))|is_a_theorem(implies(X1,X2))|~sQ71_spl|~sQ46_spl|~sQ9_spl|~sQ76_spl|~sQ2_spl)),
% 62.54/10.93 inference(resolution,[status(thm)],[f23733,f5])).
% 62.54/10.93 fof(f26331,plain,(
% 62.54/10.93 ![X0,X1,X2]: (~is_a_theorem(implies(implies(implies(X0,X1),X1),X2))|is_a_theorem(implies(X0,X2))|~sQ71_spl|~sQ46_spl|~sQ9_spl|~sQ76_spl|~sQ2_spl)),
% 62.54/10.93 inference(resolution,[status(thm)],[f24629,f20263])).
% 62.54/10.93 fof(f28848,plain,(
% 62.54/10.93 ![X0,X1,X2]: (is_a_theorem(implies(X0,implies(implies(X1,implies(X0,X2)),implies(X1,X2))))|~sQ71_spl|~sQ46_spl|~sQ9_spl|~sQ76_spl|~sQ2_spl)),
% 62.54/10.93 inference(resolution,[status(thm)],[f26331,f6310])).
% 62.54/10.93 fof(f30833,plain,(
% 62.54/10.93 ![X0,X1,X2]: (~is_a_theorem(implies(X0,implies(X1,X2)))|is_a_theorem(implies(X1,implies(X0,X2)))|~sQ71_spl|~sQ46_spl|~sQ9_spl|~sQ76_spl|~sQ2_spl)),
% 62.54/10.93 inference(resolution,[status(thm)],[f28848,f24629])).
% 62.54/10.93 fof(f32050,plain,(
% 62.54/10.93 ![X0,X1,X2]: (is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2))))|~sQ71_spl|~sQ46_spl|~sQ9_spl|~sQ76_spl|~sQ2_spl)),
% 62.54/10.93 inference(resolution,[status(thm)],[f30833,f6310])).
% 62.54/10.93 fof(f33544,plain,(
% 62.54/10.93 $false|~sQ71_spl|~sQ46_spl|~sQ9_spl|~sQ76_spl|~sQ2_spl),
% 62.54/10.93 inference(backward_subsumption_resolution,[status(thm)],[f7,f32050])).
% 62.54/10.93 fof(f33665,plain,(
% 62.54/10.93 ~sQ71_spl|~sQ46_spl|~sQ9_spl|~sQ76_spl|~sQ2_spl),
% 62.54/10.93 inference(contradiction_clause,[status(thm)],[f33544])).
% 62.54/10.93 fof(f33666,plain,(
% 62.54/10.93 $false),
% 62.54/10.93 inference(sat_refutation,[status(thm)],[f31,f34,f50,f119,f388,f941,f1558,f1940,f2139,f2183,f2245,f33665])).
% 62.54/10.93 % SZS output end CNFRefutation for theBenchmark.p
% 62.54/10.98 % Elapsed time: 10.603639 seconds
% 62.54/10.98 % CPU time: 83.831946 seconds
% 62.54/10.98 % Total memory used: 607.058 MB
% 62.54/10.98 % Net memory used: 545.609 MB
%------------------------------------------------------------------------------