%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV391+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 : n002.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:42 PM UTC 2026
% Result : Theorem 8.63s 1.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV391+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n002.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 08:47:17 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.14/0.38 % Drodi V4.1.1
% 8.63/1.52 % Refutation found
% 8.63/1.52 % SZS status Theorem for theBenchmark: Theorem is valid
% 8.63/1.52 % SZS output start CNFRefutation for theBenchmark
% 8.63/1.52 fof(f2,axiom,(
% 8.63/1.52 (! [U,V] :( less_than(U,V)| less_than(V,U) ) )),
% 8.63/1.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.63/1.52 fof(f4,axiom,(
% 8.63/1.52 (! [U,V] :( strictly_less_than(U,V)<=> ( less_than(U,V)& ~ less_than(V,U) ) ) )),
% 8.63/1.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.63/1.52 fof(f5,axiom,(
% 8.63/1.52 (! [U] : less_than(bottom,U) )),
% 8.63/1.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.63/1.52 fof(f9,axiom,(
% 8.63/1.52 (! [U,V,W,X] :( contains_slb(insert_slb(U,pair(V,X)),W)<=> ( contains_slb(U,W)| V = W ) ) )),
% 8.63/1.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.63/1.52 fof(f25,axiom,(
% 8.63/1.52 (! [U,V,W,X,Y] :( less_than(Y,X)=> ( check_cpq(triple(U,insert_slb(V,pair(X,Y)),W))<=> check_cpq(triple(U,V,W)) ) ) )),
% 8.63/1.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.63/1.52 fof(f28,axiom,(
% 8.63/1.52 (! [U,V] :( ok(triple(U,V,bad))<=> $false ) )),
% 8.63/1.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.63/1.52 fof(f32,axiom,(
% 8.63/1.52 (! [U,V,W,X] :( ( contains_slb(V,X)& less_than(lookup_slb(V,X),X) )=> remove_cpq(triple(U,V,W),X) = triple(remove_pqp(U,X),remove_slb(V,X),W) ) )),
% 8.63/1.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.63/1.52 fof(f33,axiom,(
% 8.63/1.52 (! [U,V,W,X] :( ( contains_slb(V,X)& strictly_less_than(X,lookup_slb(V,X)) )=> remove_cpq(triple(U,V,W),X) = triple(remove_pqp(U,X),remove_slb(V,X),bad) ) )),
% 8.63/1.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.63/1.52 fof(f42,lemma,(
% 8.63/1.52 (! [U,V,W] :( check_cpq(triple(U,V,W))<=> (! [X,Y] :( pair_in_list(V,X,Y)=> less_than(Y,X) ) )) )),
% 8.63/1.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.63/1.52 fof(f43,lemma,(
% 8.63/1.52 (! [U,V,W] :( pair_in_list(U,V,W)=> (! [X] :( contains_slb(U,X)=> ( pair_in_list(remove_slb(U,X),V,W)| V = X ) ) )) )),
% 8.63/1.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.63/1.52 fof(f44,lemma,(
% 8.63/1.52 (! [U,V,W,X] :( ( check_cpq(remove_cpq(triple(U,V,W),X))& ok(remove_cpq(triple(U,V,W),X)) )=> (! [Y] :( pair_in_list(V,X,Y)=> less_than(Y,X) ) )) )),
% 8.63/1.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.63/1.52 fof(f45,lemma,(
% 8.63/1.52 (! [U,V,W,X] :( ok(remove_cpq(triple(U,V,W),X))=> contains_slb(V,X) ) )),
% 8.63/1.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.63/1.52 fof(f46,conjecture,(
% 8.63/1.52 (! [U,V,W,X] :( ( check_cpq(remove_cpq(triple(U,V,W),X))& ok(remove_cpq(triple(U,V,W),X)) )=> check_cpq(triple(U,V,W)) ) )),
% 8.63/1.52 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 8.63/1.52 fof(f47,negated_conjecture,(
% 8.63/1.52 ~((! [U,V,W,X] :( ( check_cpq(remove_cpq(triple(U,V,W),X))& ok(remove_cpq(triple(U,V,W),X)) )=> check_cpq(triple(U,V,W)) ) ))),
% 8.63/1.52 inference(negated_conjecture,[status(cth)],[f46])).
% 8.63/1.52 fof(f51,plain,(
% 8.63/1.52 ![X0,X1]: (less_than(X0,X1)|less_than(X1,X0))),
% 8.63/1.52 inference(cnf_transformation,[status(thm)],[f2])).
% 8.63/1.52 fof(f53,plain,(
% 8.63/1.52 ![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))))),
% 8.63/1.52 inference(NNF_transformation,[status(thm)],[f4])).
% 8.63/1.52 fof(f54,plain,(
% 8.63/1.52 (![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))))),
% 8.63/1.52 inference(miniscoping,[status(thm)],[f53])).
% 8.63/1.52 fof(f57,plain,(
% 8.63/1.52 ![X0,X1]: (strictly_less_than(X0,X1)|~less_than(X0,X1)|less_than(X1,X0))),
% 8.63/1.52 inference(cnf_transformation,[status(thm)],[f54])).
% 8.63/1.52 fof(f58,plain,(
% 8.63/1.52 ![X0]: (less_than(bottom,X0))),
% 8.63/1.52 inference(cnf_transformation,[status(thm)],[f5])).
% 8.63/1.52 fof(f62,plain,(
% 8.63/1.52 ![U,V,W,X]: ((~contains_slb(insert_slb(U,pair(V,X)),W)|(contains_slb(U,W)|V=W))&(contains_slb(insert_slb(U,pair(V,X)),W)|(~contains_slb(U,W)&~V=W)))),
% 8.63/1.52 inference(NNF_transformation,[status(thm)],[f9])).
% 8.63/1.52 fof(f63,plain,(
% 8.63/1.52 (![U,V,W]: ((![X]: ~contains_slb(insert_slb(U,pair(V,X)),W))|(contains_slb(U,W)|V=W)))&(![U,V,W]: ((![X]: contains_slb(insert_slb(U,pair(V,X)),W))|(~contains_slb(U,W)&~V=W)))),
% 8.63/1.52 inference(miniscoping,[status(thm)],[f62])).
% 8.63/1.52 fof(f64,plain,(
% 8.63/1.52 ![X0,X1,X2,X3]: (~contains_slb(insert_slb(X0,pair(X1,X2)),X3)|contains_slb(X0,X3)|X1=X3)),
% 8.63/1.52 inference(cnf_transformation,[status(thm)],[f63])).
% 8.63/1.52 fof(f65,plain,(
% 8.63/1.52 ![X0,X1,X2,X3]: (contains_slb(insert_slb(X0,pair(X1,X2)),X3)|~contains_slb(X0,X3))),
% 8.63/1.52 inference(cnf_transformation,[status(thm)],[f63])).
% 8.63/1.52 fof(f101,plain,(
% 8.63/1.52 ![U,V,W,X,Y]: (~less_than(Y,X)|(check_cpq(triple(U,insert_slb(V,pair(X,Y)),W))<=>check_cpq(triple(U,V,W))))),
% 8.63/1.52 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 8.63/1.52 fof(f102,plain,(
% 8.63/1.52 ![U,V,W,X,Y]: (~less_than(Y,X)|((~check_cpq(triple(U,insert_slb(V,pair(X,Y)),W))|check_cpq(triple(U,V,W)))&(check_cpq(triple(U,insert_slb(V,pair(X,Y)),W))|~check_cpq(triple(U,V,W)))))),
% 8.63/1.52 inference(NNF_transformation,[status(thm)],[f101])).
% 8.63/1.52 fof(f103,plain,(
% 8.63/1.52 ![X,Y]: (~less_than(Y,X)|((![U,V,W]: (~check_cpq(triple(U,insert_slb(V,pair(X,Y)),W))|check_cpq(triple(U,V,W))))&(![U,V,W]: (check_cpq(triple(U,insert_slb(V,pair(X,Y)),W))|~check_cpq(triple(U,V,W))))))),
% 8.63/1.52 inference(miniscoping,[status(thm)],[f102])).
% 8.63/1.52 fof(f104,plain,(
% 8.63/1.52 ![X0,X1,X2,X3,X4]: (~less_than(X0,X1)|~check_cpq(triple(X2,insert_slb(X3,pair(X1,X0)),X4))|check_cpq(triple(X2,X3,X4)))),
% 8.63/1.52 inference(cnf_transformation,[status(thm)],[f103])).
% 8.63/1.52 fof(f105,plain,(
% 8.63/1.52 ![X0,X1,X2,X3,X4]: (~less_than(X0,X1)|check_cpq(triple(X2,insert_slb(X3,pair(X1,X0)),X4))|~check_cpq(triple(X2,X3,X4)))),
% 8.63/1.52 inference(cnf_transformation,[status(thm)],[f103])).
% 8.63/1.52 fof(f115,plain,(
% 8.63/1.52 ![U,V]: ((~ok(triple(U,V,bad))|$false)&(ok(triple(U,V,bad))|$true))),
% 8.63/1.52 inference(NNF_transformation,[status(thm)],[f28])).
% 8.63/1.52 fof(f116,plain,(
% 8.63/1.52 ((![U,V]: ~ok(triple(U,V,bad)))|$false)&((![U,V]: ok(triple(U,V,bad)))|$true)),
% 8.63/1.52 inference(miniscoping,[status(thm)],[f115])).
% 8.63/1.52 fof(f117,plain,(
% 8.63/1.52 ![U,V]: ~ok(triple(U,V,bad))),
% 8.63/1.52 inference(true_and_false_simplification,[status(thm)],[f116])).
% 8.63/1.52 fof(f118,plain,(
% 8.63/1.52 ![X0,X1]: (~ok(triple(X0,X1,bad)))),
% 8.63/1.52 inference(cnf_transformation,[status(thm)],[f117])).
% 8.63/1.52 fof(f126,plain,(
% 8.63/1.52 ![U,V,W,X]: ((~contains_slb(V,X)|~less_than(lookup_slb(V,X),X))|remove_cpq(triple(U,V,W),X)=triple(remove_pqp(U,X),remove_slb(V,X),W))),
% 8.63/1.52 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 8.63/1.52 fof(f127,plain,(
% 8.63/1.52 ![V,X]: ((~contains_slb(V,X)|~less_than(lookup_slb(V,X),X))|(![U,W]: remove_cpq(triple(U,V,W),X)=triple(remove_pqp(U,X),remove_slb(V,X),W)))),
% 8.63/1.52 inference(miniscoping,[status(thm)],[f126])).
% 8.63/1.52 fof(f128,plain,(
% 8.63/1.52 ![X0,X1,X2,X3]: (~contains_slb(X0,X1)|~less_than(lookup_slb(X0,X1),X1)|remove_cpq(triple(X2,X0,X3),X1)=triple(remove_pqp(X2,X1),remove_slb(X0,X1),X3))),
% 8.63/1.52 inference(cnf_transformation,[status(thm)],[f127])).
% 8.63/1.52 fof(f129,plain,(
% 8.63/1.52 ![U,V,W,X]: ((~contains_slb(V,X)|~strictly_less_than(X,lookup_slb(V,X)))|remove_cpq(triple(U,V,W),X)=triple(remove_pqp(U,X),remove_slb(V,X),bad))),
% 8.63/1.52 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 8.63/1.52 fof(f130,plain,(
% 8.63/1.52 ![V,X]: ((~contains_slb(V,X)|~strictly_less_than(X,lookup_slb(V,X)))|(![U,W]: remove_cpq(triple(U,V,W),X)=triple(remove_pqp(U,X),remove_slb(V,X),bad)))),
% 8.63/1.52 inference(miniscoping,[status(thm)],[f129])).
% 8.63/1.52 fof(f131,plain,(
% 8.63/1.52 ![X0,X1,X2,X3]: (~contains_slb(X0,X1)|~strictly_less_than(X1,lookup_slb(X0,X1))|remove_cpq(triple(X2,X0,X3),X1)=triple(remove_pqp(X2,X1),remove_slb(X0,X1),bad))),
% 8.63/1.52 inference(cnf_transformation,[status(thm)],[f130])).
% 8.63/1.52 fof(f148,plain,(
% 8.63/1.52 ![U,V,W]: (check_cpq(triple(U,V,W))<=>(![X,Y]: (~pair_in_list(V,X,Y)|less_than(Y,X))))),
% 8.63/1.52 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 8.63/1.52 fof(f149,plain,(
% 8.63/1.52 ![U,V,W]: ((~check_cpq(triple(U,V,W))|(![X,Y]: (~pair_in_list(V,X,Y)|less_than(Y,X))))&(check_cpq(triple(U,V,W))|(?[X,Y]: (pair_in_list(V,X,Y)&~less_than(Y,X)))))),
% 8.63/1.52 inference(NNF_transformation,[status(thm)],[f148])).
% 8.63/1.52 fof(f150,plain,(
% 8.63/1.52 (![V]: ((![U,W]: ~check_cpq(triple(U,V,W)))|(![X,Y]: (~pair_in_list(V,X,Y)|less_than(Y,X)))))&(![V]: ((![U,W]: check_cpq(triple(U,V,W)))|(?[X,Y]: (pair_in_list(V,X,Y)&~less_than(Y,X)))))),
% 8.63/1.52 inference(miniscoping,[status(thm)],[f149])).
% 8.63/1.52 fof(f151,plain,(
% 8.63/1.52 (![V]: ((![U,W]: ~check_cpq(triple(U,V,W)))|(![X,Y]: (~pair_in_list(V,X,Y)|less_than(Y,X)))))&(![V]: ((![U,W]: check_cpq(triple(U,V,W)))|(pair_in_list(V,sK0_skl(V),sK1_skl(V))&~less_than(sK1_skl(V),sK0_skl(V)))))),
% 8.63/1.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(X,sK0_skl(V)),skolemize(Y,sK1_skl(V))],[f150])).
% 8.63/1.52 fof(f152,plain,(
% 8.63/1.52 ![X0,X1,X2,X3,X4]: (~check_cpq(triple(X0,X1,X2))|~pair_in_list(X1,X3,X4)|less_than(X4,X3))),
% 8.63/1.52 inference(cnf_transformation,[status(thm)],[f151])).
% 8.63/1.52 fof(f153,plain,(
% 8.63/1.52 ![X0,X1,X2]: (check_cpq(triple(X0,X1,X2))|pair_in_list(X1,sK0_skl(X1),sK1_skl(X1)))),
% 8.63/1.52 inference(cnf_transformation,[status(thm)],[f151])).
% 8.63/1.52 fof(f154,plain,(
% 8.63/1.52 ![X0,X1,X2]: (check_cpq(triple(X0,X1,X2))|~less_than(sK1_skl(X1),sK0_skl(X1)))),
% 8.63/1.52 inference(cnf_transformation,[status(thm)],[f151])).
% 8.63/1.52 fof(f155,plain,(
% 8.63/1.52 ![U,V,W]: (~pair_in_list(U,V,W)|(![X]: (~contains_slb(U,X)|(pair_in_list(remove_slb(U,X),V,W)|V=X))))),
% 8.63/1.52 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 8.63/1.52 fof(f156,plain,(
% 8.63/1.52 ![X0,X1,X2,X3]: (~pair_in_list(X0,X1,X2)|~contains_slb(X0,X3)|pair_in_list(remove_slb(X0,X3),X1,X2)|X1=X3)),
% 8.63/1.52 inference(cnf_transformation,[status(thm)],[f155])).
% 8.63/1.52 fof(f157,plain,(
% 8.63/1.52 ![U,V,W,X]: ((~check_cpq(remove_cpq(triple(U,V,W),X))|~ok(remove_cpq(triple(U,V,W),X)))|(![Y]: (~pair_in_list(V,X,Y)|less_than(Y,X))))),
% 8.63/1.52 inference(pre_NNF_transformation,[status(thm)],[f44])).
% 8.63/1.52 fof(f158,plain,(
% 8.63/1.52 ![V,X]: ((![U,W]: (~check_cpq(remove_cpq(triple(U,V,W),X))|~ok(remove_cpq(triple(U,V,W),X))))|(![Y]: (~pair_in_list(V,X,Y)|less_than(Y,X))))),
% 8.63/1.52 inference(miniscoping,[status(thm)],[f157])).
% 8.63/1.52 fof(f159,plain,(
% 8.63/1.52 ![X0,X1,X2,X3,X4]: (~check_cpq(remove_cpq(triple(X0,X1,X2),X3))|~ok(remove_cpq(triple(X0,X1,X2),X3))|~pair_in_list(X1,X3,X4)|less_than(X4,X3))),
% 8.63/1.52 inference(cnf_transformation,[status(thm)],[f158])).
% 8.63/1.52 fof(f160,plain,(
% 8.63/1.52 ![U,V,W,X]: (~ok(remove_cpq(triple(U,V,W),X))|contains_slb(V,X))),
% 8.63/1.52 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 8.63/1.52 fof(f161,plain,(
% 8.63/1.52 ![V,X]: ((![U,W]: ~ok(remove_cpq(triple(U,V,W),X)))|contains_slb(V,X))),
% 8.63/1.52 inference(miniscoping,[status(thm)],[f160])).
% 8.63/1.52 fof(f162,plain,(
% 8.63/1.52 ![X0,X1,X2,X3]: (~ok(remove_cpq(triple(X0,X1,X2),X3))|contains_slb(X1,X3))),
% 8.63/1.52 inference(cnf_transformation,[status(thm)],[f161])).
% 8.63/1.52 fof(f163,plain,(
% 8.63/1.52 (?[U,V,W,X]: ((check_cpq(remove_cpq(triple(U,V,W),X))&ok(remove_cpq(triple(U,V,W),X)))&~check_cpq(triple(U,V,W))))),
% 8.63/1.52 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 8.63/1.52 fof(f164,plain,(
% 8.63/1.52 ?[U,V,W]: ((?[X]: (check_cpq(remove_cpq(triple(U,V,W),X))&ok(remove_cpq(triple(U,V,W),X))))&~check_cpq(triple(U,V,W)))),
% 8.63/1.52 inference(miniscoping,[status(thm)],[f163])).
% 8.63/1.52 fof(f165,plain,(
% 8.63/1.52 ((check_cpq(remove_cpq(triple(sK2_skl,sK3_skl,sK4_skl),sK5_skl))&ok(remove_cpq(triple(sK2_skl,sK3_skl,sK4_skl),sK5_skl)))&~check_cpq(triple(sK2_skl,sK3_skl,sK4_skl)))),
% 8.63/1.52 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl,sK4_skl,sK5_skl]),skolemize(U,sK2_skl),skolemize(V,sK3_skl),skolemize(W,sK4_skl),skolemize(X,sK5_skl)],[f164])).
% 8.63/1.52 fof(f166,plain,(
% 8.63/1.52 check_cpq(remove_cpq(triple(sK2_skl,sK3_skl,sK4_skl),sK5_skl))),
% 8.63/1.52 inference(cnf_transformation,[status(thm)],[f165])).
% 8.63/1.52 fof(f167,plain,(
% 8.63/1.52 ok(remove_cpq(triple(sK2_skl,sK3_skl,sK4_skl),sK5_skl))),
% 8.63/1.52 inference(cnf_transformation,[status(thm)],[f165])).
% 8.63/1.52 fof(f168,plain,(
% 8.63/1.52 ~check_cpq(triple(sK2_skl,sK3_skl,sK4_skl))),
% 8.63/1.52 inference(cnf_transformation,[status(thm)],[f165])).
% 8.63/1.52 fof(f169,plain,(
% 8.63/1.52 ![X0,X1]: (strictly_less_than(X0,X1)|less_than(X1,X0))),
% 8.63/1.52 inference(forward_subsumption_resolution,[status(thm)],[f57,f51])).
% 8.63/1.52 fof(f192,plain,(
% 8.63/1.52 contains_slb(sK3_skl,sK5_skl)),
% 8.63/1.52 inference(resolution,[status(thm)],[f162,f167])).
% 8.63/1.52 fof(f194,plain,(
% 8.63/1.52 ![X0]: (~check_cpq(remove_cpq(triple(sK2_skl,sK3_skl,sK4_skl),sK5_skl))|~pair_in_list(sK3_skl,sK5_skl,X0)|less_than(X0,sK5_skl))),
% 8.63/1.52 inference(resolution,[status(thm)],[f159,f167])).
% 8.63/1.52 fof(f195,definition,(
% 8.63/1.52 sQ0_spl <=> (check_cpq(remove_cpq(triple(sK2_skl,sK3_skl,sK4_skl),sK5_skl)))),
% 8.63/1.52 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 8.63/1.52 fof(f197,plain,(
% 8.63/1.52 ~check_cpq(remove_cpq(triple(sK2_skl,sK3_skl,sK4_skl),sK5_skl))|sQ0_spl),
% 8.63/1.52 inference(component_clause,[status(thm)],[f195])).
% 8.63/1.52 fof(f198,definition,(
% 8.63/1.52 ![X0]: (sQ1_spl <=> (~pair_in_list(sK3_skl,sK5_skl,X0)|less_than(X0,sK5_skl)))),
% 8.63/1.52 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 8.63/1.52 fof(f199,plain,(
% 8.63/1.52 ![X0]: (~pair_in_list(sK3_skl,sK5_skl,X0)|less_than(X0,sK5_skl)|~sQ1_spl)),
% 8.63/1.52 inference(component_clause,[status(thm)],[f198])).
% 8.63/1.52 fof(f201,plain,(
% 8.63/1.52 ~sQ0_spl|sQ1_spl),
% 8.63/1.52 inference(split_clause,[status(thm)],[f194,f195,f198])).
% 8.63/1.52 fof(f202,plain,(
% 8.63/1.52 $false|sQ0_spl),
% 8.63/1.52 inference(forward_subsumption_resolution,[status(thm)],[f197,f166])).
% 8.63/1.52 fof(f203,plain,(
% 8.63/1.52 sQ0_spl),
% 8.63/1.52 inference(contradiction_clause,[status(thm)],[f202])).
% 8.63/1.52 fof(f208,plain,(
% 8.63/1.52 ![X0,X1,X2,X3]: (check_cpq(triple(X0,insert_slb(X1,pair(X2,bottom)),X3))|~check_cpq(triple(X0,X1,X3)))),
% 8.63/1.52 inference(resolution,[status(thm)],[f58,f105])).
% 8.63/1.52 fof(f232,definition,(
% 8.63/1.52 ![X0]: (sQ4_spl <=> (~less_than(bottom,X0)))),
% 8.63/1.52 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 8.63/1.52 fof(f233,plain,(
% 8.63/1.52 ![X0]: (~less_than(bottom,X0)|~sQ4_spl)),
% 8.63/1.52 inference(component_clause,[status(thm)],[f232])).
% 8.63/1.52 fof(f248,plain,(
% 8.63/1.52 ![X0,X1]: (contains_slb(insert_slb(sK3_skl,pair(X0,X1)),sK5_skl))),
% 8.63/1.52 inference(resolution,[status(thm)],[f65,f192])).
% 8.63/1.52 fof(f251,plain,(
% 8.63/1.52 ![X0]: (contains_slb(sK3_skl,sK5_skl)|X0=sK5_skl)),
% 8.63/1.52 inference(resolution,[status(thm)],[f248,f64])).
% 8.63/1.52 fof(f253,definition,(
% 8.63/1.52 sQ5_spl <=> (contains_slb(sK3_skl,sK5_skl))),
% 8.63/1.52 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 8.63/1.52 fof(f256,definition,(
% 8.63/1.52 ![X0]: (sQ6_spl <=> (X0=sK5_skl))),
% 8.63/1.52 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 8.63/1.52 fof(f257,plain,(
% 8.63/1.52 ![X0]: (X0=sK5_skl|~sQ6_spl)),
% 8.63/1.52 inference(component_clause,[status(thm)],[f256])).
% 8.63/1.52 fof(f259,plain,(
% 8.63/1.52 sQ5_spl|sQ6_spl),
% 8.63/1.52 inference(split_clause,[status(thm)],[f251,f253,f256])).
% 8.63/1.52 fof(f266,plain,(
% 8.63/1.52 ![X0,X1]: (X0=X1|~sQ6_spl)),
% 8.63/1.52 inference(paramodulation,[status(thm)],[f257,f257])).
% 8.63/1.52 fof(f276,plain,(
% 8.63/1.52 ![X0,X1,X2,X3,X4]: (check_cpq(triple(X0,insert_slb(X1,pair(X2,bottom)),X3))|~check_cpq(X4)|~sQ6_spl)),
% 8.63/1.52 inference(paramodulation,[status(thm)],[f266,f208])).
% 8.63/1.52 fof(f278,definition,(
% 8.63/1.52 ![X0,X1,X2,X3]: (sQ8_spl <=> (check_cpq(triple(X0,insert_slb(X1,pair(X2,bottom)),X3))))),
% 8.63/1.52 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 8.63/1.52 fof(f279,plain,(
% 8.63/1.52 ![X0,X1,X2,X3]: (check_cpq(triple(X0,insert_slb(X1,pair(X2,bottom)),X3))|~sQ8_spl)),
% 8.63/1.52 inference(component_clause,[status(thm)],[f278])).
% 8.63/1.52 fof(f281,definition,(
% 8.63/1.52 ![X4]: (sQ9_spl <=> (~check_cpq(X4)))),
% 8.63/1.52 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 8.63/1.52 fof(f282,plain,(
% 8.63/1.52 ![X0]: (~check_cpq(X0)|~sQ9_spl)),
% 8.63/1.52 inference(component_clause,[status(thm)],[f281])).
% 8.63/1.52 fof(f284,plain,(
% 8.63/1.52 sQ8_spl|sQ9_spl|~sQ6_spl),
% 8.63/1.52 inference(split_clause,[status(thm)],[f276,f278,f281,f256])).
% 8.63/1.52 fof(f301,plain,(
% 8.63/1.52 $false|~sQ9_spl),
% 8.63/1.52 inference(forward_subsumption_resolution,[status(thm)],[f166,f282])).
% 8.63/1.52 fof(f302,plain,(
% 8.63/1.52 ~sQ9_spl),
% 8.63/1.52 inference(contradiction_clause,[status(thm)],[f301])).
% 8.63/1.52 fof(f323,plain,(
% 8.63/1.52 ![X0,X1,X2,X3]: (~less_than(bottom,X0)|check_cpq(triple(X1,X2,X3))|~sQ8_spl)),
% 8.63/1.52 inference(resolution,[status(thm)],[f279,f104])).
% 8.63/1.52 fof(f324,definition,(
% 8.63/1.52 ![X1,X2,X3]: (sQ10_spl <=> (check_cpq(triple(X1,X2,X3))))),
% 8.63/1.52 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 8.63/1.52 fof(f325,plain,(
% 8.63/1.52 ![X0,X1,X2]: (check_cpq(triple(X0,X1,X2))|~sQ10_spl)),
% 8.63/1.52 inference(component_clause,[status(thm)],[f324])).
% 8.63/1.52 fof(f327,plain,(
% 8.63/1.52 sQ4_spl|sQ10_spl|~sQ8_spl),
% 8.63/1.52 inference(split_clause,[status(thm)],[f323,f232,f324,f278])).
% 8.63/1.52 fof(f328,plain,(
% 8.63/1.52 $false|~sQ4_spl),
% 8.63/1.52 inference(forward_subsumption_resolution,[status(thm)],[f233,f58])).
% 8.63/1.52 fof(f329,plain,(
% 8.63/1.52 ~sQ4_spl),
% 8.63/1.52 inference(contradiction_clause,[status(thm)],[f328])).
% 8.63/1.52 fof(f330,plain,(
% 8.63/1.52 $false|~sQ10_spl),
% 8.63/1.52 inference(backward_subsumption_resolution,[status(thm)],[f168,f325])).
% 8.63/1.52 fof(f333,plain,(
% 8.63/1.52 ~sQ10_spl),
% 8.63/1.52 inference(contradiction_clause,[status(thm)],[f330])).
% 8.63/1.52 fof(f483,plain,(
% 8.63/1.52 ![X0,X1,X2,X3]: (~contains_slb(X0,X1)|remove_cpq(triple(X2,X0,X3),X1)=triple(remove_pqp(X2,X1),remove_slb(X0,X1),bad)|less_than(lookup_slb(X0,X1),X1))),
% 8.63/1.52 inference(resolution,[status(thm)],[f131,f169])).
% 8.63/1.52 fof(f628,definition,(
% 8.63/1.52 sQ20_spl <=> (less_than(lookup_slb(sK3_skl,sK5_skl),sK5_skl))),
% 8.63/1.52 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 8.63/1.52 fof(f629,plain,(
% 8.63/1.52 less_than(lookup_slb(sK3_skl,sK5_skl),sK5_skl)|~sQ20_spl),
% 8.63/1.52 inference(component_clause,[status(thm)],[f628])).
% 8.63/1.52 fof(f675,plain,(
% 8.63/1.52 ![X0,X1]: (~pair_in_list(sK3_skl,X0,X1)|pair_in_list(remove_slb(sK3_skl,sK5_skl),X0,X1)|X0=sK5_skl)),
% 8.63/1.52 inference(resolution,[status(thm)],[f156,f192])).
% 8.63/1.52 fof(f717,plain,(
% 8.63/1.52 pair_in_list(sK3_skl,sK0_skl(sK3_skl),sK1_skl(sK3_skl))),
% 8.63/1.52 inference(resolution,[status(thm)],[f153,f168])).
% 8.63/1.52 fof(f735,plain,(
% 8.63/1.52 ![X0,X1,X2,X3,X4]: (check_cpq(triple(X0,X1,X2))|~check_cpq(triple(X3,X1,X4))|less_than(sK1_skl(X1),sK0_skl(X1)))),
% 8.63/1.52 inference(resolution,[status(thm)],[f153,f152])).
% 8.63/1.52 fof(f741,definition,(
% 8.63/1.52 ![X0,X1]: (sQ24_spl <=> (check_cpq(triple(X0,sK3_skl,X1))))),
% 8.63/1.52 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 8.63/1.52 fof(f742,plain,(
% 8.63/1.52 ![X0,X1]: (check_cpq(triple(X0,sK3_skl,X1))|~sQ24_spl)),
% 8.63/1.52 inference(component_clause,[status(thm)],[f741])).
% 8.63/1.52 fof(f744,definition,(
% 8.63/1.52 sQ25_spl <=> (pair_in_list(remove_slb(sK3_skl,sK5_skl),sK0_skl(sK3_skl),sK1_skl(sK3_skl)))),
% 8.63/1.52 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 8.63/1.52 fof(f745,plain,(
% 8.63/1.52 pair_in_list(remove_slb(sK3_skl,sK5_skl),sK0_skl(sK3_skl),sK1_skl(sK3_skl))|~sQ25_spl),
% 8.63/1.52 inference(component_clause,[status(thm)],[f744])).
% 8.63/1.52 fof(f747,definition,(
% 8.63/1.52 sQ26_spl <=> (sK0_skl(sK3_skl)=sK5_skl)),
% 8.63/1.52 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 8.63/1.52 fof(f748,plain,(
% 8.63/1.52 sK0_skl(sK3_skl)=sK5_skl|~sQ26_spl),
% 8.63/1.52 inference(component_clause,[status(thm)],[f747])).
% 8.63/1.52 fof(f751,plain,(
% 8.63/1.52 ![X0,X1,X2,X3,X4]: (check_cpq(triple(X0,X1,X2))|~check_cpq(triple(X3,X1,X4)))),
% 8.63/1.52 inference(forward_subsumption_resolution,[status(thm)],[f735,f154])).
% 8.63/1.52 fof(f756,plain,(
% 8.63/1.52 ![X0,X1]: (check_cpq(triple(X0,sK3_skl,X1))|~less_than(sK1_skl(sK3_skl),sK5_skl)|~sQ26_spl)),
% 8.63/1.52 inference(paramodulation,[status(thm)],[f748,f154])).
% 8.63/1.52 fof(f757,plain,(
% 8.63/1.52 ![X0,X1]: (check_cpq(triple(X0,sK3_skl,X1))|pair_in_list(sK3_skl,sK5_skl,sK1_skl(sK3_skl))|~sQ26_spl)),
% 8.63/1.52 inference(paramodulation,[status(thm)],[f748,f153])).
% 8.63/1.52 fof(f758,definition,(
% 8.63/1.52 sQ27_spl <=> (less_than(sK1_skl(sK3_skl),sK5_skl))),
% 8.63/1.52 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 8.63/1.52 fof(f760,plain,(
% 8.63/1.52 ~less_than(sK1_skl(sK3_skl),sK5_skl)|sQ27_spl),
% 8.63/1.52 inference(component_clause,[status(thm)],[f758])).
% 8.63/1.52 fof(f761,plain,(
% 8.63/1.52 sQ24_spl|~sQ27_spl|~sQ26_spl),
% 8.63/1.52 inference(split_clause,[status(thm)],[f756,f741,f758,f747])).
% 8.63/1.52 fof(f762,definition,(
% 8.63/1.52 sQ28_spl <=> (pair_in_list(sK3_skl,sK5_skl,sK1_skl(sK3_skl)))),
% 8.63/1.52 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 8.63/1.52 fof(f763,plain,(
% 8.63/1.52 pair_in_list(sK3_skl,sK5_skl,sK1_skl(sK3_skl))|~sQ28_spl),
% 8.63/1.52 inference(component_clause,[status(thm)],[f762])).
% 8.63/1.52 fof(f765,plain,(
% 8.63/1.52 sQ24_spl|sQ28_spl|~sQ26_spl),
% 8.63/1.52 inference(split_clause,[status(thm)],[f757,f741,f762,f747])).
% 8.63/1.52 fof(f766,plain,(
% 8.63/1.52 $false|~sQ24_spl),
% 8.63/1.52 inference(backward_subsumption_resolution,[status(thm)],[f168,f742])).
% 8.63/1.52 fof(f767,plain,(
% 8.63/1.52 ~sQ24_spl),
% 8.63/1.52 inference(contradiction_clause,[status(thm)],[f766])).
% 8.63/1.52 fof(f845,plain,(
% 8.63/1.52 less_than(sK1_skl(sK3_skl),sK5_skl)|~sQ28_spl|~sQ1_spl),
% 8.63/1.52 inference(resolution,[status(thm)],[f763,f199])).
% 8.63/1.52 fof(f852,plain,(
% 8.63/1.52 $false|sQ27_spl|~sQ28_spl|~sQ1_spl),
% 8.63/1.52 inference(forward_subsumption_resolution,[status(thm)],[f845,f760])).
% 8.63/1.52 fof(f853,plain,(
% 8.63/1.52 sQ27_spl|~sQ28_spl|~sQ1_spl),
% 8.63/1.52 inference(contradiction_clause,[status(thm)],[f852])).
% 8.63/1.52 fof(f854,plain,(
% 8.63/1.52 pair_in_list(remove_slb(sK3_skl,sK5_skl),sK0_skl(sK3_skl),sK1_skl(sK3_skl))|sK0_skl(sK3_skl)=sK5_skl),
% 8.63/1.52 inference(resolution,[status(thm)],[f717,f675])).
% 8.63/1.52 fof(f860,plain,(
% 8.63/1.52 sQ25_spl|sQ26_spl),
% 8.63/1.52 inference(split_clause,[status(thm)],[f854,f744,f747])).
% 8.63/1.52 fof(f864,definition,(
% 8.63/1.52 sQ33_spl <=> (less_than(sK1_skl(sK3_skl),sK0_skl(sK3_skl)))),
% 8.63/1.52 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 8.63/1.52 fof(f865,plain,(
% 8.63/1.52 less_than(sK1_skl(sK3_skl),sK0_skl(sK3_skl))|~sQ33_spl),
% 8.63/1.52 inference(component_clause,[status(thm)],[f864])).
% 8.63/1.52 fof(f932,plain,(
% 8.63/1.52 ![X0,X1]: (check_cpq(triple(X0,sK3_skl,X1))|~sQ33_spl)),
% 8.63/1.52 inference(resolution,[status(thm)],[f865,f154])).
% 8.63/1.52 fof(f941,plain,(
% 8.63/1.52 sQ24_spl|~sQ33_spl),
% 8.63/1.52 inference(split_clause,[status(thm)],[f932,f741,f864])).
% 8.63/1.52 fof(f1099,plain,(
% 8.63/1.52 ![X0,X1]: (remove_cpq(triple(X0,sK3_skl,X1),sK5_skl)=triple(remove_pqp(X0,sK5_skl),remove_slb(sK3_skl,sK5_skl),bad)|less_than(lookup_slb(sK3_skl,sK5_skl),sK5_skl))),
% 8.63/1.52 inference(resolution,[status(thm)],[f483,f192])).
% 8.63/1.52 fof(f1110,definition,(
% 8.63/1.52 ![X0,X1]: (sQ43_spl <=> (remove_cpq(triple(X0,sK3_skl,X1),sK5_skl)=triple(remove_pqp(X0,sK5_skl),remove_slb(sK3_skl,sK5_skl),bad)))),
% 8.63/1.52 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 8.63/1.52 fof(f1111,plain,(
% 8.63/1.52 ![X0,X1]: (remove_cpq(triple(X0,sK3_skl,X1),sK5_skl)=triple(remove_pqp(X0,sK5_skl),remove_slb(sK3_skl,sK5_skl),bad)|~sQ43_spl)),
% 8.63/1.52 inference(component_clause,[status(thm)],[f1110])).
% 8.63/1.52 fof(f1113,plain,(
% 8.63/1.52 sQ43_spl|sQ20_spl),
% 8.63/1.52 inference(split_clause,[status(thm)],[f1099,f1110,f628])).
% 8.63/1.52 fof(f1223,definition,(
% 8.63/1.52 ![X0,X1]: (sQ53_spl <=> (remove_cpq(triple(X0,sK3_skl,X1),sK5_skl)=triple(remove_pqp(X0,sK5_skl),remove_slb(sK3_skl,sK5_skl),X1)))),
% 8.63/1.52 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 8.63/1.52 fof(f1224,plain,(
% 8.63/1.52 ![X0,X1]: (remove_cpq(triple(X0,sK3_skl,X1),sK5_skl)=triple(remove_pqp(X0,sK5_skl),remove_slb(sK3_skl,sK5_skl),X1)|~sQ53_spl)),
% 8.63/1.52 inference(component_clause,[status(thm)],[f1223])).
% 8.63/1.52 fof(f1380,plain,(
% 8.63/1.52 ![X0,X1,X2,X3]: (check_cpq(triple(X0,remove_slb(sK3_skl,sK5_skl),X1))|~check_cpq(remove_cpq(triple(X2,sK3_skl,X3),sK5_skl))|~sQ53_spl)),
% 8.63/1.52 inference(paramodulation,[status(thm)],[f1224,f751])).
% 8.63/1.52 fof(f1409,definition,(
% 8.63/1.52 ![X0,X1]: (sQ60_spl <=> (check_cpq(triple(X0,remove_slb(sK3_skl,sK5_skl),X1))))),
% 8.63/1.52 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 8.63/1.52 fof(f1410,plain,(
% 8.63/1.52 ![X0,X1]: (check_cpq(triple(X0,remove_slb(sK3_skl,sK5_skl),X1))|~sQ60_spl)),
% 8.63/1.52 inference(component_clause,[status(thm)],[f1409])).
% 8.63/1.52 fof(f1420,definition,(
% 8.63/1.52 ![X2,X3]: (sQ63_spl <=> (~check_cpq(remove_cpq(triple(X2,sK3_skl,X3),sK5_skl))))),
% 8.63/1.52 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 8.63/1.52 fof(f1421,plain,(
% 8.63/1.52 ![X0,X1]: (~check_cpq(remove_cpq(triple(X0,sK3_skl,X1),sK5_skl))|~sQ63_spl)),
% 8.63/1.52 inference(component_clause,[status(thm)],[f1420])).
% 8.63/1.52 fof(f1423,plain,(
% 8.63/1.52 sQ60_spl|sQ63_spl|~sQ53_spl),
% 8.63/1.52 inference(split_clause,[status(thm)],[f1380,f1409,f1420,f1223])).
% 8.63/1.52 fof(f1888,plain,(
% 8.63/1.52 ![X0,X1]: (~ok(remove_cpq(triple(X0,sK3_skl,X1),sK5_skl))|~sQ43_spl)),
% 8.63/1.52 inference(paramodulation,[status(thm)],[f1111,f118])).
% 8.63/1.52 fof(f1924,plain,(
% 8.63/1.52 $false|~sQ43_spl),
% 8.63/1.52 inference(backward_subsumption_resolution,[status(thm)],[f167,f1888])).
% 8.63/1.52 fof(f1952,plain,(
% 8.63/1.52 ~sQ43_spl),
% 8.63/1.52 inference(contradiction_clause,[status(thm)],[f1924])).
% 8.63/1.52 fof(f1953,plain,(
% 8.63/1.52 ![X0,X1]: (~contains_slb(sK3_skl,sK5_skl)|remove_cpq(triple(X0,sK3_skl,X1),sK5_skl)=triple(remove_pqp(X0,sK5_skl),remove_slb(sK3_skl,sK5_skl),X1)|~sQ20_spl)),
% 8.63/1.52 inference(resolution,[status(thm)],[f629,f128])).
% 8.63/1.52 fof(f1958,plain,(
% 8.63/1.52 ~sQ5_spl|sQ53_spl|~sQ20_spl),
% 8.63/1.52 inference(split_clause,[status(thm)],[f1953,f253,f1223,f628])).
% 8.63/1.52 fof(f4220,plain,(
% 8.63/1.52 ![X0,X1]: (~check_cpq(triple(X0,remove_slb(sK3_skl,sK5_skl),X1))|less_than(sK1_skl(sK3_skl),sK0_skl(sK3_skl))|~sQ25_spl)),
% 8.63/1.52 inference(resolution,[status(thm)],[f745,f152])).
% 8.63/1.52 fof(f4231,definition,(
% 8.63/1.52 ![X0,X1]: (sQ119_spl <=> (~check_cpq(triple(X0,remove_slb(sK3_skl,sK5_skl),X1))))),
% 8.63/1.52 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 8.63/1.52 fof(f4232,plain,(
% 8.63/1.52 ![X0,X1]: (~check_cpq(triple(X0,remove_slb(sK3_skl,sK5_skl),X1))|~sQ119_spl)),
% 8.63/1.52 inference(component_clause,[status(thm)],[f4231])).
% 8.63/1.52 fof(f4234,plain,(
% 8.63/1.52 sQ119_spl|sQ33_spl|~sQ25_spl),
% 8.63/1.52 inference(split_clause,[status(thm)],[f4220,f4231,f864,f744])).
% 8.63/1.52 fof(f4239,plain,(
% 8.63/1.52 $false|~sQ60_spl|~sQ119_spl),
% 8.63/1.52 inference(forward_subsumption_resolution,[status(thm)],[f4232,f1410])).
% 8.63/1.52 fof(f4240,plain,(
% 8.63/1.52 ~sQ60_spl|~sQ119_spl),
% 8.63/1.52 inference(contradiction_clause,[status(thm)],[f4239])).
% 8.63/1.53 fof(f4241,plain,(
% 8.63/1.53 $false|~sQ63_spl),
% 8.63/1.53 inference(backward_subsumption_resolution,[status(thm)],[f166,f1421])).
% 8.63/1.53 fof(f4244,plain,(
% 8.63/1.53 ~sQ63_spl),
% 8.63/1.53 inference(contradiction_clause,[status(thm)],[f4241])).
% 8.63/1.53 fof(f4245,plain,(
% 8.63/1.53 $false),
% 8.63/1.53 inference(sat_refutation,[status(thm)],[f201,f203,f259,f284,f302,f327,f329,f333,f761,f765,f767,f853,f860,f941,f1113,f1423,f1952,f1958,f4234,f4240,f4244])).
% 8.63/1.53 % SZS output end CNFRefutation for theBenchmark.p
% 8.63/1.53 % Elapsed time: 1.160760 seconds
% 8.63/1.53 % CPU time: 8.856622 seconds
% 8.63/1.53 % Total memory used: 197.230 MB
% 8.63/1.53 % Net memory used: 184.314 MB
%------------------------------------------------------------------------------