%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG012-1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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 11:49:27 AM UTC 2026
% Result : Unsatisfiable 88.53s 11.67s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG012-1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n016.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 12:57:22 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 88.53/11.67 % Refutation found
% 88.53/11.67 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 88.53/11.67 % SZS output start CNFRefutation for theBenchmark
% 88.53/11.67 fof(f1,axiom,(
% 88.53/11.67 (![X,Y,Z]: (f(X,f(Y,Z)) = f(f(X,Y),Z) ))),
% 88.53/11.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 88.53/11.67 fof(f2,axiom,(
% 88.53/11.67 (![X]: (( c(X)| d1(X)| d2(X) ) ))),
% 88.53/11.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 88.53/11.67 fof(f3,hypothesis,(
% 88.53/11.67 (![X]: (( ~ c(X)| ~ d1(X) ) ))),
% 88.53/11.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 88.53/11.67 fof(f4,hypothesis,(
% 88.53/11.67 (![X]: (( ~ c(X)| ~ d2(X) ) ))),
% 88.53/11.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 88.53/11.67 fof(f5,hypothesis,(
% 88.53/11.67 (![X]: (( ~ d1(X)| ~ d2(X) ) ))),
% 88.53/11.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 88.53/11.67 fof(f6,hypothesis,(
% 88.53/11.67 c(a1) ),
% 88.53/11.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 88.53/11.67 fof(f7,hypothesis,(
% 88.53/11.67 d1(a2) ),
% 88.53/11.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 88.53/11.67 fof(f8,hypothesis,(
% 88.53/11.67 d2(a3) ),
% 88.53/11.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 88.53/11.67 fof(f9,negated_conjecture,(
% 88.53/11.67 (![X,Y]: (( d2(f(X,Y))| d1(f(X,Y))| ~ c(X)| ~ c(Y) ) ))),
% 88.53/11.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 88.53/11.67 fof(f10,negated_conjecture,(
% 88.53/11.67 (![X,Y]: (( c(f(X,Y))| ~ d1(X)| ~ d1(Y) ) ))),
% 88.53/11.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 88.53/11.67 fof(f11,negated_conjecture,(
% 88.53/11.67 (![X,Y]: (( c(f(X,Y))| ~ d2(X)| ~ d2(Y) ) ))),
% 88.53/11.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 88.53/11.67 fof(f12,plain,(
% 88.53/11.67 ![X0,X1,X2]: (f(X0,f(X1,X2))=f(f(X0,X1),X2))),
% 88.53/11.67 inference(cnf_transformation,[status(thm)],[f1])).
% 88.53/11.67 fof(f13,plain,(
% 88.53/11.67 ![X0]: (c(X0)|d1(X0)|d2(X0))),
% 88.53/11.67 inference(cnf_transformation,[status(thm)],[f2])).
% 88.53/11.67 fof(f14,plain,(
% 88.53/11.67 ![X0]: (~c(X0)|~d1(X0))),
% 88.53/11.67 inference(cnf_transformation,[status(thm)],[f3])).
% 88.53/11.67 fof(f15,plain,(
% 88.53/11.67 ![X0]: (~c(X0)|~d2(X0))),
% 88.53/11.67 inference(cnf_transformation,[status(thm)],[f4])).
% 88.53/11.67 fof(f16,plain,(
% 88.53/11.67 ![X0]: (~d1(X0)|~d2(X0))),
% 88.53/11.67 inference(cnf_transformation,[status(thm)],[f5])).
% 88.53/11.67 fof(f17,plain,(
% 88.53/11.67 c(a1)),
% 88.53/11.67 inference(cnf_transformation,[status(thm)],[f6])).
% 88.53/11.67 fof(f18,plain,(
% 88.53/11.67 d1(a2)),
% 88.53/11.67 inference(cnf_transformation,[status(thm)],[f7])).
% 88.53/11.67 fof(f19,plain,(
% 88.53/11.67 d2(a3)),
% 88.53/11.67 inference(cnf_transformation,[status(thm)],[f8])).
% 88.53/11.67 fof(f20,plain,(
% 88.53/11.67 ![Y]: ((![X]: ((d2(f(X,Y))|d1(f(X,Y)))|~c(X)))|~c(Y))),
% 88.53/11.67 inference(miniscoping,[status(thm)],[f9])).
% 88.53/11.67 fof(f21,plain,(
% 88.53/11.67 ![X0,X1]: (d2(f(X0,X1))|d1(f(X0,X1))|~c(X0)|~c(X1))),
% 88.53/11.67 inference(cnf_transformation,[status(thm)],[f20])).
% 88.53/11.67 fof(f22,plain,(
% 88.53/11.67 ![Y]: ((![X]: (c(f(X,Y))|~d1(X)))|~d1(Y))),
% 88.53/11.67 inference(miniscoping,[status(thm)],[f10])).
% 88.53/11.67 fof(f23,plain,(
% 88.53/11.67 ![X0,X1]: (c(f(X0,X1))|~d1(X0)|~d1(X1))),
% 88.53/11.67 inference(cnf_transformation,[status(thm)],[f22])).
% 88.53/11.67 fof(f24,plain,(
% 88.53/11.67 ![Y]: ((![X]: (c(f(X,Y))|~d2(X)))|~d2(Y))),
% 88.53/11.67 inference(miniscoping,[status(thm)],[f11])).
% 88.53/11.67 fof(f25,plain,(
% 88.53/11.67 ![X0,X1]: (c(f(X0,X1))|~d2(X0)|~d2(X1))),
% 88.53/11.67 inference(cnf_transformation,[status(thm)],[f24])).
% 88.53/11.67 fof(f27,plain,(
% 88.53/11.67 ![X0,X1,X2]: (d2(f(X0,f(X1,X2)))|d1(f(f(X0,X1),X2))|~c(f(X0,X1))|~c(X2))),
% 88.53/11.67 inference(paramodulation,[status(thm)],[f12,f21])).
% 88.53/11.67 fof(f28,plain,(
% 88.53/11.67 ![X0,X1,X2]: (c(f(X0,f(X1,X2)))|~d2(f(X0,X1))|~d2(X2))),
% 88.53/11.67 inference(paramodulation,[status(thm)],[f12,f25])).
% 88.53/11.67 fof(f29,plain,(
% 88.53/11.67 ![X0,X1,X2]: (c(f(X0,f(X1,X2)))|~d1(f(X0,X1))|~d1(X2))),
% 88.53/11.67 inference(paramodulation,[status(thm)],[f12,f23])).
% 88.53/11.67 fof(f32,plain,(
% 88.53/11.67 ![X0,X1,X2]: (d2(f(X0,f(X1,X2)))|d1(f(X0,f(X1,X2)))|~c(f(X0,X1))|~c(X2))),
% 88.53/11.67 inference(forward_demodulation,[status(thm)],[f12,f27])).
% 88.53/11.67 fof(f33,plain,(
% 88.53/11.67 ![X0,X1]: (~c(f(X0,X1))|d1(f(X0,X1))|~c(X0)|~c(X1))),
% 88.53/11.67 inference(resolution,[status(thm)],[f15,f21])).
% 88.53/11.67 fof(f34,plain,(
% 88.53/11.67 ![X0,X1]: (~c(f(X0,X1))|~c(X0)|~c(X1))),
% 88.53/11.67 inference(forward_subsumption_resolution,[status(thm)],[f33,f14])).
% 88.53/11.67 fof(f35,plain,(
% 88.53/11.67 ![X0,X1,X2]: (~c(f(X0,f(X1,X2)))|~c(X0)|~d2(X1)|~d2(X2))),
% 88.53/11.67 inference(resolution,[status(thm)],[f34,f25])).
% 88.53/11.67 fof(f36,plain,(
% 88.53/11.67 ![X0,X1,X2]: (~c(f(X0,f(X1,X2)))|~c(X0)|~d1(X1)|~d1(X2))),
% 88.53/11.67 inference(resolution,[status(thm)],[f34,f23])).
% 88.53/11.67 fof(f37,plain,(
% 88.53/11.67 ![X0,X1]: (~c(f(X0,X1))|~c(X0)|d1(X1)|d2(X1))),
% 88.53/11.67 inference(resolution,[status(thm)],[f34,f13])).
% 88.53/11.67 fof(f38,plain,(
% 88.53/11.67 ![X0,X1,X2]: (~c(f(f(X0,X1),X2))|d1(X2)|d2(X2)|~d2(X0)|~d2(X1))),
% 88.53/11.67 inference(resolution,[status(thm)],[f37,f25])).
% 88.53/11.67 fof(f40,plain,(
% 88.53/11.67 ![X0,X1]: (~c(f(X0,X1))|d1(X1)|d2(X1)|d1(X0)|d2(X0))),
% 88.53/11.67 inference(resolution,[status(thm)],[f37,f13])).
% 88.53/11.67 fof(f41,plain,(
% 88.53/11.67 ![X0,X1,X2]: (~c(f(X0,f(X1,X2)))|d1(X2)|d2(X2)|~d2(X0)|~d2(X1))),
% 88.53/11.67 inference(forward_demodulation,[status(thm)],[f12,f38])).
% 88.53/11.67 fof(f43,plain,(
% 88.53/11.67 ![X0,X1,X2]: (d1(f(X0,f(X1,X2)))|~c(f(X0,X1))|~c(X2)|~c(f(X0,f(X1,X2))))),
% 88.53/11.67 inference(resolution,[status(thm)],[f32,f15])).
% 88.53/11.67 fof(f46,plain,(
% 88.53/11.67 ![X0,X1,X2]: (~c(f(X0,X1))|~c(X2)|~c(f(X0,f(X1,X2))))),
% 88.53/11.67 inference(forward_subsumption_resolution,[status(thm)],[f43,f14])).
% 88.53/11.67 fof(f52,plain,(
% 88.53/11.67 ![X0]: (~c(f(a1,X0))|d1(X0)|d2(X0))),
% 88.53/11.67 inference(resolution,[status(thm)],[f17,f37])).
% 88.53/11.67 fof(f53,plain,(
% 88.53/11.67 ![X0]: (~c(f(X0,a1))|~c(X0))),
% 88.53/11.67 inference(resolution,[status(thm)],[f17,f34])).
% 88.53/11.67 fof(f56,plain,(
% 88.53/11.67 ![X0,X1]: (c(f(X0,f(X1,a3)))|~d2(f(X0,X1)))),
% 88.53/11.67 inference(resolution,[status(thm)],[f19,f28])).
% 88.53/11.67 fof(f57,plain,(
% 88.53/11.67 ~c(a3)),
% 88.53/11.67 inference(resolution,[status(thm)],[f19,f15])).
% 88.53/11.67 fof(f59,definition,(
% 88.53/11.67 sQ0_spl <=> (d1(a2))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f61,plain,(
% 88.53/11.67 ~d1(a2)|sQ0_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f59])).
% 88.53/11.67 fof(f62,definition,(
% 88.53/11.67 sQ1_spl <=> (d2(a2))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f66,plain,(
% 88.53/11.67 d1(a3)|d2(a3)),
% 88.53/11.67 inference(resolution,[status(thm)],[f57,f13])).
% 88.53/11.67 fof(f67,definition,(
% 88.53/11.67 sQ2_spl <=> (d1(a3))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f68,plain,(
% 88.53/11.67 d1(a3)|~sQ2_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f67])).
% 88.53/11.67 fof(f70,definition,(
% 88.53/11.67 sQ3_spl <=> (d2(a3))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f73,plain,(
% 88.53/11.67 sQ2_spl|sQ3_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f66,f67,f70])).
% 88.53/11.67 fof(f74,plain,(
% 88.53/11.67 ~d2(a3)|~sQ2_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f68,f16])).
% 88.53/11.67 fof(f76,plain,(
% 88.53/11.67 $false|~sQ2_spl),
% 88.53/11.67 inference(forward_subsumption_resolution,[status(thm)],[f74,f19])).
% 88.53/11.67 fof(f77,plain,(
% 88.53/11.67 ~sQ2_spl),
% 88.53/11.67 inference(contradiction_clause,[status(thm)],[f76])).
% 88.53/11.67 fof(f80,plain,(
% 88.53/11.67 ![X0]: (~c(X0)|d1(f(X0,a1))|d2(f(X0,a1)))),
% 88.53/11.67 inference(resolution,[status(thm)],[f53,f13])).
% 88.53/11.67 fof(f81,plain,(
% 88.53/11.67 ![X0,X1]: (~c(f(X0,f(X1,a1)))|~c(f(X0,X1)))),
% 88.53/11.67 inference(paramodulation,[status(thm)],[f12,f53])).
% 88.53/11.67 fof(f82,definition,(
% 88.53/11.67 ![X0]: (sQ4_spl <=> (~c(X0)|~d2(X0)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f85,definition,(
% 88.53/11.67 sQ5_spl <=> (d2(a1))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f89,definition,(
% 88.53/11.67 ![X0]: (sQ6_spl <=> (~c(X0)|~d1(X0)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f92,definition,(
% 88.53/11.67 sQ7_spl <=> (d1(a1))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f96,plain,(
% 88.53/11.67 ![X0,X1,X2,X3]: (c(f(f(X0,X1),f(X2,X3)))|~d1(f(X0,f(X1,X2)))|~d1(X3))),
% 88.53/11.67 inference(paramodulation,[status(thm)],[f12,f29])).
% 88.53/11.67 fof(f97,plain,(
% 88.53/11.67 ![X0,X1,X2,X3]: (c(f(X0,f(X1,f(X2,X3))))|~d1(f(X0,f(X1,X2)))|~d1(X3))),
% 88.53/11.67 inference(forward_demodulation,[status(thm)],[f12,f96])).
% 88.53/11.67 fof(f98,plain,(
% 88.53/11.67 ![X0,X1]: (~c(f(X0,f(X1,a3)))|~c(X0)|~d2(X1))),
% 88.53/11.67 inference(resolution,[status(thm)],[f35,f19])).
% 88.53/11.67 fof(f101,plain,(
% 88.53/11.67 ![X0,X1]: (~c(f(X0,f(X1,a2)))|~c(X0)|~d1(X1))),
% 88.53/11.67 inference(resolution,[status(thm)],[f36,f18])).
% 88.53/11.67 fof(f105,definition,(
% 88.53/11.67 ![X0]: (sQ8_spl <=> (d1(X0)|d2(X0)|~d2(X0)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f109,definition,(
% 88.53/11.67 ![X0]: (sQ9_spl <=> (d1(X0)|d2(X0)|~d1(X0)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f113,plain,(
% 88.53/11.67 ![X0,X1,X2]: (~c(X0)|~c(f(X1,f(X2,X0)))|~d2(X1)|~d2(X2))),
% 88.53/11.67 inference(resolution,[status(thm)],[f46,f25])).
% 88.53/11.67 fof(f123,plain,(
% 88.53/11.67 ![X0,X1]: (~c(f(X0,f(X1,a1)))|~d2(X0)|~d2(X1))),
% 88.53/11.67 inference(resolution,[status(thm)],[f81,f25])).
% 88.53/11.67 fof(f124,plain,(
% 88.53/11.67 ![X0,X1]: (~c(f(X0,f(X1,a1)))|~d1(X0)|~d1(X1))),
% 88.53/11.67 inference(resolution,[status(thm)],[f81,f23])).
% 88.53/11.67 fof(f128,plain,(
% 88.53/11.67 ![X0]: (~c(f(X0,f(a3,a3)))|~c(X0))),
% 88.53/11.67 inference(resolution,[status(thm)],[f98,f19])).
% 88.53/11.67 fof(f142,definition,(
% 88.53/11.67 sQ11_spl <=> (d1(f(a3,a3)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f143,plain,(
% 88.53/11.67 d1(f(a3,a3))|~sQ11_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f142])).
% 88.53/11.67 fof(f146,plain,(
% 88.53/11.67 ![X0]: (~c(f(X0,f(a2,a2)))|~c(X0))),
% 88.53/11.67 inference(resolution,[status(thm)],[f101,f18])).
% 88.53/11.67 fof(f155,definition,(
% 88.53/11.67 sQ13_spl <=> (d1(f(a2,a2)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f156,plain,(
% 88.53/11.67 d1(f(a2,a2))|~sQ13_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f155])).
% 88.53/11.67 fof(f163,plain,(
% 88.53/11.67 ![X0]: (~c(f(X0,f(a3,a1)))|~d2(X0))),
% 88.53/11.67 inference(resolution,[status(thm)],[f123,f19])).
% 88.53/11.67 fof(f169,plain,(
% 88.53/11.67 ~c(f(a3,f(a3,a1)))),
% 88.53/11.67 inference(resolution,[status(thm)],[f163,f19])).
% 88.53/11.67 fof(f175,plain,(
% 88.53/11.67 ~d2(a3)|~d2(f(a3,a1))),
% 88.53/11.67 inference(resolution,[status(thm)],[f169,f25])).
% 88.53/11.67 fof(f177,plain,(
% 88.53/11.67 d1(f(a3,f(a3,a1)))|d2(f(a3,f(a3,a1)))),
% 88.53/11.67 inference(resolution,[status(thm)],[f169,f13])).
% 88.53/11.67 fof(f178,definition,(
% 88.53/11.67 sQ14_spl <=> (d2(f(a3,a1)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f181,plain,(
% 88.53/11.67 ~sQ3_spl|~sQ14_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f175,f70,f178])).
% 88.53/11.67 fof(f182,definition,(
% 88.53/11.67 sQ15_spl <=> (d1(f(a3,a1)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f183,plain,(
% 88.53/11.67 d1(f(a3,a1))|~sQ15_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f182])).
% 88.53/11.67 fof(f186,definition,(
% 88.53/11.67 sQ16_spl <=> (d1(f(a3,f(a3,a1))))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f187,plain,(
% 88.53/11.67 d1(f(a3,f(a3,a1)))|~sQ16_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f186])).
% 88.53/11.67 fof(f188,plain,(
% 88.53/11.67 ~d1(f(a3,f(a3,a1)))|sQ16_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f186])).
% 88.53/11.67 fof(f189,definition,(
% 88.53/11.67 sQ17_spl <=> (d2(f(a3,f(a3,a1))))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f190,plain,(
% 88.53/11.67 d2(f(a3,f(a3,a1)))|~sQ17_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f189])).
% 88.53/11.67 fof(f192,plain,(
% 88.53/11.67 sQ16_spl|sQ17_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f177,f186,f189])).
% 88.53/11.67 fof(f194,definition,(
% 88.53/11.67 sQ18_spl <=> (c(a3))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f197,definition,(
% 88.53/11.67 sQ19_spl <=> (c(a1))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f199,plain,(
% 88.53/11.67 ~c(a1)|sQ19_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f197])).
% 88.53/11.67 fof(f201,plain,(
% 88.53/11.67 $false|sQ19_spl),
% 88.53/11.67 inference(forward_subsumption_resolution,[status(thm)],[f199,f17])).
% 88.53/11.67 fof(f202,plain,(
% 88.53/11.67 sQ19_spl),
% 88.53/11.67 inference(contradiction_clause,[status(thm)],[f201])).
% 88.53/11.67 fof(f225,definition,(
% 88.53/11.67 sQ20_spl <=> (c(f(a3,a3)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f227,plain,(
% 88.53/11.67 ~c(f(a3,a3))|sQ20_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f225])).
% 88.53/11.67 fof(f229,definition,(
% 88.53/11.67 sQ21_spl <=> (c(f(a3,a1)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f231,plain,(
% 88.53/11.67 ~c(f(a3,a1))|sQ21_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f229])).
% 88.53/11.67 fof(f234,plain,(
% 88.53/11.67 ![X0]: (~c(f(X0,f(a2,a1)))|~d1(X0))),
% 88.53/11.67 inference(resolution,[status(thm)],[f124,f18])).
% 88.53/11.67 fof(f248,plain,(
% 88.53/11.67 ![X0,X1,X2]: (c(f(X0,f(X1,f(X2,a2))))|~d1(f(X0,f(X1,X2))))),
% 88.53/11.67 inference(resolution,[status(thm)],[f97,f18])).
% 88.53/11.67 fof(f250,plain,(
% 88.53/11.67 ~c(f(a2,f(a2,a1)))),
% 88.53/11.67 inference(resolution,[status(thm)],[f234,f18])).
% 88.53/11.67 fof(f254,plain,(
% 88.53/11.67 ~d1(a2)|~d1(f(a2,a1))),
% 88.53/11.67 inference(resolution,[status(thm)],[f250,f23])).
% 88.53/11.67 fof(f255,plain,(
% 88.53/11.67 d1(f(a2,f(a2,a1)))|d2(f(a2,f(a2,a1)))),
% 88.53/11.67 inference(resolution,[status(thm)],[f250,f13])).
% 88.53/11.67 fof(f256,definition,(
% 88.53/11.67 sQ22_spl <=> (d2(f(a2,a1)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f257,plain,(
% 88.53/11.67 d2(f(a2,a1))|~sQ22_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f256])).
% 88.53/11.67 fof(f260,definition,(
% 88.53/11.67 sQ23_spl <=> (d1(f(a2,a1)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f263,plain,(
% 88.53/11.67 ~sQ0_spl|~sQ23_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f254,f59,f260])).
% 88.53/11.67 fof(f264,definition,(
% 88.53/11.67 sQ24_spl <=> (d1(f(a2,f(a2,a1))))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f265,plain,(
% 88.53/11.67 d1(f(a2,f(a2,a1)))|~sQ24_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f264])).
% 88.53/11.67 fof(f267,definition,(
% 88.53/11.67 sQ25_spl <=> (d2(f(a2,f(a2,a1))))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f270,plain,(
% 88.53/11.67 sQ24_spl|sQ25_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f255,f264,f267])).
% 88.53/11.67 fof(f271,plain,(
% 88.53/11.67 ![X0,X1]: (~c(f(X0,f(a3,X1)))|d1(X1)|d2(X1)|~d2(X0))),
% 88.53/11.67 inference(resolution,[status(thm)],[f41,f19])).
% 88.53/11.67 fof(f278,definition,(
% 88.53/11.67 sQ26_spl <=> (c(a2))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f282,plain,(
% 88.53/11.67 $false|sQ0_spl),
% 88.53/11.67 inference(forward_subsumption_resolution,[status(thm)],[f61,f18])).
% 88.53/11.67 fof(f283,plain,(
% 88.53/11.67 sQ0_spl),
% 88.53/11.67 inference(contradiction_clause,[status(thm)],[f282])).
% 88.53/11.67 fof(f301,definition,(
% 88.53/11.67 sQ27_spl <=> (c(f(a2,a2)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f303,plain,(
% 88.53/11.67 ~c(f(a2,a2))|sQ27_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f301])).
% 88.53/11.67 fof(f305,definition,(
% 88.53/11.67 sQ28_spl <=> (c(f(a2,a1)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f306,plain,(
% 88.53/11.67 c(f(a2,a1))|~sQ28_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f305])).
% 88.53/11.67 fof(f307,plain,(
% 88.53/11.67 ~c(f(a2,a1))|sQ28_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f305])).
% 88.53/11.67 fof(f309,plain,(
% 88.53/11.67 d1(f(a1,a1))|d2(f(a1,a1))),
% 88.53/11.67 inference(resolution,[status(thm)],[f80,f17])).
% 88.53/11.67 fof(f313,definition,(
% 88.53/11.67 sQ29_spl <=> (d1(f(a1,a1)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f314,plain,(
% 88.53/11.67 d1(f(a1,a1))|~sQ29_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f313])).
% 88.53/11.67 fof(f316,definition,(
% 88.53/11.67 sQ30_spl <=> (d2(f(a1,a1)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f317,plain,(
% 88.53/11.67 d2(f(a1,a1))|~sQ30_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f316])).
% 88.53/11.67 fof(f319,plain,(
% 88.53/11.67 sQ29_spl|sQ30_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f309,f313,f316])).
% 88.53/11.67 fof(f344,plain,(
% 88.53/11.67 ![X0,X1]: (d1(X0)|d2(X0)|d1(X1)|d2(X1)|~d2(X1)|~d2(X0))),
% 88.53/11.67 inference(resolution,[status(thm)],[f40,f25])).
% 88.53/11.67 fof(f345,plain,(
% 88.53/11.67 ![X0,X1]: (d1(X0)|d2(X0)|d1(X1)|d2(X1)|~d1(X1)|~d1(X0))),
% 88.53/11.67 inference(resolution,[status(thm)],[f40,f23])).
% 88.53/11.67 fof(f348,plain,(
% 88.53/11.67 sQ8_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f344,f105])).
% 88.53/11.67 fof(f349,plain,(
% 88.53/11.67 sQ9_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f345,f109])).
% 88.53/11.67 fof(f370,definition,(
% 88.53/11.67 sQ31_spl <=> (d1(f(a1,a2)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f371,plain,(
% 88.53/11.67 d1(f(a1,a2))|~sQ31_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f370])).
% 88.53/11.67 fof(f373,definition,(
% 88.53/11.67 sQ32_spl <=> (d2(f(a1,a2)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f374,plain,(
% 88.53/11.67 d2(f(a1,a2))|~sQ32_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f373])).
% 88.53/11.67 fof(f391,plain,(
% 88.53/11.67 ![X0]: (c(f(a1,f(a2,X0)))|~d1(X0)|~sQ31_spl)),
% 88.53/11.67 inference(resolution,[status(thm)],[f371,f29])).
% 88.53/11.67 fof(f417,plain,(
% 88.53/11.67 c(f(a1,f(a2,a2)))|~sQ31_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f391,f18])).
% 88.53/11.67 fof(f430,plain,(
% 88.53/11.67 ![X0,X1]: (~c(X0)|~c(f(X1,f(a3,X0)))|~d2(X1))),
% 88.53/11.67 inference(resolution,[status(thm)],[f113,f19])).
% 88.53/11.67 fof(f437,plain,(
% 88.53/11.67 ~c(a1)|~sQ31_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f417,f146])).
% 88.53/11.67 fof(f446,plain,(
% 88.53/11.67 ~sQ19_spl|~sQ31_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f437,f197,f370])).
% 88.53/11.67 fof(f461,plain,(
% 88.53/11.67 c(f(a1,f(a1,a3)))|~sQ30_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f317,f56])).
% 88.53/11.67 fof(f471,plain,(
% 88.53/11.67 ~c(f(a1,a1))|~sQ30_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f317,f15])).
% 88.53/11.67 fof(f486,plain,(
% 88.53/11.67 ~d2(a1)|~d2(a1)|~sQ30_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f471,f25])).
% 88.53/11.67 fof(f487,plain,(
% 88.53/11.67 ~d1(a1)|~d1(a1)|~sQ30_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f471,f23])).
% 88.53/11.67 fof(f489,plain,(
% 88.53/11.67 ~sQ5_spl|~sQ30_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f486,f85,f316])).
% 88.53/11.67 fof(f490,plain,(
% 88.53/11.67 ~sQ7_spl|~sQ30_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f487,f92,f316])).
% 88.53/11.67 fof(f492,plain,(
% 88.53/11.67 d1(f(a1,a3))|d2(f(a1,a3))|~sQ30_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f461,f52])).
% 88.53/11.67 fof(f500,definition,(
% 88.53/11.67 sQ37_spl <=> (d1(f(a1,a3)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f501,plain,(
% 88.53/11.67 d1(f(a1,a3))|~sQ37_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f500])).
% 88.53/11.67 fof(f502,plain,(
% 88.53/11.67 ~d1(f(a1,a3))|sQ37_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f500])).
% 88.53/11.67 fof(f503,definition,(
% 88.53/11.67 sQ38_spl <=> (d2(f(a1,a3)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f506,plain,(
% 88.53/11.67 sQ37_spl|sQ38_spl|~sQ30_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f492,f500,f503,f316])).
% 88.53/11.67 fof(f521,plain,(
% 88.53/11.67 ![X0]: (c(f(a1,f(a3,X0)))|~d1(X0)|~sQ37_spl)),
% 88.53/11.67 inference(resolution,[status(thm)],[f501,f29])).
% 88.53/11.67 fof(f557,plain,(
% 88.53/11.67 c(f(a1,f(a3,a2)))|~sQ37_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f521,f18])).
% 88.53/11.67 fof(f558,plain,(
% 88.53/11.67 d1(f(a3,a2))|d2(f(a3,a2))|~sQ37_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f557,f52])).
% 88.53/11.67 fof(f568,definition,(
% 88.53/11.67 sQ41_spl <=> (d1(f(a3,a2)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f569,plain,(
% 88.53/11.67 d1(f(a3,a2))|~sQ41_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f568])).
% 88.53/11.67 fof(f571,definition,(
% 88.53/11.67 sQ42_spl <=> (d2(f(a3,a2)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f574,plain,(
% 88.53/11.67 sQ41_spl|sQ42_spl|~sQ37_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f558,f568,f571,f500])).
% 88.53/11.67 fof(f593,plain,(
% 88.53/11.67 ~c(f(f(a3,a2),f(a2,a1)))|~sQ41_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f569,f234])).
% 88.53/11.67 fof(f602,plain,(
% 88.53/11.67 ~c(f(a3,f(a2,f(a2,a1))))|~sQ41_spl),
% 88.53/11.67 inference(forward_demodulation,[status(thm)],[f12,f593])).
% 88.53/11.67 fof(f761,plain,(
% 88.53/11.67 ![X0]: (~c(X0)|~c(f(a3,f(a3,X0))))),
% 88.53/11.67 inference(resolution,[status(thm)],[f430,f19])).
% 88.53/11.67 fof(f769,plain,(
% 88.53/11.67 ![X0]: (~c(X0)|~d2(a3)|~d2(f(a3,X0)))),
% 88.53/11.67 inference(resolution,[status(thm)],[f761,f25])).
% 88.53/11.67 fof(f772,definition,(
% 88.53/11.67 ![X0]: (sQ53_spl <=> (~c(X0)|~d2(f(a3,X0))))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f773,plain,(
% 88.53/11.67 ![X0]: (~c(X0)|~d2(f(a3,X0))|~sQ53_spl)),
% 88.53/11.67 inference(component_clause,[status(thm)],[f772])).
% 88.53/11.67 fof(f775,plain,(
% 88.53/11.67 sQ53_spl|~sQ3_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f769,f772,f70])).
% 88.53/11.67 fof(f798,definition,(
% 88.53/11.67 sQ56_spl <=> (d2(f(a1,f(a3,a1))))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f799,plain,(
% 88.53/11.67 d2(f(a1,f(a3,a1)))|~sQ56_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f798])).
% 88.53/11.67 fof(f802,definition,(
% 88.53/11.67 sQ57_spl <=> (d1(f(a1,f(a3,a1))))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f816,definition,(
% 88.53/11.67 ![X1]: (sQ59_spl <=> (~d1(X1)|~d2(X1)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f820,definition,(
% 88.53/11.67 ![X0]: (sQ60_spl <=> (~c(X0)|~d1(f(a2,X0))))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f821,plain,(
% 88.53/11.67 ![X0]: (~c(X0)|~d1(f(a2,X0))|~sQ60_spl)),
% 88.53/11.67 inference(component_clause,[status(thm)],[f820])).
% 88.53/11.67 fof(f823,definition,(
% 88.53/11.67 ![X1]: (sQ61_spl <=> (~d1(X1)|~d1(X1)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f824,plain,(
% 88.53/11.67 ![X0]: (~d1(X0)|~d1(X0)|~sQ61_spl)),
% 88.53/11.67 inference(component_clause,[status(thm)],[f823])).
% 88.53/11.67 fof(f827,plain,(
% 88.53/11.67 ~c(f(a2,a1))|~sQ60_spl|~sQ24_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f821,f265])).
% 88.53/11.67 fof(f830,plain,(
% 88.53/11.67 d1(f(a2,a1))|d2(f(a2,a1))|~sQ60_spl|~sQ24_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f827,f13])).
% 88.53/11.67 fof(f833,plain,(
% 88.53/11.67 sQ23_spl|sQ22_spl|~sQ60_spl|~sQ24_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f830,f260,f256,f820,f264])).
% 88.53/11.67 fof(f837,definition,(
% 88.53/11.67 ![X0]: (sQ62_spl <=> (~c(X0)|d1(f(a2,X0))|~c(X0)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f838,plain,(
% 88.53/11.67 ![X0]: (~c(X0)|d1(f(a2,X0))|~c(X0)|~sQ62_spl)),
% 88.53/11.67 inference(component_clause,[status(thm)],[f837])).
% 88.53/11.67 fof(f1060,definition,(
% 88.53/11.67 sQ71_spl <=> (c(f(a1,a3)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f1061,plain,(
% 88.53/11.67 c(f(a1,a3))|~sQ71_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f1060])).
% 88.53/11.67 fof(f1062,plain,(
% 88.53/11.67 ~c(f(a1,a3))|sQ71_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f1060])).
% 88.53/11.67 fof(f1324,plain,(
% 88.53/11.67 c(f(a3,f(a3,f(a1,a2))))|~sQ16_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f248,f187])).
% 88.53/11.67 fof(f1445,plain,(
% 88.53/11.67 ~d2(a3)|~d2(f(a2,f(a2,a1)))|~sQ41_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f602,f25])).
% 88.53/11.67 fof(f1448,plain,(
% 88.53/11.67 ~sQ3_spl|~sQ25_spl|~sQ41_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f1445,f70,f267,f568])).
% 88.53/11.67 fof(f1451,plain,(
% 88.53/11.67 ![X0]: (~d1(X0)|~sQ61_spl)),
% 88.53/11.67 inference(duplicate_literals_removal,[status(thm)],[f824])).
% 88.53/11.67 fof(f1486,plain,(
% 88.53/11.67 $false|~sQ61_spl),
% 88.53/11.67 inference(backward_subsumption_resolution,[status(thm)],[f18,f1451])).
% 88.53/11.67 fof(f1502,plain,(
% 88.53/11.67 ![X0]: (c(f(X0,a2))|~d1(X0))),
% 88.53/11.67 inference(resolution,[status(thm)],[f18,f23])).
% 88.53/11.67 fof(f1507,plain,(
% 88.53/11.67 ![X0]: (d2(f(X0,a1))|d1(f(X0,a1))|~c(X0))),
% 88.53/11.67 inference(resolution,[status(thm)],[f21,f17])).
% 88.53/11.67 fof(f1527,plain,(
% 88.53/11.67 ![X0,X1]: (d1(X0)|d2(X0)|d2(f(X1,X0))|d1(f(X1,X0))|~c(X1))),
% 88.53/11.67 inference(resolution,[status(thm)],[f13,f21])).
% 88.53/11.67 fof(f1578,plain,(
% 88.53/11.67 c(f(a2,a2))),
% 88.53/11.67 inference(resolution,[status(thm)],[f1502,f18])).
% 88.53/11.67 fof(f1582,plain,(
% 88.53/11.67 ![X0]: (~c(X0)|~c(f(a2,f(a2,X0))))),
% 88.53/11.67 inference(resolution,[status(thm)],[f1578,f46])).
% 88.53/11.67 fof(f1583,plain,(
% 88.53/11.67 ![X0]: (d2(f(X0,f(a2,a2)))|d1(f(X0,f(a2,a2)))|~c(X0))),
% 88.53/11.67 inference(resolution,[status(thm)],[f1578,f21])).
% 88.53/11.67 fof(f1607,plain,(
% 88.53/11.67 ![X0,X1]: (d2(f(f(X0,X1),a1))|d1(f(f(X0,X1),a1))|~d2(X0)|~d2(X1))),
% 88.53/11.67 inference(resolution,[status(thm)],[f1507,f25])).
% 88.53/11.67 fof(f1608,plain,(
% 88.53/11.67 ![X0]: (d2(f(X0,a1))|d1(f(X0,a1))|d1(X0)|d2(X0))),
% 88.53/11.67 inference(resolution,[status(thm)],[f1507,f13])).
% 88.53/11.67 fof(f1620,plain,(
% 88.53/11.67 ![X0,X1]: (d2(f(X0,f(X1,a1)))|d1(f(f(X0,X1),a1))|~d2(X0)|~d2(X1))),
% 88.53/11.67 inference(forward_demodulation,[status(thm)],[f12,f1607])).
% 88.53/11.67 fof(f1621,plain,(
% 88.53/11.67 ![X0,X1]: (d2(f(X0,f(X1,a1)))|d1(f(X0,f(X1,a1)))|~d2(X0)|~d2(X1))),
% 88.53/11.67 inference(forward_demodulation,[status(thm)],[f12,f1620])).
% 88.53/11.67 fof(f1685,plain,(
% 88.53/11.67 ![X0]: (d1(X0)|d2(X0)|d2(f(a1,X0))|d1(f(a1,X0)))),
% 88.53/11.67 inference(resolution,[status(thm)],[f1527,f17])).
% 88.53/11.67 fof(f1691,plain,(
% 88.53/11.67 ![X0,X1,X2]: (d1(X0)|d2(X0)|d2(f(f(X1,X2),X0))|d1(f(f(X1,X2),X0))|~d2(X1)|~d2(X2))),
% 88.53/11.67 inference(resolution,[status(thm)],[f1527,f25])).
% 88.53/11.67 fof(f1713,plain,(
% 88.53/11.67 ![X0,X1,X2]: (d1(X0)|d2(X0)|d2(f(X1,f(X2,X0)))|d1(f(f(X1,X2),X0))|~d2(X1)|~d2(X2))),
% 88.53/11.67 inference(forward_demodulation,[status(thm)],[f12,f1691])).
% 88.53/11.67 fof(f1714,plain,(
% 88.53/11.67 ![X0,X1,X2]: (d1(X0)|d2(X0)|d2(f(X1,f(X2,X0)))|d1(f(X1,f(X2,X0)))|~d2(X1)|~d2(X2))),
% 88.53/11.67 inference(forward_demodulation,[status(thm)],[f12,f1713])).
% 88.53/11.67 fof(f1786,definition,(
% 88.53/11.67 sQ85_spl <=> (d1(f(a2,a3)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f1787,plain,(
% 88.53/11.67 d1(f(a2,a3))|~sQ85_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f1786])).
% 88.53/11.67 fof(f1789,definition,(
% 88.53/11.67 sQ86_spl <=> (d2(f(a2,a3)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f1790,plain,(
% 88.53/11.67 d2(f(a2,a3))|~sQ86_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f1789])).
% 88.53/11.67 fof(f1869,definition,(
% 88.53/11.67 sQ87_spl <=> (d1(f(a1,f(a3,a2))))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f1870,plain,(
% 88.53/11.67 d1(f(a1,f(a3,a2)))|~sQ87_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f1869])).
% 88.53/11.67 fof(f1872,definition,(
% 88.53/11.67 sQ88_spl <=> (d2(f(a1,f(a3,a2))))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f1873,plain,(
% 88.53/11.67 d2(f(a1,f(a3,a2)))|~sQ88_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f1872])).
% 88.53/11.67 fof(f1924,plain,(
% 88.53/11.67 ~c(f(a1,a2))|~sQ16_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f1324,f761])).
% 88.53/11.67 fof(f1937,definition,(
% 88.53/11.67 sQ91_spl <=> (d1(f(a3,f(a1,a2))))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f1938,plain,(
% 88.53/11.67 d1(f(a3,f(a1,a2)))|~sQ91_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f1937])).
% 88.53/11.67 fof(f1940,definition,(
% 88.53/11.67 sQ92_spl <=> (d2(f(a3,f(a1,a2))))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f1969,plain,(
% 88.53/11.67 d1(f(a1,a2))|d2(f(a1,a2))|~sQ16_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f1924,f13])).
% 88.53/11.67 fof(f1971,plain,(
% 88.53/11.67 sQ31_spl|sQ32_spl|~sQ16_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f1969,f370,f373,f186])).
% 88.53/11.67 fof(f1972,plain,(
% 88.53/11.67 ~c(f(a3,a1))|~sQ17_spl|~sQ53_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f190,f773])).
% 88.53/11.67 fof(f2000,plain,(
% 88.53/11.67 d1(f(a3,a1))|d2(f(a3,a1))|~sQ17_spl|~sQ53_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f1972,f13])).
% 88.53/11.67 fof(f2002,plain,(
% 88.53/11.67 sQ15_spl|sQ14_spl|~sQ17_spl|~sQ53_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f2000,f182,f178,f189,f772])).
% 88.53/11.67 fof(f2010,plain,(
% 88.53/11.67 ![X0]: (c(f(X0,f(a3,a1)))|~d1(X0)|~sQ15_spl)),
% 88.53/11.67 inference(resolution,[status(thm)],[f183,f23])).
% 88.53/11.67 fof(f2043,plain,(
% 88.53/11.67 c(f(a1,f(a2,a3)))|~sQ32_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f374,f56])).
% 88.53/11.67 fof(f2052,plain,(
% 88.53/11.67 ~c(f(a1,a2))|~sQ32_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f374,f15])).
% 88.53/11.67 fof(f2074,plain,(
% 88.53/11.67 c(f(f(a1,a1),a2))|~sQ29_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f314,f1502])).
% 88.53/11.67 fof(f2078,plain,(
% 88.53/11.67 c(f(a1,f(a1,a2)))|~sQ29_spl),
% 88.53/11.67 inference(forward_demodulation,[status(thm)],[f12,f2074])).
% 88.53/11.67 fof(f2116,plain,(
% 88.53/11.67 ![X0]: (d1(f(X0,a1))|d1(X0)|d2(X0)|~c(f(X0,a1)))),
% 88.53/11.67 inference(resolution,[status(thm)],[f1608,f15])).
% 88.53/11.67 fof(f2130,plain,(
% 88.53/11.67 ![X0]: (d1(X0)|d2(X0)|~c(f(X0,a1)))),
% 88.53/11.67 inference(forward_subsumption_resolution,[status(thm)],[f2116,f14])).
% 88.53/11.67 fof(f2165,plain,(
% 88.53/11.67 d1(f(a2,a3))|d2(f(a2,a3))|~sQ32_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f2043,f52])).
% 88.53/11.67 fof(f2177,plain,(
% 88.53/11.67 sQ85_spl|sQ86_spl|~sQ32_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f2165,f1786,f1789,f373])).
% 88.53/11.67 fof(f2198,plain,(
% 88.53/11.67 c(f(a2,f(a3,a3)))|~sQ86_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f1790,f56])).
% 88.53/11.67 fof(f2220,plain,(
% 88.53/11.67 ![X0]: (c(f(a2,f(a3,X0)))|~d1(X0)|~sQ85_spl)),
% 88.53/11.67 inference(resolution,[status(thm)],[f1787,f29])).
% 88.53/11.67 fof(f2222,plain,(
% 88.53/11.67 c(f(f(a2,a3),a2))|~sQ85_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f1787,f1502])).
% 88.53/11.67 fof(f2224,plain,(
% 88.53/11.67 ~d2(f(a2,a3))|~sQ85_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f1787,f16])).
% 88.53/11.67 fof(f2225,plain,(
% 88.53/11.67 ![X0]: (c(f(X0,f(a2,a3)))|~d1(X0)|~sQ85_spl)),
% 88.53/11.67 inference(resolution,[status(thm)],[f1787,f23])).
% 88.53/11.67 fof(f2226,plain,(
% 88.53/11.67 c(f(a2,f(a3,a2)))|~sQ85_spl),
% 88.53/11.67 inference(forward_demodulation,[status(thm)],[f12,f2222])).
% 88.53/11.67 fof(f2227,plain,(
% 88.53/11.67 $false|~sQ86_spl|~sQ85_spl),
% 88.53/11.67 inference(forward_subsumption_resolution,[status(thm)],[f2224,f1790])).
% 88.53/11.67 fof(f2228,plain,(
% 88.53/11.67 ~sQ86_spl|~sQ85_spl),
% 88.53/11.67 inference(contradiction_clause,[status(thm)],[f2227])).
% 88.53/11.67 fof(f2241,plain,(
% 88.53/11.67 ![X0]: (d1(X0)|d2(X0)|d1(f(a1,X0))|c(f(a1,f(X0,a3))))),
% 88.53/11.67 inference(resolution,[status(thm)],[f1685,f56])).
% 88.53/11.67 fof(f2724,definition,(
% 88.53/11.67 sQ111_spl <=> (d2(f(a3,f(a2,a2))))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f2725,plain,(
% 88.53/11.67 d2(f(a3,f(a2,a2)))|~sQ111_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f2724])).
% 88.53/11.67 fof(f2728,plain,(
% 88.53/11.67 ~c(f(a2,a2))|~sQ111_spl|~sQ53_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f2725,f773])).
% 88.53/11.67 fof(f2747,plain,(
% 88.53/11.67 $false|~sQ111_spl|~sQ53_spl),
% 88.53/11.67 inference(forward_subsumption_resolution,[status(thm)],[f2728,f1578])).
% 88.53/11.67 fof(f2748,plain,(
% 88.53/11.67 ~sQ111_spl|~sQ53_spl),
% 88.53/11.67 inference(contradiction_clause,[status(thm)],[f2747])).
% 88.53/11.67 fof(f2997,plain,(
% 88.53/11.67 c(f(a2,f(a2,a3)))|~sQ85_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f2225,f18])).
% 88.53/11.67 fof(f3695,plain,(
% 88.53/11.67 d2(f(a1,f(a2,a2)))|d1(f(a1,f(a2,a2)))),
% 88.53/11.67 inference(resolution,[status(thm)],[f1583,f17])).
% 88.53/11.67 fof(f3708,definition,(
% 88.53/11.67 sQ154_spl <=> (d2(f(a1,f(a2,a2))))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f3709,plain,(
% 88.53/11.67 d2(f(a1,f(a2,a2)))|~sQ154_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f3708])).
% 88.53/11.67 fof(f3711,definition,(
% 88.53/11.67 sQ155_spl <=> (d1(f(a1,f(a2,a2))))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f3712,plain,(
% 88.53/11.67 d1(f(a1,f(a2,a2)))|~sQ155_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f3711])).
% 88.53/11.67 fof(f3714,plain,(
% 88.53/11.67 sQ154_spl|sQ155_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f3695,f3708,f3711])).
% 88.53/11.67 fof(f3941,plain,(
% 88.53/11.67 c(f(a2,f(a1,a3)))|~sQ22_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f257,f56])).
% 88.53/11.67 fof(f3951,plain,(
% 88.53/11.67 ~c(f(f(a2,a1),f(a3,a1)))|~sQ22_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f257,f163])).
% 88.53/11.67 fof(f3968,plain,(
% 88.53/11.67 ~c(f(a2,f(a1,f(a3,a1))))|~sQ22_spl),
% 88.53/11.67 inference(forward_demodulation,[status(thm)],[f12,f3951])).
% 88.53/11.67 fof(f4086,plain,(
% 88.53/11.67 d1(f(a1,a3))|d2(f(a1,a3))|sQ71_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f1062,f13])).
% 88.53/11.67 fof(f4088,plain,(
% 88.53/11.67 sQ37_spl|sQ38_spl|sQ71_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f4086,f500,f503,f1060])).
% 88.53/11.67 fof(f6469,definition,(
% 88.53/11.67 sQ211_spl <=> (d1(f(a2,f(a2,a2))))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f6470,plain,(
% 88.53/11.67 d1(f(a2,f(a2,a2)))|~sQ211_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f6469])).
% 88.53/11.67 fof(f6531,plain,(
% 88.53/11.67 $false|sQ27_spl),
% 88.53/11.67 inference(forward_subsumption_resolution,[status(thm)],[f303,f1578])).
% 88.53/11.67 fof(f6532,plain,(
% 88.53/11.67 sQ27_spl),
% 88.53/11.67 inference(contradiction_clause,[status(thm)],[f6531])).
% 88.53/11.67 fof(f6635,plain,(
% 88.53/11.67 ~c(f(a2,a2))|~sQ211_spl|~sQ60_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f6470,f821])).
% 88.53/11.67 fof(f6654,plain,(
% 88.53/11.67 ~sQ27_spl|~sQ211_spl|~sQ60_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f6635,f301,f6469,f820])).
% 88.53/11.67 fof(f6957,definition,(
% 88.53/11.67 sQ233_spl <=> (d1(f(a3,f(a1,a1))))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ233_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f6958,plain,(
% 88.53/11.67 d1(f(a3,f(a1,a1)))|~sQ233_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f6957])).
% 88.53/11.67 fof(f6978,plain,(
% 88.53/11.67 ~c(f(a3,f(a1,a1)))|~sQ233_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f6958,f14])).
% 88.53/11.67 fof(f6996,plain,(
% 88.53/11.67 ~d2(a3)|~d2(f(a1,a1))|~sQ233_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f6978,f25])).
% 88.53/11.67 fof(f6998,plain,(
% 88.53/11.67 ~sQ3_spl|~sQ30_spl|~sQ233_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f6996,f70,f316,f6957])).
% 88.53/11.67 fof(f7121,plain,(
% 88.53/11.67 ~sQ61_spl),
% 88.53/11.67 inference(contradiction_clause,[status(thm)],[f1486])).
% 88.53/11.67 fof(f7363,plain,(
% 88.53/11.67 ![X0]: (d1(X0)|d2(X0)|d1(f(a1,X0))|~c(a1)|d1(f(X0,a3))|d2(f(X0,a3)))),
% 88.53/11.67 inference(resolution,[status(thm)],[f2241,f37])).
% 88.53/11.67 fof(f7394,definition,(
% 88.53/11.67 ![X0]: (sQ255_spl <=> (d1(X0)|d2(X0)|d1(f(a1,X0))|d1(f(X0,a3))|d2(f(X0,a3))))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ255_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f7406,plain,(
% 88.53/11.67 sQ255_spl|~sQ19_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f7363,f7394,f197])).
% 88.53/11.67 fof(f9224,definition,(
% 88.53/11.67 sQ270_spl <=> (c(f(a2,a3)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ270_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f9226,plain,(
% 88.53/11.67 ~c(f(a2,a3))|sQ270_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f9224])).
% 88.53/11.67 fof(f9253,definition,(
% 88.53/11.67 sQ273_spl <=> (d1(f(a1,f(a2,a3))))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ273_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f9254,plain,(
% 88.53/11.67 d1(f(a1,f(a2,a3)))|~sQ273_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f9253])).
% 88.53/11.67 fof(f9256,definition,(
% 88.53/11.67 sQ274_spl <=> (d2(f(a1,f(a2,a3))))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ274_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f9257,plain,(
% 88.53/11.67 d2(f(a1,f(a2,a3)))|~sQ274_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f9256])).
% 88.53/11.67 fof(f9258,plain,(
% 88.53/11.67 ~d2(f(a1,f(a2,a3)))|sQ274_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f9256])).
% 88.53/11.67 fof(f9388,plain,(
% 88.53/11.67 ~c(f(a1,f(a2,a3)))|~sQ274_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f9257,f15])).
% 88.53/11.67 fof(f9467,plain,(
% 88.53/11.67 $false|~sQ32_spl|~sQ274_spl),
% 88.53/11.67 inference(forward_subsumption_resolution,[status(thm)],[f9388,f2043])).
% 88.53/11.67 fof(f9468,plain,(
% 88.53/11.67 ~sQ32_spl|~sQ274_spl),
% 88.53/11.67 inference(contradiction_clause,[status(thm)],[f9467])).
% 88.53/11.67 fof(f9488,plain,(
% 88.53/11.67 ~c(f(a1,f(a2,a3)))|~sQ273_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f9254,f14])).
% 88.53/11.67 fof(f9506,plain,(
% 88.53/11.67 $false|~sQ32_spl|~sQ273_spl),
% 88.53/11.67 inference(forward_subsumption_resolution,[status(thm)],[f9488,f2043])).
% 88.53/11.67 fof(f9507,plain,(
% 88.53/11.67 ~sQ32_spl|~sQ273_spl),
% 88.53/11.67 inference(contradiction_clause,[status(thm)],[f9506])).
% 88.53/11.67 fof(f9935,definition,(
% 88.53/11.67 sQ298_spl <=> (d2(f(a3,f(a2,a3))))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ298_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f9936,plain,(
% 88.53/11.67 d2(f(a3,f(a2,a3)))|~sQ298_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f9935])).
% 88.53/11.67 fof(f11204,definition,(
% 88.53/11.67 sQ326_spl <=> (d1(f(a2,f(a3,a3))))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ326_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f11205,plain,(
% 88.53/11.67 d1(f(a2,f(a3,a3)))|~sQ326_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f11204])).
% 88.53/11.67 fof(f11211,plain,(
% 88.53/11.67 ~c(f(a3,a3))|~sQ326_spl|~sQ60_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f11205,f821])).
% 88.53/11.67 fof(f11245,plain,(
% 88.53/11.67 ~d2(a3)|~d2(a3)|~sQ326_spl|~sQ60_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f11211,f25])).
% 88.53/11.67 fof(f11247,plain,(
% 88.53/11.67 ~sQ3_spl|~sQ326_spl|~sQ60_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f11245,f70,f11204,f820])).
% 88.53/11.67 fof(f11563,plain,(
% 88.53/11.67 ![X0,X1]: (d1(X0)|d2(X0)|~d2(X1)|~d2(X1)|~d2(f(a3,X0)))),
% 88.53/11.67 inference(resolution,[status(thm)],[f271,f25])).
% 88.53/11.67 fof(f11576,definition,(
% 88.53/11.67 ![X0]: (sQ335_spl <=> (d1(X0)|d2(X0)|~d2(f(a3,X0))))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ335_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f11577,plain,(
% 88.53/11.67 ![X0]: (d1(X0)|d2(X0)|~d2(f(a3,X0))|~sQ335_spl)),
% 88.53/11.67 inference(component_clause,[status(thm)],[f11576])).
% 88.53/11.67 fof(f11579,definition,(
% 88.53/11.67 ![X1]: (sQ336_spl <=> (~d2(X1)|~d2(X1)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ336_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f11580,plain,(
% 88.53/11.67 ![X0]: (~d2(X0)|~d2(X0)|~sQ336_spl)),
% 88.53/11.67 inference(component_clause,[status(thm)],[f11579])).
% 88.53/11.67 fof(f11582,plain,(
% 88.53/11.67 sQ335_spl|sQ336_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f11563,f11576,f11579])).
% 88.53/11.67 fof(f11583,plain,(
% 88.53/11.67 ![X0]: (~d2(X0)|~sQ336_spl)),
% 88.53/11.67 inference(duplicate_literals_removal,[status(thm)],[f11580])).
% 88.53/11.67 fof(f11625,plain,(
% 88.53/11.67 $false|~sQ336_spl),
% 88.53/11.67 inference(backward_subsumption_resolution,[status(thm)],[f19,f11583])).
% 88.53/11.67 fof(f11652,plain,(
% 88.53/11.67 ~sQ336_spl),
% 88.53/11.67 inference(contradiction_clause,[status(thm)],[f11625])).
% 88.53/11.67 fof(f11659,plain,(
% 88.53/11.67 ![X0,X1,X2]: (d1(f(X0,X1))|~c(X0)|~c(X1)|c(f(X2,f(X0,X1)))|~d2(X2))),
% 88.53/11.67 inference(resolution,[status(thm)],[f21,f25])).
% 88.53/11.67 fof(f11731,plain,(
% 88.53/11.67 ![X0]: (c(f(X0,a3))|~d2(X0))),
% 88.53/11.67 inference(resolution,[status(thm)],[f19,f25])).
% 88.53/11.67 fof(f11739,plain,(
% 88.53/11.67 ~d1(f(a1,a1))|~sQ30_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f317,f16])).
% 88.53/11.67 fof(f11740,plain,(
% 88.53/11.67 ![X0]: (c(f(X0,f(a1,a1)))|~d2(X0)|~sQ30_spl)),
% 88.53/11.67 inference(resolution,[status(thm)],[f317,f25])).
% 88.53/11.67 fof(f11743,plain,(
% 88.53/11.67 ![X0]: (c(f(X0,f(a1,a2)))|~d2(X0)|~sQ32_spl)),
% 88.53/11.67 inference(resolution,[status(thm)],[f374,f25])).
% 88.53/11.67 fof(f11747,plain,(
% 88.53/11.67 c(f(a3,a3))),
% 88.53/11.67 inference(resolution,[status(thm)],[f11731,f19])).
% 88.53/11.67 fof(f11769,plain,(
% 88.53/11.67 ![X0]: (c(f(a1,f(a2,X0)))|~d2(X0)|~sQ32_spl)),
% 88.53/11.67 inference(resolution,[status(thm)],[f28,f374])).
% 88.53/11.67 fof(f11771,plain,(
% 88.53/11.67 ![X0]: (c(f(a2,f(a1,X0)))|~d2(X0)|~sQ22_spl)),
% 88.53/11.67 inference(resolution,[status(thm)],[f28,f257])).
% 88.53/11.67 fof(f11784,plain,(
% 88.53/11.67 ![X0,X1]: (d1(f(X0,a1))|~c(X0)|c(f(X0,f(a1,X1)))|~d2(X1))),
% 88.53/11.67 inference(resolution,[status(thm)],[f1507,f28])).
% 88.53/11.67 fof(f11786,plain,(
% 88.53/11.67 ![X0]: (d1(f(X0,a1))|~c(X0)|c(f(f(X0,a1),a3)))),
% 88.53/11.67 inference(resolution,[status(thm)],[f1507,f11731])).
% 88.53/11.67 fof(f11793,plain,(
% 88.53/11.67 ![X0]: (d1(f(X0,a1))|~c(X0)|c(f(X0,f(a1,a3))))),
% 88.53/11.67 inference(forward_demodulation,[status(thm)],[f12,f11786])).
% 88.53/11.67 fof(f11797,plain,(
% 88.53/11.67 d1(f(a1,f(a2,a3)))|~c(a1)|~c(f(a2,a3))|sQ274_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f9258,f21])).
% 88.53/11.67 fof(f11798,plain,(
% 88.53/11.67 sQ273_spl|~sQ19_spl|~sQ270_spl|sQ274_spl),
% 88.53/11.67 inference(split_clause,[status(thm)],[f11797,f9253,f197,f9224,f9256])).
% 88.53/11.67 fof(f11805,plain,(
% 88.53/11.67 ![X0,X1,X2,X3]: (d1(f(X0,f(X1,X2)))|~c(f(X0,X1))|~c(X2)|c(f(X0,f(f(X1,X2),X3)))|~d2(X3))),
% 88.53/11.67 inference(resolution,[status(thm)],[f32,f28])).
% 88.53/11.67 fof(f11810,plain,(
% 88.53/11.67 ![X0,X1,X2,X3]: (d1(f(X0,f(X1,X2)))|~c(f(X0,X1))|~c(X2)|c(f(X3,f(X0,f(X1,X2))))|~d2(X3))),
% 88.53/11.67 inference(resolution,[status(thm)],[f32,f25])).
% 88.53/11.67 fof(f11813,definition,(
% 88.53/11.67 sQ337_spl <=> (c(f(a1,a2)))),
% 88.53/11.67 introduced(definition,[new_symbols(definition,[sQ337_spl])],[split_symbol_definition])).
% 88.53/11.67 fof(f11815,plain,(
% 88.53/11.67 ~c(f(a1,a2))|sQ337_spl),
% 88.53/11.67 inference(component_clause,[status(thm)],[f11813])).
% 88.53/11.67 fof(f11819,plain,(
% 88.53/11.67 ![X0,X1,X2,X3]: (d1(f(X0,f(X1,X2)))|~c(f(X0,X1))|~c(X2)|c(f(X0,f(X1,f(X2,X3))))|~d2(X3))),
% 88.53/11.67 inference(forward_demodulation,[status(thm)],[f12,f11805])).
% 88.53/11.67 fof(f11837,plain,(
% 88.53/11.67 $false|sQ20_spl),
% 88.53/11.67 inference(forward_subsumption_resolution,[status(thm)],[f227,f11747])).
% 88.53/11.67 fof(f11838,plain,(
% 88.53/11.67 sQ20_spl),
% 88.53/11.67 inference(contradiction_clause,[status(thm)],[f11837])).
% 88.53/11.67 fof(f12296,plain,(
% 88.53/11.67 c(f(a3,f(a1,a1)))|~sQ30_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f11740,f19])).
% 88.53/11.67 fof(f12353,plain,(
% 88.53/11.67 c(f(a3,f(a1,a2)))|~sQ32_spl),
% 88.53/11.67 inference(resolution,[status(thm)],[f11743,f19])).
% 88.53/11.67 fof(f12356,plain,(
% 88.53/11.67 c(f(f(a1,a2),f(a1,a2)))|~sQ32_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f11743,f374])).
% 88.53/11.69 fof(f12369,plain,(
% 88.53/11.69 c(f(a1,f(a2,f(a1,a2))))|~sQ32_spl),
% 88.53/11.69 inference(forward_demodulation,[status(thm)],[f12,f12356])).
% 88.53/11.69 fof(f12748,plain,(
% 88.53/11.69 ![X0]: (~c(X0)|d1(f(a2,X0))|~sQ62_spl)),
% 88.53/11.69 inference(duplicate_literals_removal,[status(thm)],[f838])).
% 88.53/11.69 fof(f12749,plain,(
% 88.53/11.69 ![X0]: (~c(X0)|~sQ60_spl|~sQ62_spl)),
% 88.53/11.69 inference(forward_subsumption_resolution,[status(thm)],[f12748,f821])).
% 88.53/11.69 fof(f12783,plain,(
% 88.53/11.69 $false|~sQ60_spl|~sQ62_spl),
% 88.53/11.69 inference(backward_subsumption_resolution,[status(thm)],[f17,f12749])).
% 88.53/11.69 fof(f12807,definition,(
% 88.53/11.69 ![X4]: (sQ339_spl <=> (~d1(X4)))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ339_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f12808,plain,(
% 88.53/11.69 ![X0]: (~d1(X0)|~sQ339_spl)),
% 88.53/11.69 inference(component_clause,[status(thm)],[f12807])).
% 88.53/11.69 fof(f12818,definition,(
% 88.53/11.69 ![X2]: (sQ342_spl <=> (~d2(X2)))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ342_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f12819,plain,(
% 88.53/11.69 ![X0]: (~d2(X0)|~sQ342_spl)),
% 88.53/11.69 inference(component_clause,[status(thm)],[f12818])).
% 88.53/11.69 fof(f12828,plain,(
% 88.53/11.69 ~sQ60_spl|~sQ62_spl),
% 88.53/11.69 inference(contradiction_clause,[status(thm)],[f12783])).
% 88.53/11.69 fof(f12832,plain,(
% 88.53/11.69 $false|~sQ339_spl|~sQ85_spl),
% 88.53/11.69 inference(backward_subsumption_resolution,[status(thm)],[f1787,f12808])).
% 88.53/11.69 fof(f12841,plain,(
% 88.53/11.69 ~sQ339_spl|~sQ85_spl),
% 88.53/11.69 inference(contradiction_clause,[status(thm)],[f12832])).
% 88.53/11.69 fof(f12842,plain,(
% 88.53/11.69 $false|~sQ342_spl),
% 88.53/11.69 inference(backward_subsumption_resolution,[status(thm)],[f19,f12819])).
% 88.53/11.69 fof(f12852,plain,(
% 88.53/11.69 ~sQ342_spl),
% 88.53/11.69 inference(contradiction_clause,[status(thm)],[f12842])).
% 88.53/11.69 fof(f12854,plain,(
% 88.53/11.69 ![X0]: (d2(f(X0,a1))|d1(f(X0,a1))|~c(X0))),
% 88.53/11.69 inference(resolution,[status(thm)],[f17,f21])).
% 88.53/11.69 fof(f12856,plain,(
% 88.53/11.69 ![X0]: (c(f(X0,a3))|~d2(X0))),
% 88.53/11.69 inference(resolution,[status(thm)],[f25,f19])).
% 88.53/11.69 fof(f12857,plain,(
% 88.53/11.69 ![X0]: (c(f(X0,a2))|~d1(X0))),
% 88.53/11.69 inference(resolution,[status(thm)],[f23,f18])).
% 88.53/11.69 fof(f12894,plain,(
% 88.53/11.69 ~d1(f(a3,a3))),
% 88.53/11.69 inference(resolution,[status(thm)],[f11747,f14])).
% 88.53/11.69 fof(f12900,plain,(
% 88.53/11.69 ~c(a2)|~c(a2)),
% 88.53/11.69 inference(resolution,[status(thm)],[f34,f1578])).
% 88.53/11.69 fof(f12901,plain,(
% 88.53/11.69 ~c(a3)|~c(a3)),
% 88.53/11.69 inference(resolution,[status(thm)],[f34,f11747])).
% 88.53/11.69 fof(f12904,plain,(
% 88.53/11.69 ~sQ26_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f12900,f278])).
% 88.53/11.69 fof(f12905,plain,(
% 88.53/11.69 ~sQ18_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f12901,f194])).
% 88.53/11.69 fof(f12940,plain,(
% 88.53/11.69 ![X0,X1]: (d1(X0)|d2(X0)|d2(f(X1,X0))|d1(f(X1,X0))|d1(X1)|d2(X1))),
% 88.53/11.69 inference(resolution,[status(thm)],[f1527,f13])).
% 88.53/11.69 fof(f12951,plain,(
% 88.53/11.69 $false|~sQ11_spl),
% 88.53/11.69 inference(forward_subsumption_resolution,[status(thm)],[f143,f12894])).
% 88.53/11.69 fof(f12952,plain,(
% 88.53/11.69 ~sQ11_spl),
% 88.53/11.69 inference(contradiction_clause,[status(thm)],[f12951])).
% 88.53/11.69 fof(f13052,plain,(
% 88.53/11.69 ![X0]: (~d2(X0)|~d1(f(X0,a3)))),
% 88.53/11.69 inference(resolution,[status(thm)],[f12856,f14])).
% 88.53/11.69 fof(f13053,plain,(
% 88.53/11.69 ![X0]: (~d2(X0)|~d2(f(X0,a3)))),
% 88.53/11.69 inference(resolution,[status(thm)],[f12856,f15])).
% 88.53/11.69 fof(f13068,plain,(
% 88.53/11.69 ![X0,X1]: (d2(f(X0,f(X1,a1)))|d1(f(f(X0,X1),a1))|~c(f(X0,X1)))),
% 88.53/11.69 inference(paramodulation,[status(thm)],[f12,f12854])).
% 88.53/11.69 fof(f13071,plain,(
% 88.53/11.69 ![X0,X1]: (d2(f(X0,f(X1,a1)))|d1(f(X0,f(X1,a1)))|~c(f(X0,X1)))),
% 88.53/11.69 inference(forward_demodulation,[status(thm)],[f12,f13068])).
% 88.53/11.69 fof(f13074,plain,(
% 88.53/11.69 ![X0,X1,X2]: (d1(f(X0,X1))|~c(X0)|~c(X1)|~d2(X2)|~d2(f(X2,f(X0,X1))))),
% 88.53/11.69 inference(resolution,[status(thm)],[f11659,f15])).
% 88.53/11.69 fof(f13084,plain,(
% 88.53/11.69 ![X0,X1]: (~d2(f(X0,X1))|~d1(f(X0,f(X1,a3))))),
% 88.53/11.69 inference(paramodulation,[status(thm)],[f12,f13052])).
% 88.53/11.69 fof(f13094,plain,(
% 88.53/11.69 ![X0,X1]: (~d2(f(X0,X1))|~d2(f(X0,f(X1,a3))))),
% 88.53/11.69 inference(paramodulation,[status(thm)],[f12,f13053])).
% 88.53/11.69 fof(f13123,plain,(
% 88.53/11.69 ~d1(f(a1,f(a3,a1)))|~sQ56_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f799,f16])).
% 88.53/11.69 fof(f13172,plain,(
% 88.53/11.69 ![X0,X1]: (c(f(X0,f(a1,X1)))|~d2(X1)|d1(f(X0,a1))|~c(X0))),
% 88.53/11.69 inference(resolution,[status(thm)],[f28,f12854])).
% 88.53/11.69 fof(f13220,plain,(
% 88.53/11.69 ~d1(f(a1,f(a3,a2)))|~sQ37_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f557,f14])).
% 88.53/11.69 fof(f13221,plain,(
% 88.53/11.69 ~d2(f(a1,f(a3,a2)))|~sQ37_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f557,f15])).
% 88.53/11.69 fof(f13228,plain,(
% 88.53/11.69 $false|~sQ87_spl|~sQ37_spl),
% 88.53/11.69 inference(forward_subsumption_resolution,[status(thm)],[f13220,f1870])).
% 88.53/11.69 fof(f13229,plain,(
% 88.53/11.69 ~sQ87_spl|~sQ37_spl),
% 88.53/11.69 inference(contradiction_clause,[status(thm)],[f13228])).
% 88.53/11.69 fof(f13230,plain,(
% 88.53/11.69 $false|~sQ88_spl|~sQ37_spl),
% 88.53/11.69 inference(forward_subsumption_resolution,[status(thm)],[f13221,f1873])).
% 88.53/11.69 fof(f13231,plain,(
% 88.53/11.69 ~sQ88_spl|~sQ37_spl),
% 88.53/11.69 inference(contradiction_clause,[status(thm)],[f13230])).
% 88.53/11.69 fof(f13307,plain,(
% 88.53/11.69 ~d2(f(a3,f(a1,a1)))|~sQ30_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f12296,f15])).
% 88.53/11.69 fof(f13343,plain,(
% 88.53/11.69 ~d1(f(a2,f(a2,a3)))|~sQ85_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f2997,f14])).
% 88.53/11.69 fof(f13353,plain,(
% 88.53/11.69 ~d1(f(a2,f(a3,a2)))|~sQ85_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f2226,f14])).
% 88.53/11.69 fof(f13541,plain,(
% 88.53/11.69 ![X0,X1]: (d1(f(X0,a1))|~c(X0)|~d2(X1)|~c(X0)|~c(f(a1,X1)))),
% 88.53/11.69 inference(resolution,[status(thm)],[f11784,f34])).
% 88.53/11.69 fof(f13547,definition,(
% 88.53/11.69 ![X0]: (sQ350_spl <=> (d1(f(X0,a1))|~c(X0)|~c(X0)))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ350_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f13548,plain,(
% 88.53/11.69 ![X0]: (d1(f(X0,a1))|~c(X0)|~c(X0)|~sQ350_spl)),
% 88.53/11.69 inference(component_clause,[status(thm)],[f13547])).
% 88.53/11.69 fof(f13550,definition,(
% 88.53/11.69 ![X1]: (sQ351_spl <=> (~d2(X1)|~c(f(a1,X1))))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ351_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f13551,plain,(
% 88.53/11.69 ![X0]: (~d2(X0)|~c(f(a1,X0))|~sQ351_spl)),
% 88.53/11.69 inference(component_clause,[status(thm)],[f13550])).
% 88.53/11.69 fof(f13553,plain,(
% 88.53/11.69 sQ350_spl|sQ351_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f13541,f13547,f13550])).
% 88.53/11.69 fof(f13560,plain,(
% 88.53/11.69 ![X0]: (d1(f(X0,a1))|~c(X0)|~sQ350_spl)),
% 88.53/11.69 inference(duplicate_literals_removal,[status(thm)],[f13548])).
% 88.53/11.69 fof(f13578,plain,(
% 88.53/11.69 ![X0]: (d1(f(X0,a1))|~c(X0)|~c(X0)|~c(f(a1,a3)))),
% 88.53/11.69 inference(resolution,[status(thm)],[f11793,f34])).
% 88.53/11.69 fof(f13584,plain,(
% 88.53/11.69 sQ350_spl|~sQ71_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f13578,f13547,f1060])).
% 88.53/11.69 fof(f13590,plain,(
% 88.53/11.69 ~c(a1)|~sQ350_spl|~sQ30_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f13560,f11739])).
% 88.53/11.69 fof(f13597,plain,(
% 88.53/11.69 ~sQ19_spl|~sQ350_spl|~sQ30_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f13590,f197,f13547,f316])).
% 88.53/11.69 fof(f13601,plain,(
% 88.53/11.69 ~d2(f(a3,a2))|~sQ351_spl|~sQ37_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f13551,f557])).
% 88.53/11.69 fof(f13602,plain,(
% 88.53/11.69 ~d2(f(a1,a3))|~sQ351_spl|~sQ30_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f13551,f461])).
% 88.53/11.69 fof(f13606,plain,(
% 88.53/11.69 ![X0]: (~d2(X0)|d1(f(a1,X0))|d2(f(a1,X0))|~sQ351_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f13551,f13])).
% 88.53/11.69 fof(f13607,plain,(
% 88.53/11.69 ~sQ42_spl|~sQ351_spl|~sQ37_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f13601,f571,f13550,f500])).
% 88.53/11.69 fof(f13635,plain,(
% 88.53/11.69 ![X0]: (c(f(a1,f(a1,X0)))|~d1(X0)|~sQ29_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f314,f29])).
% 88.53/11.69 fof(f13885,definition,(
% 88.53/11.69 sQ358_spl <=> (d1(f(a2,f(a2,a3))))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ358_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f13886,plain,(
% 88.53/11.69 d1(f(a2,f(a2,a3)))|~sQ358_spl),
% 88.53/11.69 inference(component_clause,[status(thm)],[f13885])).
% 88.53/11.69 fof(f13894,plain,(
% 88.53/11.69 $false|~sQ85_spl|~sQ358_spl),
% 88.53/11.69 inference(forward_subsumption_resolution,[status(thm)],[f13886,f13343])).
% 88.53/11.69 fof(f13895,plain,(
% 88.53/11.69 ~sQ85_spl|~sQ358_spl),
% 88.53/11.69 inference(contradiction_clause,[status(thm)],[f13894])).
% 88.53/11.69 fof(f13901,definition,(
% 88.53/11.69 sQ359_spl <=> (d1(f(a2,f(a3,a2))))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ359_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f13902,plain,(
% 88.53/11.69 d1(f(a2,f(a3,a2)))|~sQ359_spl),
% 88.53/11.69 inference(component_clause,[status(thm)],[f13901])).
% 88.53/11.69 fof(f13909,plain,(
% 88.53/11.69 $false|~sQ85_spl|~sQ359_spl),
% 88.53/11.69 inference(forward_subsumption_resolution,[status(thm)],[f13902,f13353])).
% 88.53/11.69 fof(f13910,plain,(
% 88.53/11.69 ~sQ85_spl|~sQ359_spl),
% 88.53/11.69 inference(contradiction_clause,[status(thm)],[f13909])).
% 88.53/11.69 fof(f13931,plain,(
% 88.53/11.69 ~d1(f(a3,f(a1,a2)))|~sQ32_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f12353,f14])).
% 88.53/11.69 fof(f13932,plain,(
% 88.53/11.69 ~d2(f(a3,f(a1,a2)))|~sQ32_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f12353,f15])).
% 88.53/11.69 fof(f13975,plain,(
% 88.53/11.69 d1(f(a3,a1))|d2(f(a3,a1))|sQ21_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f231,f13])).
% 88.53/11.69 fof(f13976,plain,(
% 88.53/11.69 sQ15_spl|sQ14_spl|sQ21_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f13975,f182,f178,f229])).
% 88.53/11.69 fof(f13988,plain,(
% 88.53/11.69 ~c(a1)|~c(f(a1,a2))|~sQ29_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f2078,f34])).
% 88.53/11.69 fof(f13995,plain,(
% 88.53/11.69 ~sQ19_spl|~sQ337_spl|~sQ29_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f13988,f197,f11813,f313])).
% 88.53/11.69 fof(f14046,definition,(
% 88.53/11.69 ![X0,X1]: (sQ361_spl <=> (~d2(f(X0,X1))|~c(X0)|~d2(X1)))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ361_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f14047,plain,(
% 88.53/11.69 ![X0,X1]: (~d2(f(X0,X1))|~c(X0)|~d2(X1)|~sQ361_spl)),
% 88.53/11.69 inference(component_clause,[status(thm)],[f14046])).
% 88.53/11.69 fof(f14074,plain,(
% 88.53/11.69 $false|~sQ32_spl|~sQ91_spl),
% 88.53/11.69 inference(forward_subsumption_resolution,[status(thm)],[f1938,f13931])).
% 88.53/11.69 fof(f14075,plain,(
% 88.53/11.69 ~sQ32_spl|~sQ91_spl),
% 88.53/11.69 inference(contradiction_clause,[status(thm)],[f14074])).
% 88.53/11.69 fof(f14137,plain,(
% 88.53/11.69 ![X0]: (~c(a1)|~d2(X0)|d1(X0)|d2(X0)|d1(f(a1,X0))|~sQ361_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f14047,f1685])).
% 88.53/11.69 fof(f14155,definition,(
% 88.53/11.69 ![X0]: (sQ365_spl <=> (~d2(X0)|d1(X0)|d2(X0)|d1(f(a1,X0))))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ365_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f14158,plain,(
% 88.53/11.69 ~sQ19_spl|sQ365_spl|~sQ361_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f14137,f197,f14155,f14046])).
% 88.53/11.69 fof(f14162,definition,(
% 88.53/11.69 ![X0]: (sQ366_spl <=> (~c(X0)|d1(f(X0,a1))|d1(X0)|d2(X0)))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ366_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f14163,plain,(
% 88.53/11.69 ![X0]: (~c(X0)|d1(f(X0,a1))|d1(X0)|d2(X0)|~sQ366_spl)),
% 88.53/11.69 inference(component_clause,[status(thm)],[f14162])).
% 88.53/11.69 fof(f14318,plain,(
% 88.53/11.69 ![X0,X1]: (~c(f(X0,X1))|d1(f(a2,f(a2,X0)))|~c(f(a2,a2))|~c(X0)|~d2(X1))),
% 88.53/11.69 inference(resolution,[status(thm)],[f1582,f11819])).
% 88.53/11.69 fof(f14326,definition,(
% 88.53/11.69 ![X0,X1]: (sQ372_spl <=> (~c(f(X0,X1))|d1(f(a2,f(a2,X0)))|~c(X0)|~d2(X1)))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ372_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f14329,plain,(
% 88.53/11.69 sQ372_spl|~sQ27_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f14318,f14326,f301])).
% 88.53/11.69 fof(f14333,plain,(
% 88.53/11.69 ![X0,X1]: (~c(f(X0,X1))|d1(f(a3,f(X0,X1)))|~c(f(a3,X0))|~c(X1)|~d2(a3))),
% 88.53/11.69 inference(resolution,[status(thm)],[f761,f11810])).
% 88.53/11.69 fof(f14334,plain,(
% 88.53/11.69 ![X0,X1]: (~c(f(X0,X1))|d1(f(a3,f(a3,X0)))|~c(f(a3,a3))|~c(X0)|~d2(X1))),
% 88.53/11.69 inference(resolution,[status(thm)],[f761,f11819])).
% 88.53/11.69 fof(f14338,definition,(
% 88.53/11.69 ![X0,X1]: (sQ373_spl <=> (~c(f(X0,X1))|d1(f(a3,f(X0,X1)))|~c(f(a3,X0))|~c(X1)))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ373_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f14341,plain,(
% 88.53/11.69 sQ373_spl|~sQ3_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f14333,f14338,f70])).
% 88.53/11.69 fof(f14342,definition,(
% 88.53/11.69 ![X0,X1]: (sQ374_spl <=> (~c(f(X0,X1))|d1(f(a3,f(a3,X0)))|~c(X0)|~d2(X1)))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ374_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f14345,plain,(
% 88.53/11.69 sQ374_spl|~sQ20_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f14334,f14342,f225])).
% 88.53/11.69 fof(f14362,plain,(
% 88.53/11.69 ![X0]: (~d2(X0)|~c(a1)|d1(f(a2,X0))|d2(f(a2,X0))|~sQ32_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f11769,f37])).
% 88.53/11.69 fof(f14363,plain,(
% 88.53/11.69 ![X0]: (~d2(X0)|~c(a1)|~c(f(a2,X0))|~sQ32_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f11769,f34])).
% 88.53/11.69 fof(f14367,plain,(
% 88.53/11.69 ![X0]: (~d2(X0)|~d2(f(a1,f(a2,X0)))|~sQ32_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f11769,f15])).
% 88.53/11.69 fof(f14372,definition,(
% 88.53/11.69 ![X0]: (sQ375_spl <=> (~d2(X0)|d1(f(a2,X0))|d2(f(a2,X0))))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ375_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f14375,plain,(
% 88.53/11.69 sQ375_spl|~sQ19_spl|~sQ32_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f14362,f14372,f197,f373])).
% 88.53/11.69 fof(f14376,definition,(
% 88.53/11.69 ![X0]: (sQ376_spl <=> (~d2(X0)|~c(f(a2,X0))))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ376_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f14377,plain,(
% 88.53/11.69 ![X0]: (~d2(X0)|~c(f(a2,X0))|~sQ376_spl)),
% 88.53/11.69 inference(component_clause,[status(thm)],[f14376])).
% 88.53/11.69 fof(f14379,plain,(
% 88.53/11.69 sQ376_spl|~sQ19_spl|~sQ32_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f14363,f14376,f197,f373])).
% 88.53/11.69 fof(f14384,plain,(
% 88.53/11.69 ~d2(f(a3,a2))|~sQ376_spl|~sQ85_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f14377,f2226])).
% 88.53/11.69 fof(f14386,plain,(
% 88.53/11.69 ~d2(f(a1,a3))|~sQ376_spl|~sQ22_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f14377,f3941])).
% 88.53/11.69 fof(f14394,plain,(
% 88.53/11.69 ~sQ42_spl|~sQ376_spl|~sQ85_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f14384,f571,f14376,f1786])).
% 88.53/11.69 fof(f14416,plain,(
% 88.53/11.69 ![X0]: (~d2(f(X0,a3))|~c(X0))),
% 88.53/11.69 inference(resolution,[status(thm)],[f56,f128])).
% 88.53/11.69 fof(f14418,plain,(
% 88.53/11.69 ![X0,X1]: (~d2(f(X0,X1))|~c(X0)|~d2(X1)|~d2(a3))),
% 88.53/11.69 inference(resolution,[status(thm)],[f56,f35])).
% 88.53/11.69 fof(f14430,plain,(
% 88.53/11.69 sQ361_spl|~sQ3_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f14418,f14046,f70])).
% 88.53/11.69 fof(f14437,plain,(
% 88.53/11.69 ~sQ38_spl|~sQ376_spl|~sQ22_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f14386,f503,f14376,f256])).
% 88.53/11.69 fof(f14438,plain,(
% 88.53/11.69 ~sQ38_spl|~sQ351_spl|~sQ30_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f13602,f503,f13550,f316])).
% 88.53/11.69 fof(f14446,plain,(
% 88.53/11.69 ![X0]: (d1(f(X0,a1))|d1(X0)|d2(X0)|~sQ366_spl)),
% 88.53/11.69 inference(forward_subsumption_resolution,[status(thm)],[f14163,f13])).
% 88.53/11.69 fof(f14519,plain,(
% 88.53/11.69 ![X0]: (c(f(X0,f(a1,a2)))|~d2(X0)|~sQ32_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f374,f25])).
% 88.53/11.69 fof(f14554,plain,(
% 88.53/11.69 ![X0,X1]: (d2(f(X0,f(X1,a1)))|d1(f(f(X0,X1),a1))|~c(f(X0,X1)))),
% 88.53/11.69 inference(paramodulation,[status(thm)],[f12,f12854])).
% 88.53/11.69 fof(f14556,plain,(
% 88.53/11.69 ![X0,X1]: (d2(f(X0,f(X1,a1)))|d1(f(X0,f(X1,a1)))|~c(f(X0,X1)))),
% 88.53/11.69 inference(forward_demodulation,[status(thm)],[f12,f14554])).
% 88.53/11.69 fof(f14588,definition,(
% 88.53/11.69 ![X0]: (sQ377_spl <=> (~c(X0)|d1(f(X0,a3))|~c(X0)))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ377_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f14589,plain,(
% 88.53/11.69 ![X0]: (~c(X0)|d1(f(X0,a3))|~c(X0)|~sQ377_spl)),
% 88.53/11.69 inference(component_clause,[status(thm)],[f14588])).
% 88.53/11.69 fof(f14592,plain,(
% 88.53/11.69 ![X0]: (~c(X0)|d1(f(X0,a3))|~sQ377_spl)),
% 88.53/11.69 inference(duplicate_literals_removal,[status(thm)],[f14589])).
% 88.53/11.69 fof(f14604,plain,(
% 88.53/11.69 ![X0]: (~c(f(X0,a1))|d1(f(a3,f(X0,a1)))|~d2(a3)|~d2(X0)|~sQ53_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f773,f1621])).
% 88.53/11.69 fof(f14605,plain,(
% 88.53/11.69 ![X0,X1]: (~c(f(X0,X1))|d1(X1)|d2(X1)|d1(f(a3,f(X0,X1)))|~d2(a3)|~d2(X0)|~sQ53_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f773,f1714])).
% 88.53/11.69 fof(f14608,definition,(
% 88.53/11.69 ![X0]: (sQ378_spl <=> (~c(f(X0,a1))|d1(f(a3,f(X0,a1)))|~d2(X0)))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ378_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f14611,plain,(
% 88.53/11.69 sQ378_spl|~sQ3_spl|~sQ53_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f14604,f14608,f70,f772])).
% 88.53/11.69 fof(f14612,definition,(
% 88.53/11.69 ![X0,X1]: (sQ379_spl <=> (~c(f(X0,X1))|d1(X1)|d2(X1)|d1(f(a3,f(X0,X1)))|~d2(X0)))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ379_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f14615,plain,(
% 88.53/11.69 sQ379_spl|~sQ3_spl|~sQ53_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f14605,f14612,f70,f772])).
% 88.53/11.69 fof(f14620,plain,(
% 88.53/11.69 ![X0]: (~c(f(a1,X0))|d1(X0)|~sQ351_spl)),
% 88.53/11.69 inference(backward_subsumption_resolution,[status(thm)],[f52,f13551])).
% 88.53/11.69 fof(f14640,plain,(
% 88.53/11.69 ![X0]: (d1(f(a2,X0))|~d2(X0)|~sQ351_spl|~sQ32_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f14620,f11769])).
% 88.53/11.69 fof(f14698,plain,(
% 88.53/11.69 ![X0,X1,X2,X3,X4]: (d1(f(X0,X1))|~c(X0)|~c(X1)|c(f(f(X2,f(X3,X4)),f(X0,X1)))|d1(f(X2,f(X3,X4)))|~c(f(X2,X3))|~c(X4))),
% 88.53/11.69 inference(resolution,[status(thm)],[f11659,f32])).
% 88.53/11.69 fof(f14699,plain,(
% 88.53/11.69 ![X0,X1,X2,X3]: (d1(f(X0,X1))|~c(X0)|~c(X1)|c(f(f(X2,X3),f(X0,X1)))|d1(X3)|d2(X3)|d1(f(X2,X3))|~c(X2))),
% 88.53/11.69 inference(resolution,[status(thm)],[f11659,f1527])).
% 88.53/11.69 fof(f14709,plain,(
% 88.53/11.69 ![X0,X1,X2,X3,X4]: (d1(f(X0,X1))|~c(X0)|~c(X1)|c(f(X2,f(f(X3,X4),f(X0,X1))))|d1(f(X2,f(X3,X4)))|~c(f(X2,X3))|~c(X4))),
% 88.53/11.69 inference(forward_demodulation,[status(thm)],[f12,f14698])).
% 88.53/11.69 fof(f14710,plain,(
% 88.53/11.69 ![X0,X1,X2,X3,X4]: (d1(f(X0,X1))|~c(X0)|~c(X1)|c(f(X2,f(X3,f(X4,f(X0,X1)))))|d1(f(X2,f(X3,X4)))|~c(f(X2,X3))|~c(X4))),
% 88.53/11.69 inference(forward_demodulation,[status(thm)],[f12,f14709])).
% 88.53/11.69 fof(f14711,plain,(
% 88.53/11.69 ![X0,X1,X2,X3]: (d1(f(X0,X1))|~c(X0)|~c(X1)|c(f(X2,f(X3,f(X0,X1))))|d1(X3)|d2(X3)|d1(f(X2,X3))|~c(X2))),
% 88.53/11.69 inference(forward_demodulation,[status(thm)],[f12,f14699])).
% 88.53/11.69 fof(f14713,plain,(
% 88.53/11.69 d1(f(a2,f(a1,a2)))|~sQ351_spl|~sQ32_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f14640,f374])).
% 88.53/11.69 fof(f15329,plain,(
% 88.53/11.69 d1(f(a3,f(a1,a1)))|~c(f(a3,a1))|~c(a1)|~sQ30_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f13307,f32])).
% 88.53/11.69 fof(f15334,plain,(
% 88.53/11.69 sQ233_spl|~sQ21_spl|~sQ19_spl|~sQ30_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f15329,f6957,f229,f197,f316])).
% 88.53/11.69 fof(f15621,plain,(
% 88.53/11.69 ![X0,X1]: (d1(f(X0,a1))|~c(X0)|~c(a1)|~d2(X1)|d1(f(X1,f(X0,a1)))|~d2(X1)|~d2(X0))),
% 88.53/11.69 inference(resolution,[status(thm)],[f13074,f1621])).
% 88.53/11.69 fof(f15635,definition,(
% 88.53/11.69 ![X0,X1]: (sQ408_spl <=> (d1(f(X0,a1))|~c(X0)|~d2(X1)|d1(f(X1,f(X0,a1)))|~d2(X1)|~d2(X0)))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ408_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f15638,plain,(
% 88.53/11.69 sQ408_spl|~sQ19_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f15621,f15635,f197])).
% 88.53/11.69 fof(f15824,plain,(
% 88.53/11.69 ![X0]: (~d2(X0)|d1(f(a1,a1))|~c(a1)|d1(f(a1,X0))|~sQ351_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f13172,f14620])).
% 88.53/11.69 fof(f15825,plain,(
% 88.53/11.69 ![X0]: (~d2(X0)|d1(f(a1,a1))|~c(a1)|~d2(f(a1,X0))|~sQ351_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f13172,f13551])).
% 88.53/11.69 fof(f15837,definition,(
% 88.53/11.69 ![X0]: (sQ409_spl <=> (~d2(X0)|~d2(f(a1,X0))))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ409_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f15838,plain,(
% 88.53/11.69 ![X0]: (~d2(X0)|~d2(f(a1,X0))|~sQ409_spl)),
% 88.53/11.69 inference(component_clause,[status(thm)],[f15837])).
% 88.53/11.69 fof(f15842,definition,(
% 88.53/11.69 ![X0]: (sQ410_spl <=> (~d2(X0)|d1(f(a1,X0))))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ410_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f15843,plain,(
% 88.53/11.69 ![X0]: (~d2(X0)|d1(f(a1,X0))|~sQ410_spl)),
% 88.53/11.69 inference(component_clause,[status(thm)],[f15842])).
% 88.53/11.69 fof(f15845,plain,(
% 88.53/11.69 sQ410_spl|sQ29_spl|~sQ19_spl|~sQ351_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f15824,f15842,f313,f197,f13550])).
% 88.53/11.69 fof(f15846,plain,(
% 88.53/11.69 sQ409_spl|sQ29_spl|~sQ19_spl|~sQ351_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f15825,f15837,f313,f197,f13550])).
% 88.53/11.69 fof(f15904,plain,(
% 88.53/11.69 d1(a1)|d2(a1)|~sQ366_spl|~sQ30_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f14446,f11739])).
% 88.53/11.69 fof(f15912,plain,(
% 88.53/11.69 sQ7_spl|sQ5_spl|~sQ366_spl|~sQ30_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f15904,f92,f85,f14162,f316])).
% 88.53/11.69 fof(f15918,plain,(
% 88.53/11.69 ![X0]: (d1(f(X0,a1))|d2(f(X0,a1))|d1(f(a3,f(X0,a1)))|~d2(a3)|~d2(X0)|~sQ335_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f11577,f1621])).
% 88.53/11.69 fof(f15919,plain,(
% 88.53/11.69 ![X0,X1]: (d1(f(X0,X1))|d2(f(X0,X1))|d1(X1)|d2(X1)|d1(f(a3,f(X0,X1)))|~d2(a3)|~d2(X0)|~sQ335_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f11577,f1714])).
% 88.53/11.69 fof(f15925,definition,(
% 88.53/11.69 ![X0]: (sQ415_spl <=> (d1(f(X0,a1))|d2(f(X0,a1))|d1(f(a3,f(X0,a1)))|~d2(X0)))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ415_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f15928,plain,(
% 88.53/11.69 sQ415_spl|~sQ3_spl|~sQ335_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f15918,f15925,f70,f11576])).
% 88.53/11.69 fof(f15929,definition,(
% 88.53/11.69 ![X0,X1]: (sQ416_spl <=> (d1(f(X0,X1))|d2(f(X0,X1))|d1(X1)|d2(X1)|d1(f(a3,f(X0,X1)))|~d2(X0)))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ416_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f15932,plain,(
% 88.53/11.69 sQ416_spl|~sQ3_spl|~sQ335_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f15919,f15929,f70,f11576])).
% 88.53/11.69 fof(f15935,plain,(
% 88.53/11.69 ![X0]: (~d2(X0)|~d2(f(a1,X0))|~sQ22_spl|~sQ376_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f11771,f14377])).
% 88.53/11.69 fof(f15971,definition,(
% 88.53/11.69 ![X0]: (sQ417_spl <=> (~d2(X0)|~c(f(X0,a1))))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ417_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f15972,plain,(
% 88.53/11.69 ![X0]: (~d2(X0)|~c(f(X0,a1))|~sQ417_spl)),
% 88.53/11.69 inference(component_clause,[status(thm)],[f15971])).
% 88.53/11.69 fof(f16130,plain,(
% 88.53/11.69 ![X0]: (d1(X0)|~c(f(X0,a1))|~sQ417_spl)),
% 88.53/11.69 inference(backward_subsumption_resolution,[status(thm)],[f2130,f15972])).
% 88.53/11.69 fof(f16250,plain,(
% 88.53/11.69 ![X0]: (~d2(X0)|d1(f(a2,X0))|d2(f(a2,X0))|d1(f(a1,f(a2,X0)))|~c(a1)|~sQ32_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f14367,f1527])).
% 88.53/11.69 fof(f16260,definition,(
% 88.53/11.69 ![X0]: (sQ420_spl <=> (~d2(X0)|d1(f(a2,X0))|d2(f(a2,X0))|d1(f(a1,f(a2,X0)))))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ420_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f16264,plain,(
% 88.53/11.69 sQ420_spl|~sQ19_spl|~sQ32_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f16250,f16260,f197,f373])).
% 88.53/11.69 fof(f16284,definition,(
% 88.53/11.69 ![X0]: (sQ422_spl <=> (~d1(X0)|~c(f(a1,X0))))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ422_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f16285,plain,(
% 88.53/11.69 ![X0]: (~d1(X0)|~c(f(a1,X0))|~sQ422_spl)),
% 88.53/11.69 inference(component_clause,[status(thm)],[f16284])).
% 88.53/11.69 fof(f16414,plain,(
% 88.53/11.69 ~d2(f(a1,f(a2,a3)))|~sQ32_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f2043,f15])).
% 88.53/11.69 fof(f16475,plain,(
% 88.53/11.69 ![X0]: (~d1(X0)|~d2(f(a3,X0))|~sQ85_spl|~sQ376_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f2220,f14377])).
% 88.53/11.69 fof(f16505,plain,(
% 88.53/11.69 ~d1(f(a2,a3))|~sQ85_spl|~sQ376_spl|~sQ298_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f16475,f9936])).
% 88.53/11.69 fof(f16507,plain,(
% 88.53/11.69 ![X0]: (~d1(f(X0,a1))|d1(f(a3,f(X0,a1)))|~d2(a3)|~d2(X0)|~sQ85_spl|~sQ376_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f16475,f1621])).
% 88.53/11.69 fof(f16508,plain,(
% 88.53/11.69 ![X0,X1]: (~d1(f(X0,X1))|d1(X1)|d2(X1)|d1(f(a3,f(X0,X1)))|~d2(a3)|~d2(X0)|~sQ85_spl|~sQ376_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f16475,f1714])).
% 88.53/11.69 fof(f16512,plain,(
% 88.53/11.69 ~sQ85_spl|~sQ376_spl|~sQ298_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f16505,f1786,f14376,f9935])).
% 88.53/11.69 fof(f16514,definition,(
% 88.53/11.69 ![X0]: (sQ427_spl <=> (~d1(f(X0,a1))|d1(f(a3,f(X0,a1)))|~d2(X0)))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ427_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f16517,plain,(
% 88.53/11.69 sQ427_spl|~sQ3_spl|~sQ85_spl|~sQ376_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f16507,f16514,f70,f1786,f14376])).
% 88.53/11.69 fof(f16518,definition,(
% 88.53/11.69 ![X0,X1]: (sQ428_spl <=> (~d1(f(X0,X1))|d1(X1)|d2(X1)|d1(f(a3,f(X0,X1)))|~d2(X0)))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ428_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f16521,plain,(
% 88.53/11.69 sQ428_spl|~sQ3_spl|~sQ85_spl|~sQ376_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f16508,f16518,f70,f1786,f14376])).
% 88.53/11.69 fof(f16533,plain,(
% 88.53/11.69 d1(f(a1,a2))|d2(f(a1,a2))|sQ337_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f11815,f13])).
% 88.53/11.69 fof(f16534,plain,(
% 88.53/11.69 sQ31_spl|sQ32_spl|sQ337_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f16533,f370,f373,f11813])).
% 88.53/11.69 fof(f17003,plain,(
% 88.53/11.69 ![X0]: (d1(X0)|d2(f(a1,X0))|d1(f(a1,X0))|~sQ410_spl)),
% 88.53/11.69 inference(forward_subsumption_resolution,[status(thm)],[f1685,f15843])).
% 88.53/11.69 fof(f17007,plain,(
% 88.53/11.69 d1(a3)|d1(f(a1,a3))|~c(a1)|~sQ410_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f17003,f14416])).
% 88.53/11.69 fof(f17023,plain,(
% 88.53/11.69 sQ2_spl|sQ37_spl|~sQ19_spl|~sQ410_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f17007,f67,f500,f197,f15842])).
% 88.53/11.69 fof(f17025,definition,(
% 88.53/11.69 ![X0]: (sQ433_spl <=> (d1(X0)|d1(f(a1,X0))|~d2(X0)))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ433_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f17026,plain,(
% 88.53/11.69 ![X0]: (d1(X0)|d1(f(a1,X0))|~d2(X0)|~sQ433_spl)),
% 88.53/11.69 inference(component_clause,[status(thm)],[f17025])).
% 88.53/11.69 fof(f17534,definition,(
% 88.53/11.69 ![X0]: (sQ436_spl <=> (~d1(X0)|~c(f(X0,a2))))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ436_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f17535,plain,(
% 88.53/11.69 ![X0]: (~d1(X0)|~c(f(X0,a2))|~sQ436_spl)),
% 88.53/11.69 inference(component_clause,[status(thm)],[f17534])).
% 88.53/11.69 fof(f17547,plain,(
% 88.53/11.69 ![X0]: (~d1(X0)|~sQ436_spl)),
% 88.53/11.69 inference(forward_subsumption_resolution,[status(thm)],[f17535,f12857])).
% 88.53/11.69 fof(f17571,plain,(
% 88.53/11.69 $false|~sQ436_spl|~sQ24_spl),
% 88.53/11.69 inference(backward_subsumption_resolution,[status(thm)],[f265,f17547])).
% 88.53/11.69 fof(f17591,plain,(
% 88.53/11.69 ~sQ436_spl|~sQ24_spl),
% 88.53/11.69 inference(contradiction_clause,[status(thm)],[f17571])).
% 88.53/11.69 fof(f18031,plain,(
% 88.53/11.69 ![X0]: (~d1(X0)|d1(f(a3,X0))|~sQ37_spl|~sQ351_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f521,f14620])).
% 88.53/11.69 fof(f18054,plain,(
% 88.53/11.69 ~d1(f(a3,a1))|~sQ37_spl|~sQ351_spl|sQ16_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f18031,f188])).
% 88.53/11.69 fof(f18061,plain,(
% 88.53/11.69 ~sQ15_spl|~sQ37_spl|~sQ351_spl|sQ16_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f18054,f182,f500,f13550,f186])).
% 88.53/11.69 fof(f18063,plain,(
% 88.53/11.69 ![X0]: (d1(f(a1,X0))|~d2(X0)|~sQ433_spl)),
% 88.53/11.69 inference(forward_subsumption_resolution,[status(thm)],[f17026,f16])).
% 88.53/11.69 fof(f18064,plain,(
% 88.53/11.69 sQ409_spl|~sQ22_spl|~sQ376_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f15935,f15837,f256,f14376])).
% 88.53/11.69 fof(f18178,plain,(
% 88.53/11.69 ~c(a1)|sQ37_spl|~sQ377_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f502,f14592])).
% 88.53/11.69 fof(f18179,plain,(
% 88.53/11.69 ~sQ19_spl|sQ37_spl|~sQ377_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f18178,f197,f500,f14588])).
% 88.53/11.69 fof(f18213,plain,(
% 88.53/11.69 d1(f(a1,a3))|~sQ433_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f18063,f19])).
% 88.53/11.69 fof(f18215,plain,(
% 88.53/11.69 sQ37_spl|~sQ433_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f18213,f500,f17025])).
% 88.53/11.69 fof(f18220,plain,(
% 88.53/11.69 ![X0]: (~c(X0)|~d2(f(X0,a1))|~sQ350_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f13560,f16])).
% 88.53/11.69 fof(f18227,plain,(
% 88.53/11.69 d2(f(a1,f(a3,a1)))|d1(f(a1,f(a3,a1)))|~sQ71_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f14556,f1061])).
% 88.53/11.69 fof(f18242,plain,(
% 88.53/11.69 sQ56_spl|sQ57_spl|~sQ71_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f18227,f798,f802,f1060])).
% 88.53/11.69 fof(f18494,definition,(
% 88.53/11.69 ![X0]: (sQ441_spl <=> (~d1(X0)|~c(f(a2,X0))))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ441_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f18495,plain,(
% 88.53/11.69 ![X0]: (~d1(X0)|~c(f(a2,X0))|~sQ441_spl)),
% 88.53/11.69 inference(component_clause,[status(thm)],[f18494])).
% 88.53/11.69 fof(f18507,plain,(
% 88.53/11.69 ~d1(a2)|~sQ441_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f18495,f1578])).
% 88.53/11.69 fof(f18514,plain,(
% 88.53/11.69 ~sQ0_spl|~sQ441_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f18507,f59,f18494])).
% 88.53/11.69 fof(f18538,plain,(
% 88.53/11.69 ![X0,X1,X2]: (d1(f(X0,X1))|~c(X0)|~c(X1)|d1(f(a2,f(a2,X2)))|~c(f(a2,a2))|~c(X2)|~c(f(X2,f(X0,X1))))),
% 88.53/11.69 inference(resolution,[status(thm)],[f14710,f1582])).
% 88.53/11.69 fof(f18539,plain,(
% 88.53/11.69 ![X0,X1,X2]: (d1(f(X0,X1))|~c(X0)|~c(X1)|d1(f(a3,f(a3,X2)))|~c(f(a3,a3))|~c(X2)|~c(f(X2,f(X0,X1))))),
% 88.53/11.69 inference(resolution,[status(thm)],[f14710,f761])).
% 88.53/11.69 fof(f18552,definition,(
% 88.53/11.69 ![X0,X1,X2]: (sQ442_spl <=> (d1(f(X0,X1))|~c(X0)|~c(X1)|d1(f(a2,f(a2,X2)))|~c(X2)|~c(f(X2,f(X0,X1)))))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ442_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f18555,plain,(
% 88.53/11.69 sQ442_spl|~sQ27_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f18538,f18552,f301])).
% 88.53/11.69 fof(f18556,definition,(
% 88.53/11.69 ![X0,X1,X2]: (sQ443_spl <=> (d1(f(X0,X1))|~c(X0)|~c(X1)|d1(f(a3,f(a3,X2)))|~c(X2)|~c(f(X2,f(X0,X1)))))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ443_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f18559,plain,(
% 88.53/11.69 sQ443_spl|~sQ20_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f18539,f18556,f225])).
% 88.53/11.69 fof(f18623,plain,(
% 88.53/11.69 ![X0,X1,X2]: (d1(f(X0,X1))|~c(X0)|~c(X1)|d1(X2)|d2(X2)|d1(f(a1,X2))|~c(a1)|d1(f(X2,f(X0,X1)))|d2(f(X2,f(X0,X1))))),
% 88.53/11.69 inference(resolution,[status(thm)],[f14711,f52])).
% 88.53/11.69 fof(f18637,definition,(
% 88.53/11.69 ![X0,X1,X2]: (sQ445_spl <=> (d1(f(X0,X1))|~c(X0)|~c(X1)|d1(X2)|d2(X2)|d1(f(a1,X2))|d1(f(X2,f(X0,X1)))|d2(f(X2,f(X0,X1)))))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ445_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f18640,plain,(
% 88.53/11.69 sQ445_spl|~sQ19_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f18623,f18637,f197])).
% 88.53/11.69 fof(f18825,plain,(
% 88.53/11.69 c(f(a3,f(a1,a2)))|~sQ32_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f14519,f19])).
% 88.53/11.69 fof(f18867,definition,(
% 88.53/11.69 ![X0]: (sQ448_spl <=> (~c(X0)|~c(X0)))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ448_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f18868,plain,(
% 88.53/11.69 ![X0]: (~c(X0)|~c(X0)|~sQ448_spl)),
% 88.53/11.69 inference(component_clause,[status(thm)],[f18867])).
% 88.53/11.69 fof(f18875,plain,(
% 88.53/11.69 ![X0]: (~c(X0)|~sQ448_spl)),
% 88.53/11.69 inference(duplicate_literals_removal,[status(thm)],[f18868])).
% 88.53/11.69 fof(f18956,plain,(
% 88.53/11.69 ![X0]: (~d2(X0)|~sQ448_spl)),
% 88.53/11.69 inference(backward_subsumption_resolution,[status(thm)],[f12856,f18875])).
% 88.53/11.69 fof(f18987,plain,(
% 88.53/11.69 sQ342_spl|~sQ448_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f18956,f12818,f18867])).
% 88.53/11.69 fof(f19005,plain,(
% 88.53/11.69 ![X0,X1]: (~d1(X0)|~d1(X1)|~d2(f(X0,X1)))),
% 88.53/11.69 inference(resolution,[status(thm)],[f23,f15])).
% 88.53/11.69 fof(f19006,plain,(
% 88.53/11.69 ![X0,X1]: (~d1(X0)|~d1(X1)|~d1(f(X0,X1)))),
% 88.53/11.69 inference(resolution,[status(thm)],[f23,f14])).
% 88.53/11.69 fof(f19020,plain,(
% 88.53/11.69 ~d1(a1)|~d1(a2)|~sQ32_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f2052,f23])).
% 88.53/11.69 fof(f19021,plain,(
% 88.53/11.69 ~sQ7_spl|~sQ0_spl|~sQ32_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f19020,f92,f59,f373])).
% 88.53/11.69 fof(f19035,plain,(
% 88.53/11.69 d1(f(a2,a1))|d2(f(a2,a1))|sQ28_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f13,f307])).
% 88.53/11.69 fof(f19046,plain,(
% 88.53/11.69 sQ23_spl|sQ22_spl|sQ28_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f19035,f260,f256,f305])).
% 88.53/11.69 fof(f19050,plain,(
% 88.53/11.69 ~sQ92_spl|~sQ32_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f13932,f1940,f373])).
% 88.53/11.69 fof(f19155,plain,(
% 88.53/11.69 ~d1(f(a2,a2))),
% 88.53/11.69 inference(resolution,[status(thm)],[f1578,f14])).
% 88.53/11.69 fof(f19184,plain,(
% 88.53/11.69 ![X0,X1]: (~c(X0)|~c(X1)|~d1(X0)|~d1(X1))),
% 88.53/11.69 inference(resolution,[status(thm)],[f34,f23])).
% 88.53/11.69 fof(f19189,plain,(
% 88.53/11.69 sQ6_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f19184,f89])).
% 88.53/11.69 fof(f19246,plain,(
% 88.53/11.69 ![X0]: (~d2(X0)|~d1(a2)|~d1(X0)|~sQ376_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f14377,f23])).
% 88.53/11.69 fof(f19248,plain,(
% 88.53/11.69 sQ59_spl|~sQ0_spl|~sQ376_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f19246,f816,f59,f14376])).
% 88.53/11.69 fof(f19467,plain,(
% 88.53/11.69 ![X0,X1,X2]: (d1(f(X0,f(X1,X2)))|~c(f(X0,X1))|~c(X2)|~d1(X0)|~d1(f(X1,X2)))),
% 88.53/11.69 inference(resolution,[status(thm)],[f32,f19005])).
% 88.53/11.69 fof(f19469,plain,(
% 88.53/11.69 ![X0,X1,X2]: (d1(f(X0,f(X1,X2)))|~c(f(X0,X1))|~c(X2)|c(f(f(X0,f(X1,X2)),a3)))),
% 88.53/11.69 inference(resolution,[status(thm)],[f32,f12856])).
% 88.53/11.69 fof(f19474,plain,(
% 88.53/11.69 ![X0,X1,X2]: (~c(f(X0,X1))|~c(X2)|~d1(X0)|~d1(f(X1,X2)))),
% 88.53/11.69 inference(forward_subsumption_resolution,[status(thm)],[f19467,f19006])).
% 88.53/11.69 fof(f19476,plain,(
% 88.53/11.69 ![X0,X1,X2]: (d1(f(X0,f(X1,X2)))|~c(f(X0,X1))|~c(X2)|c(f(X0,f(f(X1,X2),a3))))),
% 88.53/11.69 inference(forward_demodulation,[status(thm)],[f12,f19469])).
% 88.53/11.69 fof(f19477,plain,(
% 88.53/11.69 ![X0,X1,X2]: (d1(f(X0,f(X1,X2)))|~c(f(X0,X1))|~c(X2)|c(f(X0,f(X1,f(X2,a3)))))),
% 88.53/11.69 inference(forward_demodulation,[status(thm)],[f12,f19476])).
% 88.53/11.69 fof(f19793,plain,(
% 88.53/11.69 d2(f(a2,f(a1,a1)))|d1(f(a2,f(a1,a1)))|~sQ28_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f13071,f306])).
% 88.53/11.69 fof(f19813,definition,(
% 88.53/11.69 sQ455_spl <=> (d2(f(a2,f(a1,a1))))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ455_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f19814,plain,(
% 88.53/11.69 d2(f(a2,f(a1,a1)))|~sQ455_spl),
% 88.53/11.69 inference(component_clause,[status(thm)],[f19813])).
% 88.53/11.69 fof(f19816,definition,(
% 88.53/11.69 sQ456_spl <=> (d1(f(a2,f(a1,a1))))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ456_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f19817,plain,(
% 88.53/11.69 d1(f(a2,f(a1,a1)))|~sQ456_spl),
% 88.53/11.69 inference(component_clause,[status(thm)],[f19816])).
% 88.53/11.69 fof(f19819,plain,(
% 88.53/11.69 sQ455_spl|sQ456_spl|~sQ28_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f19793,f19813,f19816,f305])).
% 88.53/11.69 fof(f19936,plain,(
% 88.53/11.69 ![X0]: (d1(a1)|d2(a1)|d1(f(X0,a1))|d1(X0)|d2(X0)|~c(X0)|~sQ350_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f12940,f18220])).
% 88.53/11.69 fof(f19975,plain,(
% 88.53/11.69 sQ7_spl|sQ5_spl|sQ366_spl|~sQ350_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f19936,f92,f85,f14162,f13547])).
% 88.53/11.69 fof(f20196,plain,(
% 88.53/11.69 ~d1(a2)|~d1(f(a1,a1))|~sQ455_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f19814,f19005])).
% 88.53/11.69 fof(f20212,plain,(
% 88.53/11.69 ~sQ0_spl|~sQ29_spl|~sQ455_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f20196,f59,f313,f19813])).
% 88.53/11.69 fof(f20235,plain,(
% 88.53/11.69 ~d1(a2)|~d1(f(a1,a1))|~sQ456_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f19817,f19006])).
% 88.53/11.69 fof(f20239,plain,(
% 88.53/11.69 ~sQ0_spl|~sQ29_spl|~sQ456_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f20235,f59,f313,f19816])).
% 88.53/11.69 fof(f20637,plain,(
% 88.53/11.69 $false|~sQ13_spl),
% 88.53/11.69 inference(forward_subsumption_resolution,[status(thm)],[f156,f19155])).
% 88.53/11.69 fof(f20638,plain,(
% 88.53/11.69 ~sQ13_spl),
% 88.53/11.69 inference(contradiction_clause,[status(thm)],[f20637])).
% 88.53/11.69 fof(f20725,plain,(
% 88.53/11.69 ![X0]: (d1(X0)|d2(X0)|d2(f(a1,X0))|d1(f(a1,X0)))),
% 88.53/11.69 inference(resolution,[status(thm)],[f1527,f17])).
% 88.53/11.69 fof(f21285,plain,(
% 88.53/11.69 ![X0]: (~d1(X0)|~c(a1)|~c(f(a1,X0))|~sQ29_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f13635,f34])).
% 88.53/11.69 fof(f21296,plain,(
% 88.53/11.69 sQ422_spl|~sQ19_spl|~sQ29_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f21285,f16284,f197,f313])).
% 88.53/11.69 fof(f21457,definition,(
% 88.53/11.69 ![X0]: (sQ467_spl <=> (~c(X0)))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ467_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f21458,plain,(
% 88.53/11.69 ![X0]: (~c(X0)|~sQ467_spl)),
% 88.53/11.69 inference(component_clause,[status(thm)],[f21457])).
% 88.53/11.69 fof(f21469,plain,(
% 88.53/11.69 $false|~sQ467_spl),
% 88.53/11.69 inference(backward_subsumption_resolution,[status(thm)],[f17,f21458])).
% 88.53/11.69 fof(f21487,plain,(
% 88.53/11.69 ~sQ467_spl),
% 88.53/11.69 inference(contradiction_clause,[status(thm)],[f21469])).
% 88.53/11.69 fof(f21495,plain,(
% 88.53/11.69 ![X0,X1]: (~d2(X0)|~d2(X1)|~d2(f(X0,X1)))),
% 88.53/11.69 inference(resolution,[status(thm)],[f25,f15])).
% 88.53/11.69 fof(f21496,plain,(
% 88.53/11.69 ![X0,X1]: (~d2(X0)|~d2(X1)|~d1(f(X0,X1)))),
% 88.53/11.69 inference(resolution,[status(thm)],[f25,f14])).
% 88.53/11.69 fof(f21541,plain,(
% 88.53/11.69 ~d2(a2)|~d2(a3)|sQ270_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f9226,f25])).
% 88.53/11.69 fof(f21543,plain,(
% 88.53/11.69 ~sQ1_spl|~sQ3_spl|sQ270_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f21541,f62,f70,f9224])).
% 88.53/11.69 fof(f21621,plain,(
% 88.53/11.69 d1(f(f(a1,a3),a1))|~sQ350_spl|~sQ71_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f13560,f1061])).
% 88.53/11.69 fof(f21627,plain,(
% 88.53/11.69 d1(f(a1,f(a3,a1)))|~sQ350_spl|~sQ71_spl),
% 88.53/11.69 inference(forward_demodulation,[status(thm)],[f12,f21621])).
% 88.53/11.69 fof(f21636,plain,(
% 88.53/11.69 ![X0,X1]: (~c(X0)|~c(X1)|~d2(X0)|~d2(X1))),
% 88.53/11.69 inference(resolution,[status(thm)],[f34,f25])).
% 88.53/11.69 fof(f21643,plain,(
% 88.53/11.69 sQ4_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f21636,f82])).
% 88.53/11.69 fof(f21713,plain,(
% 88.53/11.69 ~c(f(a1,f(a3,a2)))|~sQ41_spl|~sQ422_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f569,f16285])).
% 88.53/11.69 fof(f22243,plain,(
% 88.53/11.69 $false|~sQ56_spl|~sQ350_spl|~sQ71_spl),
% 88.53/11.69 inference(forward_subsumption_resolution,[status(thm)],[f21627,f13123])).
% 88.53/11.69 fof(f22244,plain,(
% 88.53/11.69 ~sQ56_spl|~sQ350_spl|~sQ71_spl),
% 88.53/11.69 inference(contradiction_clause,[status(thm)],[f22243])).
% 88.53/11.69 fof(f22399,plain,(
% 88.53/11.69 d1(f(a1,f(a3,a2)))|d2(f(a1,f(a3,a2)))|~sQ41_spl|~sQ422_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f21713,f13])).
% 88.53/11.69 fof(f22401,plain,(
% 88.53/11.69 sQ87_spl|sQ88_spl|~sQ41_spl|~sQ422_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f22399,f1869,f1872,f568,f16284])).
% 88.53/11.69 fof(f23717,definition,(
% 88.53/11.69 ![X0]: (sQ480_spl <=> (d1(X0)|~c(X0)))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ480_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f23718,plain,(
% 88.53/11.69 ![X0]: (d1(X0)|~c(X0)|~sQ480_spl)),
% 88.53/11.69 inference(component_clause,[status(thm)],[f23717])).
% 88.53/11.69 fof(f23751,plain,(
% 88.53/11.69 ![X0]: (~c(X0)|~sQ480_spl)),
% 88.53/11.69 inference(forward_subsumption_resolution,[status(thm)],[f23718,f14])).
% 88.53/11.69 fof(f23770,plain,(
% 88.53/11.69 $false|~sQ480_spl),
% 88.53/11.69 inference(backward_subsumption_resolution,[status(thm)],[f17,f23751])).
% 88.53/11.69 fof(f23805,plain,(
% 88.53/11.69 ~sQ480_spl),
% 88.53/11.69 inference(contradiction_clause,[status(thm)],[f23770])).
% 88.53/11.69 fof(f24289,plain,(
% 88.53/11.69 ![X0,X1,X2]: (d1(f(X0,f(X1,X2)))|~c(f(X0,X1))|~c(X2)|~d2(X0)|~d2(f(X1,X2)))),
% 88.53/11.69 inference(resolution,[status(thm)],[f32,f21495])).
% 88.53/11.69 fof(f24290,plain,(
% 88.53/11.69 ![X0,X1,X2]: (d1(f(X0,f(X1,X2)))|~c(f(X0,X1))|~c(X2)|~d1(X0)|~d1(f(X1,X2)))),
% 88.53/11.69 inference(resolution,[status(thm)],[f32,f19005])).
% 88.53/11.69 fof(f24300,plain,(
% 88.53/11.69 ![X0,X1,X2]: (~c(f(X0,X1))|~c(X2)|~d2(X0)|~d2(f(X1,X2)))),
% 88.53/11.69 inference(forward_subsumption_resolution,[status(thm)],[f24289,f21496])).
% 88.53/11.69 fof(f24301,plain,(
% 88.53/11.69 ![X0,X1,X2]: (~c(f(X0,X1))|~c(X2)|~d1(X0)|~d1(f(X1,X2)))),
% 88.53/11.69 inference(forward_subsumption_resolution,[status(thm)],[f24290,f19006])).
% 88.53/11.69 fof(f25462,definition,(
% 88.53/11.69 ![X0]: (sQ486_spl <=> (~d2(X0)|~c(f(a3,X0))))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ486_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f25463,plain,(
% 88.53/11.69 ![X0]: (~d2(X0)|~c(f(a3,X0))|~sQ486_spl)),
% 88.53/11.69 inference(component_clause,[status(thm)],[f25462])).
% 88.53/11.69 fof(f25478,plain,(
% 88.53/11.69 ![X0,X1]: (~c(f(X0,X1))|~c(a1)|~d1(X0)|~c(X1)|~sQ350_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f19474,f13560])).
% 88.53/11.69 fof(f25481,definition,(
% 88.53/11.69 ![X0]: (sQ487_spl <=> (~c(f(X0,a1))|~d1(X0)))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ487_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f25482,plain,(
% 88.53/11.69 ![X0]: (~c(f(X0,a1))|~d1(X0)|~sQ487_spl)),
% 88.53/11.69 inference(component_clause,[status(thm)],[f25481])).
% 88.53/11.69 fof(f25494,definition,(
% 88.53/11.69 ![X0,X1]: (sQ489_spl <=> (~c(f(X0,X1))|~d1(X0)|~c(X1)))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ489_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f25495,plain,(
% 88.53/11.69 ![X0,X1]: (~c(f(X0,X1))|~d1(X0)|~c(X1)|~sQ489_spl)),
% 88.53/11.69 inference(component_clause,[status(thm)],[f25494])).
% 88.53/11.69 fof(f25497,plain,(
% 88.53/11.69 sQ489_spl|~sQ19_spl|~sQ350_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f25478,f25494,f197,f13547])).
% 88.53/11.69 fof(f25508,plain,(
% 88.53/11.69 ![X0]: (d1(f(a3,f(a3,X0)))|~c(f(a3,a3))|~c(X0)|~c(f(X0,a3)))),
% 88.53/11.69 inference(resolution,[status(thm)],[f19477,f761])).
% 88.53/11.69 fof(f25510,plain,(
% 88.53/11.69 ![X0]: (d1(f(a2,f(a2,X0)))|~c(f(a2,a2))|~c(X0)|~c(f(X0,a3)))),
% 88.53/11.69 inference(resolution,[status(thm)],[f19477,f1582])).
% 88.53/11.69 fof(f25520,definition,(
% 88.53/11.69 ![X0]: (sQ490_spl <=> (d1(f(a3,f(a3,X0)))|~c(X0)|~c(f(X0,a3))))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ490_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f25523,plain,(
% 88.53/11.69 sQ490_spl|~sQ20_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f25508,f25520,f225])).
% 88.53/11.69 fof(f25524,definition,(
% 88.53/11.69 ![X0]: (sQ491_spl <=> (d1(f(a2,f(a2,X0)))|~c(X0)|~c(f(X0,a3))))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ491_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f25527,plain,(
% 88.53/11.69 sQ491_spl|~sQ27_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f25510,f25524,f301])).
% 88.53/11.69 fof(f25551,plain,(
% 88.53/11.69 ~c(f(a3,f(a1,a2)))|~sQ486_spl|~sQ32_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f25463,f374])).
% 88.53/11.69 fof(f25557,plain,(
% 88.53/11.69 $false|~sQ486_spl|~sQ32_spl),
% 88.53/11.69 inference(forward_subsumption_resolution,[status(thm)],[f25551,f18825])).
% 88.53/11.69 fof(f25558,plain,(
% 88.53/11.69 ~sQ486_spl|~sQ32_spl),
% 88.53/11.69 inference(contradiction_clause,[status(thm)],[f25557])).
% 88.53/11.69 fof(f25606,plain,(
% 88.53/11.69 ![X0]: (~c(f(a2,X0))|~c(X0)|~sQ489_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f25495,f18])).
% 88.53/11.69 fof(f25620,plain,(
% 88.53/11.69 ~c(f(a3,a3))|~sQ489_spl|~sQ86_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f25606,f2198])).
% 88.53/11.69 fof(f25630,plain,(
% 88.53/11.69 ~sQ20_spl|~sQ489_spl|~sQ86_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f25620,f225,f25494,f1789])).
% 88.53/11.69 fof(f25638,plain,(
% 88.53/11.69 ![X0]: (~d2(X0)|d1(f(a1,X0))|~sQ409_spl|~sQ351_spl)),
% 88.53/11.69 inference(forward_subsumption_resolution,[status(thm)],[f13606,f15838])).
% 88.53/11.69 fof(f27207,plain,(
% 88.53/11.69 ![X0]: (d1(X0)|d2(f(a1,X0))|d1(f(a1,X0))|~sQ409_spl|~sQ351_spl)),
% 88.53/11.69 inference(forward_subsumption_resolution,[status(thm)],[f20725,f25638])).
% 88.53/11.69 fof(f27211,plain,(
% 88.53/11.69 d1(f(a2,a3))|d1(f(a1,f(a2,a3)))|~sQ409_spl|~sQ351_spl|~sQ32_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f27207,f16414])).
% 88.53/11.69 fof(f27245,plain,(
% 88.53/11.69 sQ85_spl|sQ273_spl|~sQ409_spl|~sQ351_spl|~sQ32_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f27211,f1786,f9253,f15837,f13550,f373])).
% 88.53/11.69 fof(f27609,plain,(
% 88.53/11.69 ![X0]: (~c(f(X0,a1))|~c(f(a2,a2))|~d1(X0)|~sQ155_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f3712,f19474])).
% 88.53/11.69 fof(f27631,plain,(
% 88.53/11.69 sQ487_spl|~sQ27_spl|~sQ155_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f27609,f25481,f301,f3711])).
% 88.53/11.69 fof(f27845,definition,(
% 88.53/11.69 ![X0]: (sQ542_spl <=> (d2(X0)|~c(X0)))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ542_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f27846,plain,(
% 88.53/11.69 ![X0]: (d2(X0)|~c(X0)|~sQ542_spl)),
% 88.53/11.69 inference(component_clause,[status(thm)],[f27845])).
% 88.53/11.69 fof(f27860,plain,(
% 88.53/11.69 ![X0]: (~c(X0)|~sQ542_spl)),
% 88.53/11.69 inference(forward_subsumption_resolution,[status(thm)],[f27846,f15])).
% 88.53/11.69 fof(f27868,plain,(
% 88.53/11.69 $false|~sQ542_spl),
% 88.53/11.69 inference(backward_subsumption_resolution,[status(thm)],[f17,f27860])).
% 88.53/11.69 fof(f27892,plain,(
% 88.53/11.69 ~sQ542_spl),
% 88.53/11.69 inference(contradiction_clause,[status(thm)],[f27868])).
% 88.53/11.69 fof(f29632,plain,(
% 88.53/11.69 ![X0]: (~c(X0)|~d1(a2)|~d1(f(a2,X0)))),
% 88.53/11.69 inference(resolution,[status(thm)],[f1582,f23])).
% 88.53/11.69 fof(f29634,plain,(
% 88.53/11.69 sQ60_spl|~sQ0_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f29632,f820,f59])).
% 88.53/11.69 fof(f31698,plain,(
% 88.53/11.69 ![X0,X1]: (~d1(X0)|~d1(X1)|~d1(X0)|~d1(f(X1,a1)))),
% 88.53/11.69 inference(resolution,[status(thm)],[f124,f23])).
% 88.53/11.69 fof(f31708,definition,(
% 88.53/11.69 ![X1]: (sQ557_spl <=> (~d1(X1)|~d1(f(X1,a1))))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ557_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f31711,plain,(
% 88.53/11.69 sQ61_spl|sQ557_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f31698,f823,f31708])).
% 88.53/11.69 fof(f31720,plain,(
% 88.53/11.69 ![X0]: (~d2(f(a1,X0))|d1(f(X0,a3))|d1(f(a1,f(X0,a3)))|~sQ409_spl|~sQ351_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f13094,f27207])).
% 88.53/11.69 fof(f31725,plain,(
% 88.53/11.69 ![X0]: (~d2(f(a1,X0))|d1(f(X0,a3))|~sQ409_spl|~sQ351_spl)),
% 88.53/11.69 inference(forward_subsumption_resolution,[status(thm)],[f31720,f13084])).
% 88.53/11.69 fof(f32054,definition,(
% 88.53/11.69 ![X0,X1]: (sQ560_spl <=> (~d2(f(X0,X1))|~c(X0)|~d1(X1)))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ560_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f32055,plain,(
% 88.53/11.69 ![X0,X1]: (~d2(f(X0,X1))|~c(X0)|~d1(X1)|~sQ560_spl)),
% 88.53/11.69 inference(component_clause,[status(thm)],[f32054])).
% 88.53/11.69 fof(f32062,plain,(
% 88.53/11.69 ~c(a1)|~d1(a2)|~sQ560_spl|~sQ32_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f32055,f374])).
% 88.53/11.69 fof(f32073,plain,(
% 88.53/11.69 ~sQ19_spl|~sQ0_spl|~sQ560_spl|~sQ32_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f32062,f197,f59,f32054,f373])).
% 88.53/11.69 fof(f33528,plain,(
% 88.53/11.69 ~c(a1)|~c(f(a2,f(a1,a2)))|~sQ32_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f12369,f34])).
% 88.53/11.69 fof(f33567,definition,(
% 88.53/11.69 sQ564_spl <=> (c(f(a2,f(a1,a2))))),
% 88.53/11.69 introduced(definition,[new_symbols(definition,[sQ564_spl])],[split_symbol_definition])).
% 88.53/11.69 fof(f33570,plain,(
% 88.53/11.69 ~sQ19_spl|~sQ564_spl|~sQ32_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f33528,f197,f33567,f373])).
% 88.53/11.69 fof(f36314,plain,(
% 88.53/11.69 ~d1(a2)|~d1(f(a1,f(a3,a1)))|~sQ22_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f3968,f23])).
% 88.53/11.69 fof(f36316,plain,(
% 88.53/11.69 ~sQ0_spl|~sQ57_spl|~sQ22_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f36314,f59,f802,f256])).
% 88.53/11.69 fof(f36966,plain,(
% 88.53/11.69 ![X0]: (~c(f(X0,a1))|~c(a1)|~d2(X0)|~sQ30_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f24300,f317])).
% 88.53/11.69 fof(f36980,plain,(
% 88.53/11.69 sQ417_spl|~sQ19_spl|~sQ30_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f36966,f15971,f197,f316])).
% 88.53/11.69 fof(f37015,plain,(
% 88.53/11.69 ![X0]: (~c(f(X0,a1))|~sQ487_spl|~sQ417_spl)),
% 88.53/11.69 inference(forward_subsumption_resolution,[status(thm)],[f16130,f25482])).
% 88.53/11.69 fof(f37019,plain,(
% 88.53/11.69 ![X0,X1]: (~c(f(X0,f(X1,a1)))|~sQ487_spl|~sQ417_spl)),
% 88.53/11.69 inference(paramodulation,[status(thm)],[f12,f37015])).
% 88.53/11.69 fof(f37028,plain,(
% 88.53/11.69 ![X0]: (~c(f(X0,a2))|~c(f(a1,a2))|~d1(X0)|~sQ351_spl|~sQ32_spl)),
% 88.53/11.69 inference(resolution,[status(thm)],[f24301,f14713])).
% 88.53/11.69 fof(f37049,plain,(
% 88.53/11.69 sQ436_spl|~sQ337_spl|~sQ351_spl|~sQ32_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f37028,f17534,f11813,f13550,f373])).
% 88.53/11.69 fof(f37112,plain,(
% 88.53/11.69 ![X0]: (~d1(X0)|~sQ487_spl|~sQ417_spl|~sQ15_spl)),
% 88.53/11.69 inference(backward_subsumption_resolution,[status(thm)],[f2010,f37019])).
% 88.53/11.69 fof(f37125,plain,(
% 88.53/11.69 sQ339_spl|~sQ487_spl|~sQ417_spl|~sQ15_spl),
% 88.53/11.69 inference(split_clause,[status(thm)],[f37112,f12807,f25481,f15971,f182])).
% 88.53/11.69 fof(f37386,plain,(
% 88.53/11.69 d1(f(f(a2,a2),a3))|~sQ154_spl|~sQ409_spl|~sQ351_spl),
% 88.53/11.69 inference(resolution,[status(thm)],[f3709,f31725])).
% 88.53/11.69 fof(f37439,plain,(
% 88.53/11.69 d1(f(a2,f(a2,a3)))|~sQ154_spl|~sQ409_spl|~sQ351_spl),
% 88.53/11.69 inference(forward_demodulation,[status(thm)],[f12,f37386])).
% 88.53/11.69 fof(f37440,plain,(
% 88.53/11.69 $false|~sQ85_spl|~sQ154_spl|~sQ409_spl|~sQ351_spl),
% 88.53/11.69 inference(forward_subsumption_resolution,[status(thm)],[f37439,f13343])).
% 88.53/11.69 fof(f37441,plain,(
% 88.53/11.69 ~sQ85_spl|~sQ154_spl|~sQ409_spl|~sQ351_spl),
% 88.53/11.69 inference(contradiction_clause,[status(thm)],[f37440])).
% 88.53/11.69 fof(f37442,plain,(
% 88.53/11.69 $false),
% 88.53/11.69 inference(sat_refutation,[status(thm)],[f73,f77,f181,f192,f202,f263,f270,f283,f319,f348,f349,f446,f489,f490,f506,f574,f775,f833,f1448,f1971,f2002,f2177,f2228,f2748,f3714,f4088,f6532,f6654,f6998,f7121,f7406,f9468,f9507,f11247,f11582,f11652,f11798,f11838,f12828,f12841,f12852,f12904,f12905,f12952,f13229,f13231,f13553,f13584,f13597,f13607,f13895,f13910,f13976,f13995,f14075,f14158,f14329,f14341,f14345,f14375,f14379,f14394,f14430,f14437,f14438,f14611,f14615,f15334,f15638,f15845,f15846,f15912,f15928,f15932,f16264,f16512,f16517,f16521,f16534,f17023,f17591,f18061,f18064,f18179,f18215,f18242,f18514,f18555,f18559,f18640,f18987,f19021,f19046,f19050,f19189,f19248,f19819,f19975,f20212,f20239,f20638,f21296,f21487,f21543,f21643,f22244,f22401,f23805,f25497,f25523,f25527,f25558,f25630,f27245,f27631,f27892,f29634,f31711,f32073,f33570,f36316,f36980,f37049,f37125,f37441])).
% 88.53/11.71 % SZS output end CNFRefutation for theBenchmark.p
% 11.43/11.74 % Elapsed time: 11.369205 seconds
% 11.43/11.74 % CPU time: 89.296637 seconds
% 11.43/11.74 % Total memory used: 392.946 MB
% 11.43/11.74 % Net memory used: 288.587 MB
%------------------------------------------------------------------------------