%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL005-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 : n011.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:11 PM UTC 2026
% Result : Unsatisfiable 14.25s 2.43s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL005-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n011.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 23:59:40 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 14.25/2.43 % Refutation found
% 14.25/2.43 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 14.25/2.43 % SZS output start CNFRefutation for theBenchmark
% 14.25/2.43 fof(f1,axiom,(
% 14.25/2.43 (![X,Y]: (( ~ is_a_theorem(or(not(X),Y))| ~ is_a_theorem(X)| is_a_theorem(Y) ) ))),
% 14.25/2.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.25/2.43 fof(f2,axiom,(
% 14.25/2.43 (![X,Y,Z,U,V]: (is_a_theorem(or(not(or(not(or(not(X),Y)),or(Z,or(U,V)))),or(not(or(not(U),X)),or(Z,or(V,X))))) ))),
% 14.25/2.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.25/2.43 fof(f3,negated_conjecture,(
% 14.25/2.43 ~ is_a_theorem(or(not(or(a,a)),a)) ),
% 14.25/2.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 14.25/2.43 fof(f4,plain,(
% 14.25/2.43 ![Y]: ((![X]: (~is_a_theorem(or(not(X),Y))|~is_a_theorem(X)))|is_a_theorem(Y))),
% 14.25/2.43 inference(miniscoping,[status(thm)],[f1])).
% 14.25/2.43 fof(f5,plain,(
% 14.25/2.43 ![X0,X1]: (~is_a_theorem(or(not(X0),X1))|~is_a_theorem(X0)|is_a_theorem(X1))),
% 14.25/2.43 inference(cnf_transformation,[status(thm)],[f4])).
% 14.25/2.43 fof(f6,plain,(
% 14.25/2.43 ![X0,X1,X2,X3,X4]: (is_a_theorem(or(not(or(not(or(not(X0),X1)),or(X2,or(X3,X4)))),or(not(or(not(X3),X0)),or(X2,or(X4,X0))))))),
% 14.25/2.43 inference(cnf_transformation,[status(thm)],[f2])).
% 14.25/2.43 fof(f7,plain,(
% 14.25/2.43 ~is_a_theorem(or(not(or(a,a)),a))),
% 14.25/2.43 inference(cnf_transformation,[status(thm)],[f3])).
% 14.25/2.43 fof(f8,plain,(
% 14.25/2.43 ![X0,X1,X2,X3,X4]: (~is_a_theorem(or(not(or(not(X0),X1)),or(X2,or(X3,X4))))|is_a_theorem(or(not(or(not(X3),X0)),or(X2,or(X4,X0)))))),
% 14.25/2.43 inference(resolution,[status(thm)],[f6,f5])).
% 14.25/2.43 fof(f9,plain,(
% 14.25/2.43 ![X0,X1,X2,X3,X4]: (~is_a_theorem(or(not(or(not(X0),X1)),or(X2,or(X3,X4))))|~is_a_theorem(or(not(X3),X0))|is_a_theorem(or(X2,or(X4,X0))))),
% 14.25/2.43 inference(resolution,[status(thm)],[f8,f5])).
% 14.25/2.43 fof(f10,plain,(
% 14.25/2.43 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~is_a_theorem(or(not(or(not(or(not(or(not(X0),X1)),or(X2,or(X3,X1)))),X4)),or(X5,or(or(not(or(not(X1),X6)),or(X2,or(X0,X3))),X7))))|is_a_theorem(or(X5,or(X7,or(not(or(not(X0),X1)),or(X2,or(X3,X1)))))))),
% 14.25/2.43 inference(resolution,[status(thm)],[f9,f6])).
% 14.25/2.43 fof(f11,plain,(
% 14.25/2.43 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~is_a_theorem(or(not(or(not(or(X0,or(X1,X2))),X3)),or(X4,or(or(not(X5),X2),X6))))|is_a_theorem(or(X4,or(X6,or(X0,or(X1,X2)))))|~is_a_theorem(or(not(or(not(X2),X7)),or(X0,or(X5,X1)))))),
% 14.25/2.43 inference(resolution,[status(thm)],[f9,f8])).
% 14.25/2.43 fof(f13,plain,(
% 14.25/2.43 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~is_a_theorem(or(not(or(not(or(X0,or(X1,X2))),X3)),or(X4,or(or(not(X5),X2),X6))))|is_a_theorem(or(X4,or(X6,or(X0,or(X1,X2)))))|~is_a_theorem(or(not(or(not(X1),X7)),or(X0,or(X2,X5)))))),
% 14.25/2.43 inference(resolution,[status(thm)],[f11,f8])).
% 14.25/2.43 fof(f14,plain,(
% 14.25/2.43 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~is_a_theorem(or(not(or(not(or(not(or(not(X0),X1)),or(or(not(X1),X2),X3))),X4)),or(X5,or(or(not(or(X6,X1)),X3),X7))))|is_a_theorem(or(X5,or(X7,or(not(or(not(X0),X1)),or(or(not(X1),X2),X3))))))),
% 14.25/2.43 inference(resolution,[status(thm)],[f13,f6])).
% 14.25/2.43 fof(f19,plain,(
% 14.25/2.43 ![X0,X1,X2,X3,X4,X5,X6,X7]: (is_a_theorem(or(X0,or(X1,or(not(or(not(X2),X3)),or(or(not(X3),X4),X5)))))|~is_a_theorem(or(not(or(not(X1),X6)),or(X0,or(or(not(or(not(X2),X3)),or(or(not(X3),X4),X5)),or(not(or(X7,X3)),X5))))))),
% 14.25/2.43 inference(resolution,[status(thm)],[f14,f8])).
% 14.25/2.43 fof(f21,plain,(
% 14.25/2.43 ![X0,X1,X2,X3,X4,X5,X6,X7]: (is_a_theorem(or(X0,or(X1,or(not(or(not(X2),X3)),or(X4,or(X5,X3))))))|~is_a_theorem(or(not(or(not(X1),X6)),or(X0,or(or(not(or(not(X2),X3)),or(X4,or(X5,X3))),or(not(or(not(X3),X7)),or(X4,or(X2,X5))))))))),
% 14.25/2.43 inference(resolution,[status(thm)],[f10,f8])).
% 14.25/2.43 fof(f40,plain,(
% 14.25/2.43 ![X0,X1,X2,X3,X4,X5,X6,X7]: (is_a_theorem(or(X0,or(X1,or(not(or(not(X2),X3)),or(or(not(X3),X4),X5)))))|~is_a_theorem(or(not(or(not(or(not(or(X6,X3)),X5)),X7)),or(X0,or(X1,or(not(or(not(X2),X3)),or(or(not(X3),X4),X5)))))))),
% 14.25/2.43 inference(resolution,[status(thm)],[f19,f8])).
% 14.25/2.43 fof(f46,plain,(
% 14.25/2.43 ![X0,X1,X2,X3,X4,X5]: (is_a_theorem(or(not(or(not(X0),or(X1,or(X2,X3)))),or(or(not(or(X1,or(X2,X3))),X4),or(not(or(not(X2),X5)),or(X1,or(X3,X5)))))))),
% 14.25/2.43 inference(resolution,[status(thm)],[f21,f6])).
% 14.25/2.43 fof(f53,plain,(
% 14.25/2.43 ![X0,X1,X2,X3,X4]: (is_a_theorem(or(not(or(not(X0),or(or(not(X1),X2),X1))),or(X3,or(not(or(not(X4),X1)),or(or(not(X1),X2),X1))))))),
% 14.25/2.43 inference(resolution,[status(thm)],[f40,f6])).
% 14.25/2.43 fof(f55,plain,(
% 14.25/2.43 ![X0,X1,X2,X3,X4,X5]: (is_a_theorem(or(or(not(or(not(or(not(X0),X1)),or(X2,or(not(X1),X3)))),X4),or(not(or(not(X2),X5)),or(not(or(not(X0),X1)),or(or(not(X1),X3),X5))))))),
% 14.25/2.43 inference(resolution,[status(thm)],[f40,f46])).
% 14.25/2.43 fof(f62,plain,(
% 14.25/2.43 ![X0,X1,X2,X3,X4]: (~is_a_theorem(or(not(X0),or(or(not(X1),X2),X1)))|is_a_theorem(or(X3,or(not(or(not(X4),X1)),or(or(not(X1),X2),X1)))))),
% 14.25/2.43 inference(resolution,[status(thm)],[f53,f5])).
% 14.25/2.43 fof(f81,definition,(
% 14.25/2.43 ![X0]: (sQ0_spl <=> (~is_a_theorem(X0)))),
% 14.25/2.43 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 14.25/2.43 fof(f82,plain,(
% 14.25/2.43 ![X0]: (~is_a_theorem(X0)|~sQ0_spl)),
% 14.25/2.43 inference(component_clause,[status(thm)],[f81])).
% 14.25/2.43 fof(f88,plain,(
% 14.25/2.43 $false|~sQ0_spl),
% 14.25/2.43 inference(backward_subsumption_resolution,[status(thm)],[f55,f82])).
% 14.25/2.43 fof(f98,plain,(
% 14.25/2.43 ~sQ0_spl),
% 14.25/2.43 inference(contradiction_clause,[status(thm)],[f88])).
% 14.25/2.43 fof(f103,plain,(
% 14.25/2.43 ![X0,X1,X2,X3,X4]: (is_a_theorem(or(not(or(not(X0),or(not(X1),X2))),or(not(or(not(X3),X1)),or(or(X4,X1),or(not(X1),X2))))))),
% 14.25/2.44 inference(resolution,[status(thm)],[f6,f8])).
% 14.25/2.44 fof(f111,plain,(
% 14.25/2.44 ![X0,X1,X2,X3,X4]: (is_a_theorem(or(not(or(not(or(X0,X1)),X2)),or(not(or(not(X3),X1)),or(or(not(X1),X4),X2)))))),
% 14.25/2.44 inference(resolution,[status(thm)],[f103,f8])).
% 14.25/2.44 fof(f115,plain,(
% 14.25/2.44 ![X0,X1,X2,X3,X4]: (is_a_theorem(or(not(or(not(or(not(X0),X1)),or(X2,X0))),or(not(or(not(X3),X0)),or(X4,or(X2,X0))))))),
% 14.25/2.44 inference(resolution,[status(thm)],[f111,f8])).
% 14.25/2.44 fof(f117,plain,(
% 14.25/2.44 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~is_a_theorem(or(not(or(not(or(not(or(not(X0),X1)),or(or(not(X1),X2),X3))),X4)),or(X5,or(or(not(or(X6,X1)),X3),X7))))|is_a_theorem(or(X5,or(X7,or(not(or(not(X0),X1)),or(or(not(X1),X2),X3))))))),
% 14.25/2.44 inference(resolution,[status(thm)],[f111,f9])).
% 14.25/2.44 fof(f118,plain,(
% 14.25/2.44 ![X0,X1,X2,X3,X4]: (~is_a_theorem(or(not(or(X0,X1)),X2))|is_a_theorem(or(not(or(not(X3),X1)),or(or(not(X1),X4),X2))))),
% 14.25/2.44 inference(resolution,[status(thm)],[f111,f5])).
% 14.25/2.44 fof(f136,plain,(
% 14.25/2.44 ![X0,X1,X2,X3,X4]: (~is_a_theorem(or(not(or(not(X0),X1)),or(X2,X0)))|is_a_theorem(or(not(or(not(X3),X0)),or(X4,or(X2,X0)))))),
% 14.25/2.44 inference(resolution,[status(thm)],[f115,f5])).
% 14.25/2.44 fof(f144,plain,(
% 14.25/2.44 ![X0,X1,X2,X3,X4]: (is_a_theorem(or(not(or(not(X0),or(not(X1),or(X2,X1)))),or(X3,or(not(or(not(X4),X1)),or(not(X1),or(X2,X1)))))))),
% 14.25/2.44 inference(resolution,[status(thm)],[f10,f111])).
% 14.25/2.44 fof(f159,plain,(
% 14.25/2.44 ![X0,X1,X2,X3,X4]: (is_a_theorem(or(not(or(not(not(or(not(X0),X1))),X2)),or(X3,or(or(or(not(X1),X4),X1),X2)))))),
% 14.25/2.44 inference(resolution,[status(thm)],[f53,f8])).
% 14.25/2.44 fof(f168,plain,(
% 14.25/2.44 ![X0,X1,X2,X3,X4,X5]: (is_a_theorem(or(not(or(not(X0),X1)),or(or(not(X1),X2),or(X3,or(or(or(not(X4),X5),X4),X1))))))),
% 14.25/2.44 inference(resolution,[status(thm)],[f159,f118])).
% 14.25/2.44 fof(f182,plain,(
% 14.25/2.44 ![X0,X1,X2,X3,X4,X5]: (is_a_theorem(or(not(or(not(X0),X1)),or(or(not(X2),X3),or(or(or(or(not(X4),X5),X4),X2),X1)))))),
% 14.25/2.44 inference(resolution,[status(thm)],[f168,f8])).
% 14.25/2.44 fof(f201,plain,(
% 14.25/2.44 ![X0,X1,X2,X3,X4,X5]: (is_a_theorem(or(not(or(not(or(or(or(not(X0),X1),X0),X2)),X3)),or(or(not(X2),X4),or(X5,X3)))))),
% 14.25/2.44 inference(resolution,[status(thm)],[f182,f8])).
% 14.25/2.44 fof(f218,plain,(
% 14.25/2.44 ![X0,X1,X2,X3,X4]: (is_a_theorem(or(X0,or(not(or(not(X1),or(X2,X3))),or(or(not(or(X2,X3)),X4),or(X2,X3))))))),
% 14.25/2.44 inference(resolution,[status(thm)],[f201,f62])).
% 14.25/2.44 fof(f261,plain,(
% 14.25/2.44 ![X0,X1,X2,X3,X4]: (~is_a_theorem(X0)|is_a_theorem(or(not(or(not(X1),or(X2,X3))),or(or(not(or(X2,X3)),X4),or(X2,X3)))))),
% 14.25/2.44 inference(resolution,[status(thm)],[f218,f5])).
% 14.25/2.44 fof(f262,definition,(
% 14.25/2.44 ![X1,X2,X3,X4]: (sQ2_spl <=> (is_a_theorem(or(not(or(not(X1),or(X2,X3))),or(or(not(or(X2,X3)),X4),or(X2,X3))))))),
% 14.25/2.44 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 14.25/2.44 fof(f263,plain,(
% 14.25/2.44 ![X0,X1,X2,X3]: (is_a_theorem(or(not(or(not(X0),or(X1,X2))),or(or(not(or(X1,X2)),X3),or(X1,X2))))|~sQ2_spl)),
% 14.25/2.44 inference(component_clause,[status(thm)],[f262])).
% 14.25/2.44 fof(f265,plain,(
% 14.25/2.44 sQ0_spl|sQ2_spl),
% 14.25/2.44 inference(split_clause,[status(thm)],[f261,f81,f262])).
% 14.25/2.44 fof(f272,plain,(
% 14.25/2.44 ![X0,X1,X2,X3,X4]: (is_a_theorem(or(not(or(not(X0),or(X1,X2))),or(X3,or(or(not(or(X1,X2)),X4),or(X1,X2)))))|~sQ2_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f263,f136])).
% 14.25/2.44 fof(f345,plain,(
% 14.25/2.44 ![X0,X1,X2,X3,X4]: (is_a_theorem(or(not(or(not(or(not(or(X0,X1)),X2)),X3)),or(X4,or(or(X0,X1),X3))))|~sQ2_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f272,f8])).
% 14.25/2.44 fof(f394,plain,(
% 14.25/2.44 ![X0,X1,X2,X3,X4]: (is_a_theorem(or(X0,or(X1,or(not(or(not(or(X2,X3)),X3)),or(or(not(X3),X4),X3)))))|~sQ2_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f345,f117])).
% 14.25/2.44 fof(f483,plain,(
% 14.25/2.44 ![X0,X1,X2,X3,X4]: (~is_a_theorem(X0)|is_a_theorem(or(X1,or(not(or(not(or(X2,X3)),X3)),or(or(not(X3),X4),X3))))|~sQ2_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f394,f5])).
% 14.25/2.44 fof(f484,definition,(
% 14.25/2.44 ![X1,X2,X3,X4]: (sQ6_spl <=> (is_a_theorem(or(X1,or(not(or(not(or(X2,X3)),X3)),or(or(not(X3),X4),X3))))))),
% 14.25/2.44 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 14.25/2.44 fof(f485,plain,(
% 14.25/2.44 ![X0,X1,X2,X3]: (is_a_theorem(or(X0,or(not(or(not(or(X1,X2)),X2)),or(or(not(X2),X3),X2))))|~sQ6_spl)),
% 14.25/2.44 inference(component_clause,[status(thm)],[f484])).
% 14.25/2.44 fof(f487,plain,(
% 14.25/2.44 sQ0_spl|sQ6_spl|~sQ2_spl),
% 14.25/2.44 inference(split_clause,[status(thm)],[f483,f81,f484,f262])).
% 14.25/2.44 fof(f511,plain,(
% 14.25/2.44 ![X0,X1,X2,X3]: (~is_a_theorem(X0)|is_a_theorem(or(not(or(not(or(X1,X2)),X2)),or(or(not(X2),X3),X2)))|~sQ6_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f485,f5])).
% 14.25/2.44 fof(f512,definition,(
% 14.25/2.44 ![X1,X2,X3]: (sQ7_spl <=> (is_a_theorem(or(not(or(not(or(X1,X2)),X2)),or(or(not(X2),X3),X2)))))),
% 14.25/2.44 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 14.25/2.44 fof(f513,plain,(
% 14.25/2.44 ![X0,X1,X2]: (is_a_theorem(or(not(or(not(or(X0,X1)),X1)),or(or(not(X1),X2),X1)))|~sQ7_spl)),
% 14.25/2.44 inference(component_clause,[status(thm)],[f512])).
% 14.25/2.44 fof(f515,plain,(
% 14.25/2.44 sQ0_spl|sQ7_spl|~sQ6_spl),
% 14.25/2.44 inference(split_clause,[status(thm)],[f511,f81,f512,f484])).
% 14.25/2.44 fof(f522,plain,(
% 14.25/2.44 ![X0,X1,X2,X3]: (is_a_theorem(or(X0,or(not(or(not(X1),X2)),or(or(not(X2),X3),X2))))|~sQ7_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f513,f62])).
% 14.25/2.44 fof(f541,plain,(
% 14.25/2.44 ![X0,X1,X2,X3]: (~is_a_theorem(X0)|is_a_theorem(or(not(or(not(X1),X2)),or(or(not(X2),X3),X2)))|~sQ7_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f522,f5])).
% 14.25/2.44 fof(f542,definition,(
% 14.25/2.44 ![X1,X2,X3]: (sQ8_spl <=> (is_a_theorem(or(not(or(not(X1),X2)),or(or(not(X2),X3),X2)))))),
% 14.25/2.44 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 14.25/2.44 fof(f543,plain,(
% 14.25/2.44 ![X0,X1,X2]: (is_a_theorem(or(not(or(not(X0),X1)),or(or(not(X1),X2),X1)))|~sQ8_spl)),
% 14.25/2.44 inference(component_clause,[status(thm)],[f542])).
% 14.25/2.44 fof(f545,plain,(
% 14.25/2.44 sQ0_spl|sQ8_spl|~sQ7_spl),
% 14.25/2.44 inference(split_clause,[status(thm)],[f541,f81,f542,f512])).
% 14.25/2.44 fof(f555,plain,(
% 14.25/2.44 ![X0,X1,X2,X3]: (is_a_theorem(or(not(or(not(X0),X1)),or(X2,or(or(not(X1),X3),X1))))|~sQ8_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f543,f136])).
% 14.25/2.44 fof(f574,plain,(
% 14.25/2.44 ![X0,X1,X2,X3]: (is_a_theorem(or(not(or(not(or(not(X0),X1)),X2)),or(X3,or(X0,X2))))|~sQ8_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f555,f8])).
% 14.25/2.44 fof(f612,plain,(
% 14.25/2.44 ![X0,X1,X2,X3]: (~is_a_theorem(or(not(or(not(X0),X1)),X2))|is_a_theorem(or(X3,or(X0,X2)))|~sQ8_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f574,f5])).
% 14.25/2.44 fof(f637,plain,(
% 14.25/2.44 ![X0,X1,X2,X3]: (~is_a_theorem(or(not(or(not(X0),X1)),X2))|~is_a_theorem(X3)|is_a_theorem(or(X0,X2))|~sQ8_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f612,f5])).
% 14.25/2.44 fof(f638,definition,(
% 14.25/2.44 ![X0,X1,X2]: (sQ10_spl <=> (~is_a_theorem(or(not(or(not(X0),X1)),X2))|is_a_theorem(or(X0,X2))))),
% 14.25/2.44 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 14.25/2.44 fof(f639,plain,(
% 14.25/2.44 ![X0,X1,X2]: (~is_a_theorem(or(not(or(not(X0),X1)),X2))|is_a_theorem(or(X0,X2))|~sQ10_spl)),
% 14.25/2.44 inference(component_clause,[status(thm)],[f638])).
% 14.25/2.44 fof(f641,plain,(
% 14.25/2.44 sQ10_spl|sQ0_spl|~sQ8_spl),
% 14.25/2.44 inference(split_clause,[status(thm)],[f637,f638,f81,f542])).
% 14.25/2.44 fof(f652,plain,(
% 14.25/2.44 ![X0,X1,X2,X3,X4]: (is_a_theorem(or(X0,or(X1,or(not(or(not(X2),X3)),or(not(X3),or(X4,X3))))))|~sQ10_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f639,f144])).
% 14.25/2.44 fof(f968,plain,(
% 14.25/2.44 ![X0,X1,X2,X3,X4]: (~is_a_theorem(X0)|is_a_theorem(or(X1,or(not(or(not(X2),X3)),or(not(X3),or(X4,X3)))))|~sQ10_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f652,f5])).
% 14.25/2.44 fof(f969,definition,(
% 14.25/2.44 ![X1,X2,X3,X4]: (sQ19_spl <=> (is_a_theorem(or(X1,or(not(or(not(X2),X3)),or(not(X3),or(X4,X3)))))))),
% 14.25/2.44 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 14.25/2.44 fof(f970,plain,(
% 14.25/2.44 ![X0,X1,X2,X3]: (is_a_theorem(or(X0,or(not(or(not(X1),X2)),or(not(X2),or(X3,X2)))))|~sQ19_spl)),
% 14.25/2.44 inference(component_clause,[status(thm)],[f969])).
% 14.25/2.44 fof(f972,plain,(
% 14.25/2.44 sQ0_spl|sQ19_spl|~sQ10_spl),
% 14.25/2.44 inference(split_clause,[status(thm)],[f968,f81,f969,f638])).
% 14.25/2.44 fof(f982,plain,(
% 14.25/2.44 ![X0,X1,X2,X3]: (~is_a_theorem(X0)|is_a_theorem(or(not(or(not(X1),X2)),or(not(X2),or(X3,X2))))|~sQ19_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f970,f5])).
% 14.25/2.44 fof(f983,definition,(
% 14.25/2.44 ![X1,X2,X3]: (sQ20_spl <=> (is_a_theorem(or(not(or(not(X1),X2)),or(not(X2),or(X3,X2))))))),
% 14.25/2.44 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 14.25/2.44 fof(f984,plain,(
% 14.25/2.44 ![X0,X1,X2]: (is_a_theorem(or(not(or(not(X0),X1)),or(not(X1),or(X2,X1))))|~sQ20_spl)),
% 14.25/2.44 inference(component_clause,[status(thm)],[f983])).
% 14.25/2.44 fof(f986,plain,(
% 14.25/2.44 sQ0_spl|sQ20_spl|~sQ19_spl),
% 14.25/2.44 inference(split_clause,[status(thm)],[f982,f81,f983,f969])).
% 14.25/2.44 fof(f1000,plain,(
% 14.25/2.44 ![X0,X1,X2]: (is_a_theorem(or(X0,or(not(X1),or(X2,X1))))|~sQ20_spl|~sQ10_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f984,f639])).
% 14.25/2.44 fof(f1024,plain,(
% 14.25/2.44 ![X0,X1,X2]: (~is_a_theorem(X0)|is_a_theorem(or(not(X1),or(X2,X1)))|~sQ20_spl|~sQ10_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f1000,f5])).
% 14.25/2.44 fof(f1025,definition,(
% 14.25/2.44 ![X1,X2]: (sQ21_spl <=> (is_a_theorem(or(not(X1),or(X2,X1)))))),
% 14.25/2.44 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 14.25/2.44 fof(f1026,plain,(
% 14.25/2.44 ![X0,X1]: (is_a_theorem(or(not(X0),or(X1,X0)))|~sQ21_spl)),
% 14.25/2.44 inference(component_clause,[status(thm)],[f1025])).
% 14.25/2.44 fof(f1028,plain,(
% 14.25/2.44 sQ0_spl|sQ21_spl|~sQ20_spl|~sQ10_spl),
% 14.25/2.44 inference(split_clause,[status(thm)],[f1024,f81,f1025,f983,f638])).
% 14.25/2.44 fof(f1032,plain,(
% 14.25/2.44 ![X0,X1,X2]: (is_a_theorem(or(not(or(not(not(X0)),X0)),or(X1,or(X2,X0))))|~sQ21_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f1026,f8])).
% 14.25/2.44 fof(f1033,plain,(
% 14.25/2.44 ![X0,X1,X2]: (is_a_theorem(or(X0,or(X1,or(not(X0),X2))))|~sQ21_spl|~sQ10_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f1026,f639])).
% 14.25/2.44 fof(f1260,plain,(
% 14.25/2.44 ![X0,X1,X2]: (is_a_theorem(or(not(or(not(X0),not(X1))),or(X2,or(X1,not(X1)))))|~sQ21_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f1032,f8])).
% 14.25/2.44 fof(f1261,plain,(
% 14.25/2.44 ![X0,X1,X2]: (is_a_theorem(or(not(X0),or(X1,or(X2,X0))))|~sQ21_spl|~sQ10_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f1032,f639])).
% 14.25/2.44 fof(f1265,plain,(
% 14.25/2.44 ![X0,X1,X2]: (~is_a_theorem(or(not(not(X0)),X0))|is_a_theorem(or(X1,or(X2,X0)))|~sQ21_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f1032,f5])).
% 14.25/2.44 fof(f1285,plain,(
% 14.25/2.44 ![X0,X1,X2]: (~is_a_theorem(X0)|is_a_theorem(or(X1,or(X2,X0)))|~sQ21_spl|~sQ10_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f1261,f5])).
% 14.25/2.44 fof(f2004,plain,(
% 14.25/2.44 ![X0,X1,X2]: (is_a_theorem(or(X0,or(X1,or(X2,not(X2)))))|~sQ21_spl|~sQ10_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f1260,f639])).
% 14.25/2.44 fof(f2010,plain,(
% 14.25/2.44 ![X0,X1,X2,X3]: (is_a_theorem(or(X0,or(X1,or(X2,or(X3,not(X3))))))|~sQ10_spl|~sQ21_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f2004,f1265])).
% 14.25/2.44 fof(f2028,plain,(
% 14.25/2.44 ![X0,X1,X2]: (~is_a_theorem(X0)|is_a_theorem(or(X1,or(X2,not(X2))))|~sQ21_spl|~sQ10_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f2004,f5])).
% 14.25/2.44 fof(f2029,definition,(
% 14.25/2.44 ![X1,X2]: (sQ51_spl <=> (is_a_theorem(or(X1,or(X2,not(X2))))))),
% 14.25/2.44 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 14.25/2.44 fof(f2030,plain,(
% 14.25/2.44 ![X0,X1]: (is_a_theorem(or(X0,or(X1,not(X1))))|~sQ51_spl)),
% 14.25/2.44 inference(component_clause,[status(thm)],[f2029])).
% 14.25/2.44 fof(f2032,plain,(
% 14.25/2.44 sQ0_spl|sQ51_spl|~sQ21_spl|~sQ10_spl),
% 14.25/2.44 inference(split_clause,[status(thm)],[f2028,f81,f2029,f1025,f638])).
% 14.25/2.44 fof(f2041,plain,(
% 14.25/2.44 ![X0,X1]: (~is_a_theorem(X0)|is_a_theorem(or(X1,not(X1)))|~sQ51_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f2030,f5])).
% 14.25/2.44 fof(f2042,definition,(
% 14.25/2.44 ![X1]: (sQ52_spl <=> (is_a_theorem(or(X1,not(X1)))))),
% 14.25/2.44 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 14.25/2.44 fof(f2043,plain,(
% 14.25/2.44 ![X0]: (is_a_theorem(or(X0,not(X0)))|~sQ52_spl)),
% 14.25/2.44 inference(component_clause,[status(thm)],[f2042])).
% 14.25/2.44 fof(f2045,plain,(
% 14.25/2.44 sQ0_spl|sQ52_spl|~sQ51_spl),
% 14.25/2.44 inference(split_clause,[status(thm)],[f2041,f81,f2042,f2029])).
% 14.25/2.44 fof(f2048,plain,(
% 14.25/2.44 ![X0,X1]: (is_a_theorem(or(X0,not(not(or(not(X0),X1)))))|~sQ52_spl|~sQ10_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f2043,f639])).
% 14.25/2.44 fof(f2377,plain,(
% 14.25/2.44 ![X0,X1,X2,X3,X4]: (~is_a_theorem(or(not(X0),X1))|is_a_theorem(or(X2,or(X3,X1)))|~is_a_theorem(or(not(or(not(X3),X4)),or(X2,or(X1,X0)))))),
% 14.25/2.44 inference(resolution,[status(thm)],[f9,f8])).
% 14.25/2.44 fof(f2384,plain,(
% 14.25/2.44 ![X0,X1,X2,X3]: (~is_a_theorem(or(not(X0),X1))|is_a_theorem(or(X2,or(X3,X1)))|~is_a_theorem(or(X0,X3))|~sQ21_spl|~sQ10_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f9,f1285])).
% 14.25/2.44 fof(f2528,plain,(
% 14.25/2.44 ![X0,X1,X2]: (~is_a_theorem(or(not(not(X0)),X0))|~is_a_theorem(X1)|is_a_theorem(or(X2,X0))|~sQ21_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f1265,f5])).
% 14.25/2.44 fof(f2529,definition,(
% 14.25/2.44 ![X0,X2]: (sQ64_spl <=> (~is_a_theorem(or(not(not(X0)),X0))|is_a_theorem(or(X2,X0))))),
% 14.25/2.44 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 14.25/2.44 fof(f2530,plain,(
% 14.25/2.44 ![X0,X1]: (~is_a_theorem(or(not(not(X0)),X0))|is_a_theorem(or(X1,X0))|~sQ64_spl)),
% 14.25/2.44 inference(component_clause,[status(thm)],[f2529])).
% 14.25/2.44 fof(f2532,plain,(
% 14.25/2.44 sQ64_spl|sQ0_spl|~sQ21_spl),
% 14.25/2.44 inference(split_clause,[status(thm)],[f2528,f2529,f81,f1025])).
% 14.25/2.44 fof(f2539,plain,(
% 14.25/2.44 ![X0,X1]: (~is_a_theorem(or(not(not(X0)),X0))|~is_a_theorem(X1)|is_a_theorem(X0)|~sQ64_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f2530,f5])).
% 14.25/2.44 fof(f2544,definition,(
% 14.25/2.44 ![X0]: (sQ66_spl <=> (~is_a_theorem(or(not(not(X0)),X0))|is_a_theorem(X0)))),
% 14.25/2.44 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 14.25/2.44 fof(f2545,plain,(
% 14.25/2.44 ![X0]: (~is_a_theorem(or(not(not(X0)),X0))|is_a_theorem(X0)|~sQ66_spl)),
% 14.25/2.44 inference(component_clause,[status(thm)],[f2544])).
% 14.25/2.44 fof(f2547,plain,(
% 14.25/2.44 sQ66_spl|sQ0_spl|~sQ64_spl),
% 14.25/2.44 inference(split_clause,[status(thm)],[f2539,f2544,f81,f2529])).
% 14.25/2.44 fof(f2597,plain,(
% 14.25/2.44 ![X0,X1,X2,X3]: (~is_a_theorem(or(not(or(X0,not(X0))),X1))|is_a_theorem(or(X2,or(X3,X1)))|~sQ10_spl|~sQ21_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f2377,f2010])).
% 14.25/2.44 fof(f3086,plain,(
% 14.25/2.44 ![X0,X1,X2]: (~is_a_theorem(or(not(or(X0,not(X0))),X1))|is_a_theorem(or(X2,X1))|~sQ10_spl|~sQ21_spl|~sQ66_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f2597,f2545])).
% 14.25/2.44 fof(f3103,plain,(
% 14.25/2.44 ![X0,X1]: (~is_a_theorem(or(not(or(X0,not(X0))),X1))|is_a_theorem(X1)|~sQ10_spl|~sQ21_spl|~sQ66_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f3086,f2545])).
% 14.25/2.44 fof(f3214,plain,(
% 14.25/2.44 ![X0,X1,X2]: (is_a_theorem(or(X0,or(not(not(or(X1,not(X1)))),X2)))|~sQ66_spl|~sQ21_spl|~sQ10_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f3103,f1033])).
% 14.25/2.44 fof(f3289,plain,(
% 14.25/2.44 ![X0,X1]: (is_a_theorem(or(not(not(or(X0,not(X0)))),X1))|~sQ21_spl|~sQ10_spl|~sQ66_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f3214,f2545])).
% 14.25/2.44 fof(f3557,plain,(
% 14.25/2.44 ![X0,X1,X2]: (~is_a_theorem(or(not(X0),X1))|~is_a_theorem(or(X0,X2))|is_a_theorem(or(X2,X1))|~sQ21_spl|~sQ10_spl|~sQ66_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f2384,f2545])).
% 14.25/2.44 fof(f3590,plain,(
% 14.25/2.44 ![X0,X1]: (~is_a_theorem(or(not(X0),X1))|~is_a_theorem(or(X0,not(not(X1))))|is_a_theorem(X1)|~sQ21_spl|~sQ10_spl|~sQ66_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f3557,f2545])).
% 14.25/2.44 fof(f3846,plain,(
% 14.25/2.44 ![X0,X1]: (~is_a_theorem(or(not(not(not(or(X0,not(X0))))),X1))|is_a_theorem(X1)|~sQ21_spl|~sQ10_spl|~sQ66_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f3590,f3289])).
% 14.25/2.44 fof(f3851,plain,(
% 14.25/2.44 ![X0,X1]: (~is_a_theorem(or(not(X0),or(not(X0),X1)))|is_a_theorem(or(not(X0),X1))|~sQ21_spl|~sQ66_spl|~sQ52_spl|~sQ10_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f3590,f2048])).
% 14.25/2.44 fof(f4593,plain,(
% 14.25/2.44 ![X0,X1]: (is_a_theorem(or(not(or(not(not(X0)),X0)),or(X1,X0)))|~sQ66_spl|~sQ52_spl|~sQ10_spl|~sQ21_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f3851,f1032])).
% 14.25/2.44 fof(f4603,plain,(
% 14.25/2.44 ![X0]: (is_a_theorem(or(not(X0),X0))|~sQ66_spl|~sQ52_spl|~sQ10_spl|~sQ21_spl)),
% 14.25/2.44 inference(resolution,[status(thm)],[f3851,f1026])).
% 14.69/2.46 fof(f4811,plain,(
% 14.69/2.46 ![X0,X1,X2]: (~is_a_theorem(or(not(X0),X1))|is_a_theorem(or(X2,or(not(or(X1,X0)),X1)))|~sQ66_spl|~sQ52_spl|~sQ10_spl|~sQ21_spl)),
% 14.69/2.46 inference(resolution,[status(thm)],[f4593,f2377])).
% 14.69/2.46 fof(f6444,plain,(
% 14.69/2.46 ![X0,X1]: (~is_a_theorem(or(not(X0),X1))|is_a_theorem(or(not(or(X1,X0)),X1))|~sQ52_spl|~sQ21_spl|~sQ10_spl|~sQ66_spl)),
% 14.69/2.46 inference(resolution,[status(thm)],[f4811,f3846])).
% 14.69/2.46 fof(f6479,plain,(
% 14.69/2.46 ~is_a_theorem(or(not(a),a))|~sQ52_spl|~sQ21_spl|~sQ10_spl|~sQ66_spl),
% 14.69/2.46 inference(resolution,[status(thm)],[f6444,f7])).
% 14.69/2.46 fof(f6508,plain,(
% 14.69/2.46 $false|~sQ52_spl|~sQ21_spl|~sQ10_spl|~sQ66_spl),
% 14.69/2.46 inference(forward_subsumption_resolution,[status(thm)],[f6479,f4603])).
% 14.69/2.46 fof(f6509,plain,(
% 14.69/2.46 ~sQ52_spl|~sQ21_spl|~sQ10_spl|~sQ66_spl),
% 14.69/2.46 inference(contradiction_clause,[status(thm)],[f6508])).
% 14.69/2.46 fof(f6510,plain,(
% 14.69/2.46 $false),
% 14.69/2.46 inference(sat_refutation,[status(thm)],[f98,f265,f487,f515,f545,f641,f972,f986,f1028,f2032,f2045,f2532,f2547,f6509])).
% 14.69/2.46 % SZS output end CNFRefutation for theBenchmark.p
% 14.69/2.48 % Elapsed time: 2.103079 seconds
% 14.69/2.48 % CPU time: 16.339777 seconds
% 14.69/2.48 % Total memory used: 289.408 MB
% 14.69/2.48 % Net memory used: 269.078 MB
%------------------------------------------------------------------------------