%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV401+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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 02:50:43 PM UTC 2026
% Result : Theorem 7.32s 1.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV401+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n015.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 08:48:06 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.47 % Drodi V4.1.1
% 7.32/1.57 % Refutation found
% 7.32/1.57 % SZS status Theorem for theBenchmark: Theorem is valid
% 7.32/1.57 % SZS output start CNFRefutation for theBenchmark
% 7.32/1.57 fof(f1,axiom,(
% 7.32/1.57 (! [U,V,W] :( ( less_than(U,V)& less_than(V,W) )=> less_than(U,W) ) )),
% 7.32/1.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.32/1.57 fof(f2,axiom,(
% 7.32/1.57 (! [U,V] :( less_than(U,V)| less_than(V,U) ) )),
% 7.32/1.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.32/1.57 fof(f4,axiom,(
% 7.32/1.57 (! [U,V] :( strictly_less_than(U,V)<=> ( less_than(U,V)& ~ less_than(V,U) ) ) )),
% 7.32/1.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.32/1.57 fof(f11,axiom,(
% 7.32/1.57 (! [U,V,W,X,Y] :( pair_in_list(insert_slb(U,pair(V,X)),W,Y)<=> ( pair_in_list(U,W,Y)| ( V = W& X = Y ) ) ) )),
% 7.32/1.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.32/1.57 fof(f17,axiom,(
% 7.32/1.57 (! [U,V,W,X] :( strictly_less_than(X,W)=> update_slb(insert_slb(U,pair(V,X)),W) = insert_slb(update_slb(U,W),pair(V,W)) ) )),
% 7.32/1.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.32/1.57 fof(f18,axiom,(
% 7.32/1.57 (! [U,V,W,X] :( less_than(W,X)=> update_slb(insert_slb(U,pair(V,X)),W) = insert_slb(update_slb(U,W),pair(V,X)) ) )),
% 7.32/1.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.32/1.57 fof(f19,conjecture,(
% 7.32/1.57 (! [U] :( (! [V,W,X] :( ( pair_in_list(U,V,W)& less_than(X,W) )=> pair_in_list(update_slb(U,X),V,W) ))=> (! [Y,Z,X1,X2,X3] :( ( pair_in_list(insert_slb(U,pair(X2,X3)),Y,Z)& less_than(X1,Z) )=> pair_in_list(update_slb(insert_slb(U,pair(X2,X3)),X1),Y,Z) ) )) )),
% 7.32/1.57 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.32/1.57 fof(f20,negated_conjecture,(
% 7.32/1.57 ~((! [U] :( (! [V,W,X] :( ( pair_in_list(U,V,W)& less_than(X,W) )=> pair_in_list(update_slb(U,X),V,W) ))=> (! [Y,Z,X1,X2,X3] :( ( pair_in_list(insert_slb(U,pair(X2,X3)),Y,Z)& less_than(X1,Z) )=> pair_in_list(update_slb(insert_slb(U,pair(X2,X3)),X1),Y,Z) ) )) ))),
% 7.32/1.57 inference(negated_conjecture,[status(cth)],[f19])).
% 7.32/1.57 fof(f21,plain,(
% 7.32/1.57 ![U,V,W]: ((~less_than(U,V)|~less_than(V,W))|less_than(U,W))),
% 7.32/1.57 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 7.32/1.57 fof(f22,plain,(
% 7.32/1.57 ![U,W]: ((![V]: (~less_than(U,V)|~less_than(V,W)))|less_than(U,W))),
% 7.32/1.57 inference(miniscoping,[status(thm)],[f21])).
% 7.32/1.57 fof(f23,plain,(
% 7.32/1.57 ![X0,X1,X2]: (~less_than(X0,X1)|~less_than(X1,X2)|less_than(X0,X2))),
% 7.32/1.57 inference(cnf_transformation,[status(thm)],[f22])).
% 7.32/1.57 fof(f24,plain,(
% 7.32/1.57 ![X0,X1]: (less_than(X0,X1)|less_than(X1,X0))),
% 7.32/1.57 inference(cnf_transformation,[status(thm)],[f2])).
% 7.32/1.57 fof(f26,plain,(
% 7.32/1.57 ![U,V]: ((~strictly_less_than(U,V)|(less_than(U,V)&~less_than(V,U)))&(strictly_less_than(U,V)|(~less_than(U,V)|less_than(V,U))))),
% 7.32/1.57 inference(NNF_transformation,[status(thm)],[f4])).
% 7.32/1.57 fof(f27,plain,(
% 7.32/1.57 (![U,V]: (~strictly_less_than(U,V)|(less_than(U,V)&~less_than(V,U))))&(![U,V]: (strictly_less_than(U,V)|(~less_than(U,V)|less_than(V,U))))),
% 7.32/1.57 inference(miniscoping,[status(thm)],[f26])).
% 7.32/1.57 fof(f30,plain,(
% 7.32/1.57 ![X0,X1]: (strictly_less_than(X0,X1)|~less_than(X0,X1)|less_than(X1,X0))),
% 7.32/1.57 inference(cnf_transformation,[status(thm)],[f27])).
% 7.32/1.57 fof(f41,plain,(
% 7.32/1.57 ![U,V,W,X,Y]: ((~pair_in_list(insert_slb(U,pair(V,X)),W,Y)|(pair_in_list(U,W,Y)|(V=W&X=Y)))&(pair_in_list(insert_slb(U,pair(V,X)),W,Y)|(~pair_in_list(U,W,Y)&(~V=W|~X=Y))))),
% 7.32/1.57 inference(NNF_transformation,[status(thm)],[f11])).
% 7.32/1.57 fof(f42,plain,(
% 7.32/1.57 (![U,V,W,X,Y]: (~pair_in_list(insert_slb(U,pair(V,X)),W,Y)|(pair_in_list(U,W,Y)|(V=W&X=Y))))&(![U,V,W,X,Y]: (pair_in_list(insert_slb(U,pair(V,X)),W,Y)|(~pair_in_list(U,W,Y)&(~V=W|~X=Y))))),
% 7.32/1.57 inference(miniscoping,[status(thm)],[f41])).
% 7.32/1.57 fof(f43,plain,(
% 7.32/1.57 ![X0,X1,X2,X3,X4]: (~pair_in_list(insert_slb(X0,pair(X1,X2)),X3,X4)|pair_in_list(X0,X3,X4)|X1=X3)),
% 7.32/1.57 inference(cnf_transformation,[status(thm)],[f42])).
% 7.32/1.57 fof(f44,plain,(
% 7.32/1.57 ![X0,X1,X2,X3,X4]: (~pair_in_list(insert_slb(X0,pair(X1,X2)),X3,X4)|pair_in_list(X0,X3,X4)|X2=X4)),
% 7.32/1.57 inference(cnf_transformation,[status(thm)],[f42])).
% 7.32/1.57 fof(f45,plain,(
% 7.32/1.57 ![X0,X1,X2,X3,X4]: (pair_in_list(insert_slb(X0,pair(X1,X2)),X3,X4)|~pair_in_list(X0,X3,X4))),
% 7.32/1.57 inference(cnf_transformation,[status(thm)],[f42])).
% 7.32/1.57 fof(f46,plain,(
% 7.32/1.57 ![X0,X1,X2,X3,X4]: (pair_in_list(insert_slb(X0,pair(X1,X2)),X3,X4)|~X1=X3|~X2=X4)),
% 7.32/1.57 inference(cnf_transformation,[status(thm)],[f42])).
% 7.32/1.57 fof(f56,plain,(
% 7.32/1.57 ![U,V,W,X]: (~strictly_less_than(X,W)|update_slb(insert_slb(U,pair(V,X)),W)=insert_slb(update_slb(U,W),pair(V,W)))),
% 7.32/1.57 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 7.32/1.57 fof(f57,plain,(
% 7.32/1.57 ![W,X]: (~strictly_less_than(X,W)|(![U,V]: update_slb(insert_slb(U,pair(V,X)),W)=insert_slb(update_slb(U,W),pair(V,W))))),
% 7.32/1.57 inference(miniscoping,[status(thm)],[f56])).
% 7.32/1.57 fof(f58,plain,(
% 7.32/1.57 ![X0,X1,X2,X3]: (~strictly_less_than(X0,X1)|update_slb(insert_slb(X2,pair(X3,X0)),X1)=insert_slb(update_slb(X2,X1),pair(X3,X1)))),
% 7.32/1.57 inference(cnf_transformation,[status(thm)],[f57])).
% 7.32/1.57 fof(f59,plain,(
% 7.32/1.57 ![U,V,W,X]: (~less_than(W,X)|update_slb(insert_slb(U,pair(V,X)),W)=insert_slb(update_slb(U,W),pair(V,X)))),
% 7.32/1.57 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 7.32/1.57 fof(f60,plain,(
% 7.32/1.57 ![W,X]: (~less_than(W,X)|(![U,V]: update_slb(insert_slb(U,pair(V,X)),W)=insert_slb(update_slb(U,W),pair(V,X))))),
% 7.32/1.57 inference(miniscoping,[status(thm)],[f59])).
% 7.32/1.57 fof(f61,plain,(
% 7.32/1.57 ![X0,X1,X2,X3]: (~less_than(X0,X1)|update_slb(insert_slb(X2,pair(X3,X1)),X0)=insert_slb(update_slb(X2,X0),pair(X3,X1)))),
% 7.32/1.57 inference(cnf_transformation,[status(thm)],[f60])).
% 7.32/1.57 fof(f62,plain,(
% 7.32/1.57 (?[U]: ((![V,W,X]: ((~pair_in_list(U,V,W)|~less_than(X,W))|pair_in_list(update_slb(U,X),V,W)))&(?[Y,Z,X1,X2,X3]: ((pair_in_list(insert_slb(U,pair(X2,X3)),Y,Z)&less_than(X1,Z))&~pair_in_list(update_slb(insert_slb(U,pair(X2,X3)),X1),Y,Z)))))),
% 7.32/1.57 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 7.32/1.57 fof(f63,plain,(
% 7.32/1.57 ((![V,W,X]: ((~pair_in_list(sK0_skl,V,W)|~less_than(X,W))|pair_in_list(update_slb(sK0_skl,X),V,W)))&((pair_in_list(insert_slb(sK0_skl,pair(sK4_skl,sK5_skl)),sK1_skl,sK2_skl)&less_than(sK3_skl,sK2_skl))&~pair_in_list(update_slb(insert_slb(sK0_skl,pair(sK4_skl,sK5_skl)),sK3_skl),sK1_skl,sK2_skl)))),
% 7.32/1.57 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl]),skolemize(U,sK0_skl),skolemize(Y,sK1_skl),skolemize(Z,sK2_skl),skolemize(X1,sK3_skl),skolemize(X2,sK4_skl),skolemize(X3,sK5_skl)],[f62])).
% 7.32/1.57 fof(f64,plain,(
% 7.32/1.57 ![X0,X1,X2]: (~pair_in_list(sK0_skl,X0,X1)|~less_than(X2,X1)|pair_in_list(update_slb(sK0_skl,X2),X0,X1))),
% 7.32/1.57 inference(cnf_transformation,[status(thm)],[f63])).
% 7.32/1.57 fof(f65,plain,(
% 7.32/1.57 pair_in_list(insert_slb(sK0_skl,pair(sK4_skl,sK5_skl)),sK1_skl,sK2_skl)),
% 7.32/1.57 inference(cnf_transformation,[status(thm)],[f63])).
% 7.32/1.57 fof(f66,plain,(
% 7.32/1.57 less_than(sK3_skl,sK2_skl)),
% 7.32/1.57 inference(cnf_transformation,[status(thm)],[f63])).
% 7.32/1.57 fof(f67,plain,(
% 7.32/1.57 ~pair_in_list(update_slb(insert_slb(sK0_skl,pair(sK4_skl,sK5_skl)),sK3_skl),sK1_skl,sK2_skl)),
% 7.32/1.57 inference(cnf_transformation,[status(thm)],[f63])).
% 7.32/1.57 fof(f68,plain,(
% 7.32/1.57 ![X0,X1]: (strictly_less_than(X0,X1)|less_than(X1,X0))),
% 7.32/1.57 inference(forward_subsumption_resolution,[status(thm)],[f30,f24])).
% 7.32/1.57 fof(f70,plain,(
% 7.32/1.57 ![X0,X1,X2]: (pair_in_list(insert_slb(X0,pair(X1,X2)),X1,X2))),
% 7.32/1.57 inference(destructive_equality_resolution,[status(thm)],[f46])).
% 7.32/1.57 fof(f71,plain,(
% 7.32/1.57 ![X0]: (~pair_in_list(sK0_skl,X0,sK2_skl)|pair_in_list(update_slb(sK0_skl,sK3_skl),X0,sK2_skl))),
% 7.32/1.57 inference(resolution,[status(thm)],[f64,f66])).
% 7.32/1.57 fof(f76,plain,(
% 7.32/1.57 ![X0]: (~less_than(sK2_skl,X0)|less_than(sK3_skl,X0))),
% 7.32/1.57 inference(resolution,[status(thm)],[f23,f66])).
% 7.32/1.57 fof(f78,plain,(
% 7.32/1.57 ![X0,X1,X2]: (~less_than(X0,X1)|less_than(X2,X1)|less_than(X0,X2))),
% 7.32/1.57 inference(resolution,[status(thm)],[f23,f24])).
% 7.32/1.57 fof(f83,plain,(
% 7.32/1.57 ![X0]: (~less_than(X0,sK3_skl)|less_than(X0,sK2_skl))),
% 7.32/1.57 inference(resolution,[status(thm)],[f23,f66])).
% 7.32/1.57 fof(f97,plain,(
% 7.32/1.57 ![X0]: (less_than(sK3_skl,X0)|less_than(X0,sK2_skl))),
% 7.32/1.57 inference(resolution,[status(thm)],[f76,f24])).
% 7.32/1.57 fof(f113,plain,(
% 7.32/1.57 pair_in_list(sK0_skl,sK1_skl,sK2_skl)|sK4_skl=sK1_skl),
% 7.32/1.57 inference(resolution,[status(thm)],[f43,f65])).
% 7.32/1.57 fof(f114,definition,(
% 7.32/1.57 sQ0_spl <=> (pair_in_list(sK0_skl,sK1_skl,sK2_skl))),
% 7.32/1.57 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 7.32/1.57 fof(f115,plain,(
% 7.32/1.57 pair_in_list(sK0_skl,sK1_skl,sK2_skl)|~sQ0_spl),
% 7.32/1.57 inference(component_clause,[status(thm)],[f114])).
% 7.32/1.57 fof(f117,definition,(
% 7.32/1.57 sQ1_spl <=> (sK4_skl=sK1_skl)),
% 7.32/1.57 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 7.32/1.57 fof(f118,plain,(
% 7.32/1.57 sK4_skl=sK1_skl|~sQ1_spl),
% 7.32/1.57 inference(component_clause,[status(thm)],[f117])).
% 7.32/1.57 fof(f120,plain,(
% 7.32/1.57 sQ0_spl|sQ1_spl),
% 7.32/1.57 inference(split_clause,[status(thm)],[f113,f114,f117])).
% 7.32/1.57 fof(f121,plain,(
% 7.32/1.57 pair_in_list(sK0_skl,sK1_skl,sK2_skl)|sK5_skl=sK2_skl),
% 7.32/1.57 inference(resolution,[status(thm)],[f44,f65])).
% 7.32/1.57 fof(f122,definition,(
% 7.32/1.57 sQ2_spl <=> (sK5_skl=sK2_skl)),
% 7.32/1.57 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 7.32/1.57 fof(f123,plain,(
% 7.32/1.57 sK5_skl=sK2_skl|~sQ2_spl),
% 7.32/1.57 inference(component_clause,[status(thm)],[f122])).
% 7.32/1.57 fof(f125,plain,(
% 7.32/1.57 sQ0_spl|sQ2_spl),
% 7.32/1.57 inference(split_clause,[status(thm)],[f121,f114,f122])).
% 7.32/1.57 fof(f129,plain,(
% 7.32/1.57 less_than(sK3_skl,sK2_skl)|less_than(sK3_skl,sK2_skl)),
% 7.32/1.57 inference(resolution,[status(thm)],[f97,f83])).
% 7.32/1.57 fof(f134,plain,(
% 7.32/1.57 ![X0,X1]: (less_than(X0,sK2_skl)|~less_than(X0,X1)|less_than(sK3_skl,X1))),
% 7.32/1.57 inference(resolution,[status(thm)],[f97,f23])).
% 7.32/1.57 fof(f142,definition,(
% 7.32/1.57 sQ3_spl <=> (less_than(sK3_skl,sK2_skl))),
% 7.32/1.57 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 7.32/1.57 fof(f145,plain,(
% 7.32/1.57 sQ3_spl),
% 7.32/1.57 inference(split_clause,[status(thm)],[f129,f142])).
% 7.32/1.57 fof(f168,plain,(
% 7.32/1.57 ![X0,X1]: (less_than(X0,X1)|less_than(sK3_skl,X0)|less_than(X1,sK2_skl))),
% 7.32/1.57 inference(resolution,[status(thm)],[f78,f97])).
% 7.32/1.57 fof(f179,plain,(
% 7.32/1.57 ![X0,X1]: (update_slb(insert_slb(X0,pair(X1,sK2_skl)),sK3_skl)=insert_slb(update_slb(X0,sK3_skl),pair(X1,sK2_skl)))),
% 7.32/1.57 inference(resolution,[status(thm)],[f61,f66])).
% 7.32/1.57 fof(f244,plain,(
% 7.32/1.57 ![X0,X1,X2,X3]: (update_slb(insert_slb(X0,pair(X1,X2)),X3)=insert_slb(update_slb(X0,X3),pair(X1,X3))|less_than(X3,X2))),
% 7.32/1.57 inference(resolution,[status(thm)],[f58,f68])).
% 7.32/1.57 fof(f258,definition,(
% 7.32/1.57 ![X0]: (sQ10_spl <=> (less_than(X0,sK2_skl)|less_than(sK3_skl,X0)))),
% 7.32/1.57 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 7.32/1.57 fof(f262,plain,(
% 7.32/1.57 pair_in_list(update_slb(sK0_skl,sK3_skl),sK1_skl,sK2_skl)|~sQ0_spl),
% 7.32/1.57 inference(resolution,[status(thm)],[f71,f115])).
% 7.32/1.57 fof(f263,plain,(
% 7.32/1.57 ![X0,X1]: (pair_in_list(insert_slb(update_slb(sK0_skl,sK3_skl),pair(X0,X1)),sK1_skl,sK2_skl)|~sQ0_spl)),
% 7.32/1.57 inference(resolution,[status(thm)],[f262,f45])).
% 7.32/1.57 fof(f309,plain,(
% 7.32/1.57 ![X0,X1]: (less_than(sK3_skl,X0)|less_than(X1,sK2_skl)|less_than(X0,sK2_skl)|less_than(sK3_skl,X1))),
% 7.32/1.57 inference(resolution,[status(thm)],[f168,f134])).
% 7.32/1.57 fof(f361,plain,(
% 7.32/1.57 sQ10_spl),
% 7.32/1.57 inference(split_clause,[status(thm)],[f309,f258])).
% 7.32/1.57 fof(f450,plain,(
% 7.32/1.57 ~pair_in_list(update_slb(insert_slb(sK0_skl,pair(sK1_skl,sK5_skl)),sK3_skl),sK1_skl,sK2_skl)|~sQ1_spl),
% 7.32/1.57 inference(forward_demodulation,[status(thm)],[f118,f67])).
% 7.32/1.57 fof(f451,plain,(
% 7.32/1.57 ~pair_in_list(update_slb(insert_slb(sK0_skl,pair(sK1_skl,sK2_skl)),sK3_skl),sK1_skl,sK2_skl)|~sQ2_spl|~sQ1_spl),
% 7.32/1.57 inference(forward_demodulation,[status(thm)],[f123,f450])).
% 7.32/1.57 fof(f452,plain,(
% 7.32/1.57 ~pair_in_list(insert_slb(update_slb(sK0_skl,sK3_skl),pair(sK1_skl,sK2_skl)),sK1_skl,sK2_skl)|~sQ2_spl|~sQ1_spl),
% 7.32/1.57 inference(backward_demodulation,[status(thm)],[f179,f451])).
% 7.32/1.57 fof(f455,plain,(
% 7.32/1.57 $false|~sQ2_spl|~sQ1_spl),
% 7.32/1.57 inference(forward_subsumption_resolution,[status(thm)],[f452,f70])).
% 7.32/1.57 fof(f456,plain,(
% 7.32/1.57 ~sQ2_spl|~sQ1_spl),
% 7.32/1.57 inference(contradiction_clause,[status(thm)],[f455])).
% 7.32/1.57 fof(f591,plain,(
% 7.32/1.57 ![X0,X1,X2,X3,X4,X5]: (update_slb(insert_slb(X0,pair(X1,X2)),X3)=insert_slb(update_slb(X0,X3),pair(X1,X3))|update_slb(insert_slb(X4,pair(X5,X2)),X3)=insert_slb(update_slb(X4,X3),pair(X5,X2)))),
% 7.32/1.57 inference(resolution,[status(thm)],[f244,f61])).
% 7.32/1.57 fof(f1069,definition,(
% 7.32/1.57 sQ45_spl <=> (pair_in_list(insert_slb(update_slb(sK0_skl,sK3_skl),pair(sK4_skl,sK5_skl)),sK1_skl,sK2_skl))),
% 7.32/1.57 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 7.32/1.57 fof(f1071,plain,(
% 7.32/1.57 ~pair_in_list(insert_slb(update_slb(sK0_skl,sK3_skl),pair(sK4_skl,sK5_skl)),sK1_skl,sK2_skl)|sQ45_spl),
% 7.32/1.57 inference(component_clause,[status(thm)],[f1069])).
% 7.32/1.57 fof(f1077,plain,(
% 7.32/1.57 $false|~sQ0_spl|sQ45_spl),
% 7.32/1.57 inference(forward_subsumption_resolution,[status(thm)],[f1071,f263])).
% 7.32/1.57 fof(f1078,plain,(
% 7.32/1.57 ~sQ0_spl|sQ45_spl),
% 7.32/1.58 inference(contradiction_clause,[status(thm)],[f1077])).
% 7.32/1.58 fof(f1599,plain,(
% 7.32/1.58 ![X0,X1]: (~pair_in_list(insert_slb(update_slb(sK0_skl,sK3_skl),pair(sK4_skl,sK3_skl)),sK1_skl,sK2_skl)|update_slb(insert_slb(X0,pair(X1,sK5_skl)),sK3_skl)=insert_slb(update_slb(X0,sK3_skl),pair(X1,sK5_skl)))),
% 7.32/1.58 inference(paramodulation,[status(thm)],[f591,f67])).
% 7.32/1.58 fof(f1628,definition,(
% 7.32/1.58 sQ62_spl <=> (pair_in_list(insert_slb(update_slb(sK0_skl,sK3_skl),pair(sK4_skl,sK3_skl)),sK1_skl,sK2_skl))),
% 7.32/1.58 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 7.32/1.58 fof(f1630,plain,(
% 7.32/1.58 ~pair_in_list(insert_slb(update_slb(sK0_skl,sK3_skl),pair(sK4_skl,sK3_skl)),sK1_skl,sK2_skl)|sQ62_spl),
% 7.32/1.58 inference(component_clause,[status(thm)],[f1628])).
% 7.32/1.58 fof(f1631,definition,(
% 7.32/1.58 ![X0,X1]: (sQ63_spl <=> (update_slb(insert_slb(X0,pair(X1,sK5_skl)),sK3_skl)=insert_slb(update_slb(X0,sK3_skl),pair(X1,sK5_skl))))),
% 7.32/1.58 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 7.32/1.58 fof(f1632,plain,(
% 7.32/1.59 ![X0,X1]: (update_slb(insert_slb(X0,pair(X1,sK5_skl)),sK3_skl)=insert_slb(update_slb(X0,sK3_skl),pair(X1,sK5_skl))|~sQ63_spl)),
% 7.32/1.59 inference(component_clause,[status(thm)],[f1631])).
% 7.32/1.59 fof(f1634,plain,(
% 7.32/1.59 ~sQ62_spl|sQ63_spl),
% 7.32/1.59 inference(split_clause,[status(thm)],[f1599,f1628,f1631])).
% 7.32/1.59 fof(f1636,plain,(
% 7.32/1.59 $false|~sQ0_spl|sQ62_spl),
% 7.32/1.59 inference(forward_subsumption_resolution,[status(thm)],[f1630,f263])).
% 7.32/1.59 fof(f1637,plain,(
% 7.32/1.59 ~sQ0_spl|sQ62_spl),
% 7.32/1.59 inference(contradiction_clause,[status(thm)],[f1636])).
% 7.32/1.59 fof(f1638,plain,(
% 7.32/1.59 ~pair_in_list(insert_slb(update_slb(sK0_skl,sK3_skl),pair(sK4_skl,sK5_skl)),sK1_skl,sK2_skl)|~sQ63_spl),
% 7.32/1.59 inference(backward_demodulation,[status(thm)],[f1632,f67])).
% 7.32/1.59 fof(f1639,plain,(
% 7.32/1.59 ~sQ45_spl|~sQ63_spl),
% 7.32/1.59 inference(split_clause,[status(thm)],[f1638,f1069,f1631])).
% 7.32/1.59 fof(f1640,plain,(
% 7.32/1.59 $false),
% 7.32/1.59 inference(sat_refutation,[status(thm)],[f120,f125,f145,f361,f456,f1078,f1634,f1637,f1639])).
% 7.32/1.59 % SZS output end CNFRefutation for theBenchmark.p
% 7.32/1.60 % Elapsed time: 1.122314 seconds
% 7.32/1.60 % CPU time: 8.339035 seconds
% 7.32/1.60 % Total memory used: 139.386 MB
% 7.32/1.60 % Net memory used: 133.370 MB
%------------------------------------------------------------------------------