%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV391+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/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 02:47:34 PM UTC 2026
% Result : Theorem 10.26s 1.78s
% Output : CNFRefutation 10.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 87
% Syntax : Number of formulae : 381 ( 32 unt; 64 def)
% Number of atoms : 995 ( 134 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 1002 ( 388 ~; 489 |; 38 &)
% ( 71 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 72 ( 70 usr; 65 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 7 con; 0-3 aty)
% Number of variables : 906 ( 894 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [U,V,W] :
( ( less_than(V,W)
& less_than(U,V) )
=> less_than(U,W) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [U,V] :
( less_than(V,U)
| less_than(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [U] : less_than(U,U),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [U,V] :
( strictly_less_than(U,V)
<=> ( ~ less_than(V,U)
& less_than(U,V) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [U] : less_than(bottom,U),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [U,V,W,X] :
( contains_slb(insert_slb(U,pair(V,X)),W)
<=> ( V = W
| contains_slb(U,W) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [U,V] : ~ pair_in_list(create_slb,U,V),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [U,V,W,X,Y] :
( pair_in_list(insert_slb(U,pair(V,X)),W,Y)
<=> ( ( X = Y
& V = W )
| pair_in_list(U,W,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [U,V,W] : remove_slb(insert_slb(U,pair(V,W)),V) = U,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [U,V,W,X] :
( ( contains_slb(U,W)
& V != W )
=> remove_slb(insert_slb(U,pair(V,X)),W) = insert_slb(remove_slb(U,W),pair(V,X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [U,V,W] : lookup_slb(insert_slb(U,pair(V,W)),V) = W,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [U,V,W,X] :
( ( contains_slb(U,W)
& V != W )
=> lookup_slb(insert_slb(U,pair(V,X)),W) = lookup_slb(U,W) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [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)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [U,V] : check_cpq(triple(U,create_slb,V)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [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)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [U,V,W,X] :
( ~ contains_slb(V,X)
=> remove_cpq(triple(U,V,W),X) = triple(U,V,bad) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [U,V,W,X] :
( ( less_than(lookup_slb(V,X),X)
& contains_slb(V,X) )
=> remove_cpq(triple(U,V,W),X) = triple(remove_pqp(U,X),remove_slb(V,X),W) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [U,V,W,X] :
( ( strictly_less_than(X,lookup_slb(V,X))
& contains_slb(V,X) )
=> remove_cpq(triple(U,V,W),X) = triple(remove_pqp(U,X),remove_slb(V,X),bad) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,lemma,
! [U,V,W] :
( check_cpq(triple(U,V,W))
<=> ! [X,Y] :
( pair_in_list(V,X,Y)
=> less_than(Y,X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,lemma,
! [U,V,W] :
( pair_in_list(U,V,W)
=> ! [X] :
( contains_slb(U,X)
=> ( V = X
| pair_in_list(remove_slb(U,X),V,W) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,lemma,
! [U,V,W,X] :
( ( ok(remove_cpq(triple(U,V,W),X))
& check_cpq(remove_cpq(triple(U,V,W),X)) )
=> ! [Y] :
( pair_in_list(V,X,Y)
=> less_than(Y,X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,lemma,
! [U,V,W,X] :
( ok(remove_cpq(triple(U,V,W),X))
=> contains_slb(V,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,conjecture,
! [U,V,W,X] :
( ( ok(remove_cpq(triple(U,V,W),X))
& check_cpq(remove_cpq(triple(U,V,W),X)) )
=> check_cpq(triple(U,V,W)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,negated_conjecture,
~ ! [U,V,W,X] :
( ( ok(remove_cpq(triple(U,V,W),X))
& check_cpq(remove_cpq(triple(U,V,W),X)) )
=> check_cpq(triple(U,V,W)) ),
inference(negated_conjecture,[status(cth)],[f46]) ).
fof(f48,plain,
! [U,V,W] :
( less_than(U,W)
| ~ less_than(V,W)
| ~ less_than(U,V) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f49,plain,
! [U,W] :
( less_than(U,W)
| ! [V] :
( ~ less_than(V,W)
| ~ less_than(U,V) ) ),
inference(miniscoping,[status(thm)],[f48]) ).
fof(f50,plain,
! [X0,X1,X2] :
( less_than(X0,X2)
| ~ less_than(X1,X2)
| ~ less_than(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f51,plain,
! [X0,X1] :
( less_than(X1,X0)
| less_than(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f52,plain,
! [X0] : less_than(X0,X0),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f53,plain,
! [U,V] :
( ( less_than(V,U)
| ~ less_than(U,V)
| strictly_less_than(U,V) )
& ( ( ~ less_than(V,U)
& less_than(U,V) )
| ~ strictly_less_than(U,V) ) ),
inference(NNF_transformation,[status(thm)],[f4]) ).
fof(f54,plain,
( ! [U,V] :
( less_than(V,U)
| ~ less_than(U,V)
| strictly_less_than(U,V) )
& ! [U,V] :
( ( ~ less_than(V,U)
& less_than(U,V) )
| ~ strictly_less_than(U,V) ) ),
inference(miniscoping,[status(thm)],[f53]) ).
fof(f57,plain,
! [X0,X1] :
( less_than(X1,X0)
| ~ less_than(X0,X1)
| strictly_less_than(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f58,plain,
! [X0] : less_than(bottom,X0),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f62,plain,
! [U,V,W,X] :
( ( ( V != W
& ~ contains_slb(U,W) )
| contains_slb(insert_slb(U,pair(V,X)),W) )
& ( V = W
| contains_slb(U,W)
| ~ contains_slb(insert_slb(U,pair(V,X)),W) ) ),
inference(NNF_transformation,[status(thm)],[f9]) ).
fof(f63,plain,
( ! [U,V,W] :
( ( V != W
& ~ contains_slb(U,W) )
| ! [X] : contains_slb(insert_slb(U,pair(V,X)),W) )
& ! [U,V,W] :
( V = W
| contains_slb(U,W)
| ! [X] : ~ contains_slb(insert_slb(U,pair(V,X)),W) ) ),
inference(miniscoping,[status(thm)],[f62]) ).
fof(f65,plain,
! [X0,X1,X2,X3] :
( ~ contains_slb(X0,X3)
| contains_slb(insert_slb(X0,pair(X1,X2)),X3) ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f66,plain,
! [X0,X1,X2,X3] :
( X1 != X3
| contains_slb(insert_slb(X0,pair(X1,X2)),X3) ),
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f67,plain,
! [X0,X1] : ~ pair_in_list(create_slb,X0,X1),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f68,plain,
! [U,V,W,X,Y] :
( ( ( ( X != Y
| V != W )
& ~ pair_in_list(U,W,Y) )
| pair_in_list(insert_slb(U,pair(V,X)),W,Y) )
& ( ( X = Y
& V = W )
| pair_in_list(U,W,Y)
| ~ pair_in_list(insert_slb(U,pair(V,X)),W,Y) ) ),
inference(NNF_transformation,[status(thm)],[f11]) ).
fof(f69,plain,
( ! [U,V,W,X,Y] :
( ( ( X != Y
| V != W )
& ~ pair_in_list(U,W,Y) )
| pair_in_list(insert_slb(U,pair(V,X)),W,Y) )
& ! [U,V,W,X,Y] :
( ( X = Y
& V = W )
| pair_in_list(U,W,Y)
| ~ pair_in_list(insert_slb(U,pair(V,X)),W,Y) ) ),
inference(miniscoping,[status(thm)],[f68]) ).
fof(f70,plain,
! [X0,X1,X2,X3,X4] :
( X1 = X3
| pair_in_list(X0,X3,X4)
| ~ pair_in_list(insert_slb(X0,pair(X1,X2)),X3,X4) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f72,plain,
! [X0,X1,X2,X3,X4] :
( ~ pair_in_list(X0,X3,X4)
| pair_in_list(insert_slb(X0,pair(X1,X2)),X3,X4) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f73,plain,
! [X0,X1,X2,X3,X4] :
( X2 != X4
| X1 != X3
| pair_in_list(insert_slb(X0,pair(X1,X2)),X3,X4) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f74,plain,
! [X0,X1,X2] : remove_slb(insert_slb(X0,pair(X1,X2)),X1) = X0,
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f75,plain,
! [U,V,W,X] :
( remove_slb(insert_slb(U,pair(V,X)),W) = insert_slb(remove_slb(U,W),pair(V,X))
| ~ contains_slb(U,W)
| V = W ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f76,plain,
! [U,V,W] :
( ! [X] : remove_slb(insert_slb(U,pair(V,X)),W) = insert_slb(remove_slb(U,W),pair(V,X))
| ~ contains_slb(U,W)
| V = W ),
inference(miniscoping,[status(thm)],[f75]) ).
fof(f77,plain,
! [X0,X1,X2,X3] :
( remove_slb(insert_slb(X2,pair(X0,X3)),X1) = insert_slb(remove_slb(X2,X1),pair(X0,X3))
| ~ contains_slb(X2,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f78,plain,
! [X0,X1,X2] : lookup_slb(insert_slb(X0,pair(X1,X2)),X1) = X2,
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f79,plain,
! [U,V,W,X] :
( lookup_slb(insert_slb(U,pair(V,X)),W) = lookup_slb(U,W)
| ~ contains_slb(U,W)
| V = W ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f80,plain,
! [U,V,W] :
( ! [X] : lookup_slb(insert_slb(U,pair(V,X)),W) = lookup_slb(U,W)
| ~ contains_slb(U,W)
| V = W ),
inference(miniscoping,[status(thm)],[f79]) ).
fof(f81,plain,
! [X0,X1,X2,X3] :
( lookup_slb(insert_slb(X2,pair(X0,X3)),X1) = lookup_slb(X2,X1)
| ~ contains_slb(X2,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f86,plain,
! [U,V,W,X] :
( update_slb(insert_slb(U,pair(V,X)),W) = insert_slb(update_slb(U,W),pair(V,X))
| ~ less_than(W,X) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f87,plain,
! [W,X] :
( ! [U,V] : update_slb(insert_slb(U,pair(V,X)),W) = insert_slb(update_slb(U,W),pair(V,X))
| ~ less_than(W,X) ),
inference(miniscoping,[status(thm)],[f86]) ).
fof(f88,plain,
! [X0,X1,X2,X3] :
( update_slb(insert_slb(X2,pair(X3,X1)),X0) = insert_slb(update_slb(X2,X0),pair(X3,X1))
| ~ less_than(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f100,plain,
! [X0,X1] : check_cpq(triple(X0,create_slb,X1)),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f101,plain,
! [U,V,W,X,Y] :
( ( check_cpq(triple(U,insert_slb(V,pair(X,Y)),W))
<=> check_cpq(triple(U,V,W)) )
| ~ less_than(Y,X) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f102,plain,
! [U,V,W,X,Y] :
( ( ( ~ check_cpq(triple(U,V,W))
| 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)) ) )
| ~ less_than(Y,X) ),
inference(NNF_transformation,[status(thm)],[f101]) ).
fof(f103,plain,
! [X,Y] :
( ( ! [U,V,W] :
( ~ check_cpq(triple(U,V,W))
| check_cpq(triple(U,insert_slb(V,pair(X,Y)),W)) )
& ! [U,V,W] :
( check_cpq(triple(U,V,W))
| ~ check_cpq(triple(U,insert_slb(V,pair(X,Y)),W)) ) )
| ~ less_than(Y,X) ),
inference(miniscoping,[status(thm)],[f102]) ).
fof(f104,plain,
! [X0,X1,X2,X3,X4] :
( check_cpq(triple(X2,X3,X4))
| ~ check_cpq(triple(X2,insert_slb(X3,pair(X1,X0)),X4))
| ~ less_than(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f105,plain,
! [X0,X1,X2,X3,X4] :
( ~ check_cpq(triple(X2,X3,X4))
| check_cpq(triple(X2,insert_slb(X3,pair(X1,X0)),X4))
| ~ less_than(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f123,plain,
! [U,V,W,X] :
( remove_cpq(triple(U,V,W),X) = triple(U,V,bad)
| contains_slb(V,X) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f124,plain,
! [V,X] :
( ! [U,W] : remove_cpq(triple(U,V,W),X) = triple(U,V,bad)
| contains_slb(V,X) ),
inference(miniscoping,[status(thm)],[f123]) ).
fof(f125,plain,
! [X0,X1,X2,X3] :
( remove_cpq(triple(X2,X0,X3),X1) = triple(X2,X0,bad)
| contains_slb(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f126,plain,
! [U,V,W,X] :
( remove_cpq(triple(U,V,W),X) = triple(remove_pqp(U,X),remove_slb(V,X),W)
| ~ less_than(lookup_slb(V,X),X)
| ~ contains_slb(V,X) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f127,plain,
! [V,X] :
( ! [U,W] : remove_cpq(triple(U,V,W),X) = triple(remove_pqp(U,X),remove_slb(V,X),W)
| ~ less_than(lookup_slb(V,X),X)
| ~ contains_slb(V,X) ),
inference(miniscoping,[status(thm)],[f126]) ).
fof(f128,plain,
! [X0,X1,X2,X3] :
( remove_cpq(triple(X2,X0,X3),X1) = triple(remove_pqp(X2,X1),remove_slb(X0,X1),X3)
| ~ less_than(lookup_slb(X0,X1),X1)
| ~ contains_slb(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f129,plain,
! [U,V,W,X] :
( remove_cpq(triple(U,V,W),X) = triple(remove_pqp(U,X),remove_slb(V,X),bad)
| ~ strictly_less_than(X,lookup_slb(V,X))
| ~ contains_slb(V,X) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f130,plain,
! [V,X] :
( ! [U,W] : remove_cpq(triple(U,V,W),X) = triple(remove_pqp(U,X),remove_slb(V,X),bad)
| ~ strictly_less_than(X,lookup_slb(V,X))
| ~ contains_slb(V,X) ),
inference(miniscoping,[status(thm)],[f129]) ).
fof(f131,plain,
! [X0,X1,X2,X3] :
( remove_cpq(triple(X2,X0,X3),X1) = triple(remove_pqp(X2,X1),remove_slb(X0,X1),bad)
| ~ strictly_less_than(X1,lookup_slb(X0,X1))
| ~ contains_slb(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f148,plain,
! [U,V,W] :
( check_cpq(triple(U,V,W))
<=> ! [X,Y] :
( less_than(Y,X)
| ~ pair_in_list(V,X,Y) ) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f149,plain,
! [U,V,W] :
( ( ? [X,Y] :
( ~ less_than(Y,X)
& pair_in_list(V,X,Y) )
| check_cpq(triple(U,V,W)) )
& ( ! [X,Y] :
( less_than(Y,X)
| ~ pair_in_list(V,X,Y) )
| ~ check_cpq(triple(U,V,W)) ) ),
inference(NNF_transformation,[status(thm)],[f148]) ).
fof(f150,plain,
( ! [V] :
( ? [X,Y] :
( ~ less_than(Y,X)
& pair_in_list(V,X,Y) )
| ! [U,W] : check_cpq(triple(U,V,W)) )
& ! [V] :
( ! [X,Y] :
( less_than(Y,X)
| ~ pair_in_list(V,X,Y) )
| ! [U,W] : ~ check_cpq(triple(U,V,W)) ) ),
inference(miniscoping,[status(thm)],[f149]) ).
fof(f151,plain,
( ! [V] :
( ( ~ less_than(sK1_skl(V),sK0_skl(V))
& pair_in_list(V,sK0_skl(V),sK1_skl(V)) )
| ! [U,W] : check_cpq(triple(U,V,W)) )
& ! [V] :
( ! [X,Y] :
( less_than(Y,X)
| ~ pair_in_list(V,X,Y) )
| ! [U,W] : ~ check_cpq(triple(U,V,W)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(X,sK0_skl(V)),skolemize(Y,sK1_skl(V))],[f150]) ).
fof(f152,plain,
! [X0,X1,X2,X3,X4] :
( less_than(X4,X3)
| ~ pair_in_list(X1,X3,X4)
| ~ check_cpq(triple(X0,X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f153,plain,
! [X0,X1,X2] :
( pair_in_list(X1,sK0_skl(X1),sK1_skl(X1))
| check_cpq(triple(X0,X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f154,plain,
! [X0,X1,X2] :
( ~ less_than(sK1_skl(X1),sK0_skl(X1))
| check_cpq(triple(X0,X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f155,plain,
! [U,V,W] :
( ! [X] :
( V = X
| pair_in_list(remove_slb(U,X),V,W)
| ~ contains_slb(U,X) )
| ~ pair_in_list(U,V,W) ),
inference(pre_NNF_transformation,[status(thm)],[f43]) ).
fof(f156,plain,
! [X0,X1,X2,X3] :
( X1 = X3
| pair_in_list(remove_slb(X0,X3),X1,X2)
| ~ contains_slb(X0,X3)
| ~ pair_in_list(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f157,plain,
! [U,V,W,X] :
( ! [Y] :
( less_than(Y,X)
| ~ pair_in_list(V,X,Y) )
| ~ ok(remove_cpq(triple(U,V,W),X))
| ~ check_cpq(remove_cpq(triple(U,V,W),X)) ),
inference(pre_NNF_transformation,[status(thm)],[f44]) ).
fof(f158,plain,
! [V,X] :
( ! [Y] :
( less_than(Y,X)
| ~ pair_in_list(V,X,Y) )
| ! [U,W] :
( ~ ok(remove_cpq(triple(U,V,W),X))
| ~ check_cpq(remove_cpq(triple(U,V,W),X)) ) ),
inference(miniscoping,[status(thm)],[f157]) ).
fof(f159,plain,
! [X0,X1,X2,X3,X4] :
( less_than(X4,X3)
| ~ pair_in_list(X1,X3,X4)
| ~ ok(remove_cpq(triple(X0,X1,X2),X3))
| ~ check_cpq(remove_cpq(triple(X0,X1,X2),X3)) ),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f160,plain,
! [U,V,W,X] :
( contains_slb(V,X)
| ~ ok(remove_cpq(triple(U,V,W),X)) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f161,plain,
! [V,X] :
( contains_slb(V,X)
| ! [U,W] : ~ ok(remove_cpq(triple(U,V,W),X)) ),
inference(miniscoping,[status(thm)],[f160]) ).
fof(f162,plain,
! [X0,X1,X2,X3] :
( contains_slb(X1,X3)
| ~ ok(remove_cpq(triple(X0,X1,X2),X3)) ),
inference(cnf_transformation,[status(thm)],[f161]) ).
fof(f163,plain,
? [U,V,W,X] :
( ~ check_cpq(triple(U,V,W))
& ok(remove_cpq(triple(U,V,W),X))
& check_cpq(remove_cpq(triple(U,V,W),X)) ),
inference(pre_NNF_transformation,[status(thm)],[f47]) ).
fof(f164,plain,
? [U,V,W] :
( ~ check_cpq(triple(U,V,W))
& ? [X] :
( ok(remove_cpq(triple(U,V,W),X))
& check_cpq(remove_cpq(triple(U,V,W),X)) ) ),
inference(miniscoping,[status(thm)],[f163]) ).
fof(f165,plain,
( ~ check_cpq(triple(sK2_skl,sK3_skl,sK4_skl))
& ok(remove_cpq(triple(sK2_skl,sK3_skl,sK4_skl),sK5_skl))
& check_cpq(remove_cpq(triple(sK2_skl,sK3_skl,sK4_skl),sK5_skl)) ),
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]) ).
fof(f166,plain,
check_cpq(remove_cpq(triple(sK2_skl,sK3_skl,sK4_skl),sK5_skl)),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f167,plain,
ok(remove_cpq(triple(sK2_skl,sK3_skl,sK4_skl),sK5_skl)),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f168,plain,
~ check_cpq(triple(sK2_skl,sK3_skl,sK4_skl)),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f169,plain,
! [X0,X1] :
( less_than(X1,X0)
| strictly_less_than(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f57,f51]) ).
fof(f170,plain,
! [X0,X1,X2] : contains_slb(insert_slb(X0,pair(X1,X2)),X1),
inference(destructive_equality_resolution,[status(thm)],[f66]) ).
fof(f171,plain,
! [X0,X1,X2] : pair_in_list(insert_slb(X0,pair(X1,X2)),X1,X2),
inference(destructive_equality_resolution,[status(thm)],[f73]) ).
fof(f174,plain,
contains_slb(sK3_skl,sK5_skl),
inference(resolution,[status(thm)],[f162,f167]) ).
fof(f175,plain,
! [X0,X1,X2,X3] :
( ~ check_cpq(triple(X0,X1,X3))
| check_cpq(triple(X0,insert_slb(X1,pair(X2,X2)),X3)) ),
inference(resolution,[status(thm)],[f52,f105]) ).
fof(f176,plain,
! [X0,X1,X2,X3] :
( ~ check_cpq(triple(X0,X1,X3))
| check_cpq(triple(X0,insert_slb(X1,pair(X2,bottom)),X3)) ),
inference(resolution,[status(thm)],[f58,f105]) ).
fof(f177,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ check_cpq(triple(X3,X4,X5))
| check_cpq(triple(X3,insert_slb(X4,pair(X2,X0)),X5))
| ~ less_than(X1,X2)
| ~ less_than(X0,X1) ),
inference(resolution,[status(thm)],[f50,f105]) ).
fof(f179,plain,
! [X0,X1,X2,X3,X4] :
( ~ check_cpq(triple(X2,X3,X4))
| check_cpq(triple(X2,insert_slb(X3,pair(X0,X1)),X4))
| less_than(X0,X1) ),
inference(resolution,[status(thm)],[f51,f105]) ).
fof(f182,plain,
! [X0,X1,X2] : check_cpq(triple(X0,insert_slb(create_slb,pair(X1,X1)),X2)),
inference(resolution,[status(thm)],[f175,f100]) ).
fof(f183,plain,
! [X0,X1,X2] :
( check_cpq(triple(X1,create_slb,X2))
| ~ less_than(X0,X0) ),
inference(resolution,[status(thm)],[f182,f104]) ).
fof(f184,plain,
! [X0,X1,X2,X3] : check_cpq(triple(X0,insert_slb(insert_slb(create_slb,pair(X1,X1)),pair(X2,X2)),X3)),
inference(resolution,[status(thm)],[f182,f175]) ).
fof(f185,definition,
! [X0] :
( sQ0_spl
<=> ~ less_than(X0,X0) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f186,plain,
! [X0] :
( ~ sQ0_spl
| ~ less_than(X0,X0) ),
inference(component_clause,[status(thm)],[f185]) ).
fof(f188,definition,
! [X1,X2] :
( sQ1_spl
<=> check_cpq(triple(X1,create_slb,X2)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f191,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f183,f185,f188]) ).
fof(f192,plain,
( ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f186,f52]) ).
fof(f193,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f192]) ).
fof(f194,plain,
! [X0,X1,X2,X3] :
( check_cpq(triple(X1,insert_slb(create_slb,pair(X2,X2)),X3))
| ~ less_than(X0,X0) ),
inference(resolution,[status(thm)],[f184,f104]) ).
fof(f195,plain,
! [X0,X1,X2,X3,X4] : check_cpq(triple(X0,insert_slb(insert_slb(insert_slb(create_slb,pair(X1,X1)),pair(X2,X2)),pair(X3,X3)),X4)),
inference(resolution,[status(thm)],[f184,f175]) ).
fof(f196,definition,
! [X1,X2,X3] :
( sQ2_spl
<=> check_cpq(triple(X1,insert_slb(create_slb,pair(X2,X2)),X3)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f199,plain,
( sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f194,f185,f196]) ).
fof(f201,plain,
! [X0,X1,X2,X3,X4] :
( check_cpq(triple(X0,insert_slb(insert_slb(X1,pair(X3,bottom)),pair(X4,X4)),X2))
| ~ check_cpq(triple(X0,X1,X2)) ),
inference(resolution,[status(thm)],[f176,f175]) ).
fof(f202,definition,
! [X0,X1,X2] :
( sQ3_spl
<=> ( check_cpq(triple(X0,X1,X2))
| ~ check_cpq(triple(X0,X1,X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f205,definition,
! [X3] :
( sQ4_spl
<=> ~ less_than(bottom,X3) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f206,plain,
! [X0] :
( ~ sQ4_spl
| ~ less_than(bottom,X0) ),
inference(component_clause,[status(thm)],[f205]) ).
fof(f210,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( check_cpq(triple(X3,insert_slb(insert_slb(X4,pair(X2,X0)),pair(X6,X6)),X5))
| ~ check_cpq(triple(X3,X4,X5))
| ~ less_than(X1,X2)
| ~ less_than(X0,X1) ),
inference(resolution,[status(thm)],[f177,f175]) ).
fof(f216,plain,
! [X0,X1,X2,X3,X4,X5] :
( check_cpq(triple(X2,insert_slb(insert_slb(X3,pair(X0,X1)),pair(X5,X5)),X4))
| ~ check_cpq(triple(X2,X3,X4))
| less_than(X0,X1) ),
inference(resolution,[status(thm)],[f179,f175]) ).
fof(f217,definition,
! [X0,X1] :
( sQ6_spl
<=> ( ~ less_than(X1,X0)
| less_than(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f218,plain,
! [X0,X1] :
( ~ sQ6_spl
| ~ less_than(X1,X0)
| less_than(X0,X1) ),
inference(component_clause,[status(thm)],[f217]) ).
fof(f225,plain,
! [X0,X1,X2,X3,X4] :
( check_cpq(triple(X1,insert_slb(insert_slb(create_slb,pair(X2,X2)),pair(X3,X3)),X4))
| ~ less_than(X0,X0) ),
inference(resolution,[status(thm)],[f195,f104]) ).
fof(f226,plain,
! [X0,X1,X2,X3,X4,X5] : check_cpq(triple(X0,insert_slb(insert_slb(insert_slb(insert_slb(create_slb,pair(X1,X1)),pair(X2,X2)),pair(X3,X3)),pair(X4,X4)),X5)),
inference(resolution,[status(thm)],[f195,f175]) ).
fof(f227,definition,
! [X1,X2,X3,X4] :
( sQ7_spl
<=> check_cpq(triple(X1,insert_slb(insert_slb(create_slb,pair(X2,X2)),pair(X3,X3)),X4)) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f230,plain,
( sQ7_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f225,f185,f227]) ).
fof(f231,plain,
! [X0,X1,X2,X3,X4] :
( check_cpq(triple(X0,insert_slb(X1,pair(X4,bottom)),X2))
| ~ less_than(X3,X3)
| ~ check_cpq(triple(X0,X1,X2)) ),
inference(resolution,[status(thm)],[f201,f104]) ).
fof(f232,plain,
! [X0,X1,X2,X3,X4,X5] :
( check_cpq(triple(X0,insert_slb(insert_slb(insert_slb(X1,pair(X3,bottom)),pair(X4,X4)),pair(X5,X5)),X2))
| ~ check_cpq(triple(X0,X1,X2)) ),
inference(resolution,[status(thm)],[f201,f175]) ).
fof(f233,definition,
! [X0,X1,X2,X4] :
( sQ8_spl
<=> ( check_cpq(triple(X0,insert_slb(X1,pair(X4,bottom)),X2))
| ~ check_cpq(triple(X0,X1,X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f236,plain,
( sQ0_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f231,f233,f185]) ).
fof(f237,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( check_cpq(triple(X3,insert_slb(X4,pair(X2,X0)),X5))
| ~ less_than(X6,X6)
| ~ check_cpq(triple(X3,X4,X5))
| ~ less_than(X1,X2)
| ~ less_than(X0,X1) ),
inference(resolution,[status(thm)],[f210,f104]) ).
fof(f238,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( check_cpq(triple(X3,insert_slb(insert_slb(insert_slb(X4,pair(X2,X0)),pair(X6,X6)),pair(X7,X7)),X5))
| ~ check_cpq(triple(X3,X4,X5))
| ~ less_than(X1,X2)
| ~ less_than(X0,X1) ),
inference(resolution,[status(thm)],[f210,f175]) ).
fof(f239,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ9_spl
<=> ( check_cpq(triple(X3,insert_slb(X4,pair(X2,X0)),X5))
| ~ check_cpq(triple(X3,X4,X5))
| ~ less_than(X1,X2)
| ~ less_than(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f242,plain,
( sQ0_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f237,f239,f185]) ).
fof(f243,plain,
! [X0,X1,X2,X3,X4,X5] :
( check_cpq(triple(X2,insert_slb(X3,pair(X0,X1)),X4))
| ~ less_than(X5,X5)
| ~ check_cpq(triple(X2,X3,X4))
| less_than(X0,X1) ),
inference(resolution,[status(thm)],[f216,f104]) ).
fof(f244,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( check_cpq(triple(X2,insert_slb(insert_slb(insert_slb(X3,pair(X0,X1)),pair(X5,X5)),pair(X6,X6)),X4))
| ~ check_cpq(triple(X2,X3,X4))
| less_than(X0,X1) ),
inference(resolution,[status(thm)],[f216,f175]) ).
fof(f245,definition,
! [X0,X1,X2,X3,X4] :
( sQ10_spl
<=> ( check_cpq(triple(X2,insert_slb(X3,pair(X0,X1)),X4))
| ~ check_cpq(triple(X2,X3,X4))
| less_than(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f248,plain,
( sQ0_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f243,f245,f185]) ).
fof(f249,plain,
! [X0,X1,X2,X3,X4,X5] :
( check_cpq(triple(X1,insert_slb(insert_slb(insert_slb(create_slb,pair(X2,X2)),pair(X3,X3)),pair(X4,X4)),X5))
| ~ less_than(X0,X0) ),
inference(resolution,[status(thm)],[f226,f104]) ).
fof(f251,definition,
! [X1,X2,X3,X4,X5] :
( sQ11_spl
<=> check_cpq(triple(X1,insert_slb(insert_slb(insert_slb(create_slb,pair(X2,X2)),pair(X3,X3)),pair(X4,X4)),X5)) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f254,plain,
( sQ11_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f249,f185,f251]) ).
fof(f255,plain,
! [X0,X1,X2,X3,X4,X5] :
( check_cpq(triple(X0,insert_slb(insert_slb(X1,pair(X4,bottom)),pair(X5,X5)),X2))
| ~ less_than(X3,X3)
| ~ check_cpq(triple(X0,X1,X2)) ),
inference(resolution,[status(thm)],[f232,f104]) ).
fof(f256,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( check_cpq(triple(X0,insert_slb(insert_slb(insert_slb(insert_slb(X1,pair(X3,bottom)),pair(X4,X4)),pair(X5,X5)),pair(X6,X6)),X2))
| ~ check_cpq(triple(X0,X1,X2)) ),
inference(resolution,[status(thm)],[f232,f175]) ).
fof(f257,definition,
! [X0,X1,X2,X4,X5] :
( sQ12_spl
<=> ( check_cpq(triple(X0,insert_slb(insert_slb(X1,pair(X4,bottom)),pair(X5,X5)),X2))
| ~ check_cpq(triple(X0,X1,X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f260,plain,
( sQ0_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f255,f257,f185]) ).
fof(f261,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( check_cpq(triple(X2,insert_slb(insert_slb(X3,pair(X0,X1)),pair(X6,X6)),X4))
| ~ less_than(X5,X5)
| ~ check_cpq(triple(X2,X3,X4))
| less_than(X0,X1) ),
inference(resolution,[status(thm)],[f244,f104]) ).
fof(f263,definition,
! [X0,X1,X2,X3,X4,X6] :
( sQ13_spl
<=> ( check_cpq(triple(X2,insert_slb(insert_slb(X3,pair(X0,X1)),pair(X6,X6)),X4))
| ~ check_cpq(triple(X2,X3,X4))
| less_than(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f266,plain,
( sQ0_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f261,f263,f185]) ).
fof(f267,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( check_cpq(triple(X3,insert_slb(insert_slb(X4,pair(X2,X0)),pair(X7,X7)),X5))
| ~ less_than(X6,X6)
| ~ check_cpq(triple(X3,X4,X5))
| ~ less_than(X1,X2)
| ~ less_than(X0,X1) ),
inference(resolution,[status(thm)],[f238,f104]) ).
fof(f269,definition,
! [X0,X1,X2,X3,X4,X5,X7] :
( sQ14_spl
<=> ( check_cpq(triple(X3,insert_slb(insert_slb(X4,pair(X2,X0)),pair(X7,X7)),X5))
| ~ check_cpq(triple(X3,X4,X5))
| ~ less_than(X1,X2)
| ~ less_than(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f272,plain,
( sQ0_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f267,f269,f185]) ).
fof(f273,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( check_cpq(triple(X0,insert_slb(insert_slb(insert_slb(X1,pair(X4,bottom)),pair(X5,X5)),pair(X6,X6)),X2))
| ~ less_than(X3,X3)
| ~ check_cpq(triple(X0,X1,X2)) ),
inference(resolution,[status(thm)],[f256,f104]) ).
fof(f275,definition,
! [X0,X1,X2,X4,X5,X6] :
( sQ15_spl
<=> ( check_cpq(triple(X0,insert_slb(insert_slb(insert_slb(X1,pair(X4,bottom)),pair(X5,X5)),pair(X6,X6)),X2))
| ~ check_cpq(triple(X0,X1,X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f278,plain,
( sQ0_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f273,f275,f185]) ).
fof(f281,plain,
! [X0,X1,X2,X3,X4] :
( less_than(X3,X2)
| ~ check_cpq(triple(X0,insert_slb(X1,pair(X2,X3)),X4)) ),
inference(resolution,[status(thm)],[f171,f152]) ).
fof(f282,plain,
! [X0,X1,X2,X3,X4] :
( check_cpq(triple(X0,X1,X4))
| ~ check_cpq(triple(X0,insert_slb(X1,pair(X2,X3)),X4)) ),
inference(backward_subsumption_resolution,[status(thm)],[f104,f281]) ).
fof(f284,plain,
! [X0,X1,X2,X3,X4] : pair_in_list(insert_slb(insert_slb(X0,pair(X1,X2)),pair(X3,X4)),X1,X2),
inference(resolution,[status(thm)],[f72,f171]) ).
fof(f285,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ contains_slb(X2,X1)
| remove_slb(insert_slb(insert_slb(X2,pair(X3,X4)),pair(X0,X5)),X1) = insert_slb(remove_slb(insert_slb(X2,pair(X3,X4)),X1),pair(X0,X5))
| X0 = X1 ),
inference(resolution,[status(thm)],[f77,f65]) ).
fof(f287,plain,
! [X0,X1] :
( remove_slb(insert_slb(sK3_skl,pair(X0,X1)),sK5_skl) = insert_slb(remove_slb(sK3_skl,sK5_skl),pair(X0,X1))
| X0 = sK5_skl ),
inference(resolution,[status(thm)],[f77,f174]) ).
fof(f289,plain,
! [X0] :
( sK3_skl = insert_slb(remove_slb(sK3_skl,sK5_skl),pair(sK5_skl,X0))
| sK5_skl = sK5_skl ),
inference(paramodulation,[status(thm)],[f74,f287]) ).
fof(f291,definition,
( sQ16_spl
<=> sK5_skl = sK5_skl ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f294,definition,
! [X0] :
( sQ17_spl
<=> sK3_skl = insert_slb(remove_slb(sK3_skl,sK5_skl),pair(sK5_skl,X0)) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f297,plain,
( sQ17_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f289,f291,f294]) ).
fof(f300,plain,
! [X0,X1,X2,X3] :
( ~ check_cpq(triple(X1,X2,X3))
| less_than(X0,X0) ),
inference(resolution,[status(thm)],[f281,f256]) ).
fof(f310,plain,
! [X0,X1,X2,X3] :
( ~ check_cpq(triple(X1,X2,X3))
| less_than(bottom,X0) ),
inference(resolution,[status(thm)],[f281,f176]) ).
fof(f311,plain,
! [X0,X1,X2,X3,X4] :
( ~ check_cpq(triple(X2,X3,X4))
| less_than(X1,X0)
| less_than(X0,X1) ),
inference(resolution,[status(thm)],[f281,f179]) ).
fof(f312,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ check_cpq(triple(X3,X4,X5))
| ~ less_than(X2,X1)
| ~ less_than(X0,X2)
| less_than(X0,X1) ),
inference(resolution,[status(thm)],[f281,f177]) ).
fof(f313,definition,
! [X0] :
( sQ18_spl
<=> less_than(X0,X0) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f316,definition,
! [X1,X2,X3] :
( sQ19_spl
<=> ~ check_cpq(triple(X1,X2,X3)) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f317,plain,
! [X0,X1,X2] :
( ~ sQ19_spl
| ~ check_cpq(triple(X0,X1,X2)) ),
inference(component_clause,[status(thm)],[f316]) ).
fof(f319,plain,
( sQ19_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f300,f313,f316]) ).
fof(f321,definition,
! [X1,X2,X3] :
( sQ20_spl
<=> ( ~ less_than(X2,X3)
| ~ less_than(X1,X2) ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f322,plain,
! [X0,X1,X2] :
( ~ sQ20_spl
| ~ less_than(X1,X2)
| ~ less_than(X0,X1) ),
inference(component_clause,[status(thm)],[f321]) ).
fof(f325,definition,
! [X1,X2] :
( sQ21_spl
<=> less_than(X1,X2) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f326,plain,
! [X0,X1] :
( ~ sQ21_spl
| less_than(X0,X1) ),
inference(component_clause,[status(thm)],[f325]) ).
fof(f332,definition,
! [X0] :
( sQ22_spl
<=> less_than(bottom,X0) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f335,plain,
( sQ19_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f310,f332,f316]) ).
fof(f336,definition,
! [X0,X1] :
( sQ23_spl
<=> ( less_than(X1,X0)
| less_than(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f339,plain,
( sQ19_spl
| sQ23_spl ),
inference(split_clause,[status(thm)],[f311,f336,f316]) ).
fof(f340,definition,
! [X0,X1,X2] :
( sQ24_spl
<=> ( ~ less_than(X2,X1)
| ~ less_than(X0,X2)
| less_than(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f343,plain,
( sQ19_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f312,f340,f316]) ).
fof(f344,plain,
( ~ sQ19_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f226,f317]) ).
fof(f352,plain,
~ sQ19_spl,
inference(contradiction_clause,[status(thm)],[f344]) ).
fof(f355,plain,
! [X0,X1,X2,X3,X4] :
( less_than(X0,X1)
| ~ check_cpq(triple(X2,X3,X4))
| ~ less_than(X0,X1) ),
inference(resolution,[status(thm)],[f105,f281]) ).
fof(f356,definition,
! [X0,X1] :
( sQ25_spl
<=> ( less_than(X0,X1)
| ~ less_than(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f359,plain,
( sQ19_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f355,f356,f316]) ).
fof(f370,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ contains_slb(X2,X1)
| lookup_slb(insert_slb(insert_slb(X2,pair(X3,X4)),pair(X0,X5)),X1) = lookup_slb(insert_slb(X2,pair(X3,X4)),X1)
| X0 = X1 ),
inference(resolution,[status(thm)],[f81,f65]) ).
fof(f372,plain,
! [X0,X1] :
( lookup_slb(insert_slb(sK3_skl,pair(X0,X1)),sK5_skl) = lookup_slb(sK3_skl,sK5_skl)
| X0 = sK5_skl ),
inference(resolution,[status(thm)],[f81,f174]) ).
fof(f380,plain,
! [X0,X1,X2,X3,X4] :
( ~ less_than(X4,X2)
| ~ less_than(X3,X4)
| update_slb(insert_slb(X0,pair(X1,X2)),X3) = insert_slb(update_slb(X0,X3),pair(X1,X2)) ),
inference(resolution,[status(thm)],[f88,f50]) ).
fof(f382,plain,
! [X0] :
( X0 = lookup_slb(sK3_skl,sK5_skl)
| sK5_skl = sK5_skl ),
inference(paramodulation,[status(thm)],[f78,f372]) ).
fof(f384,definition,
! [X0] :
( sQ27_spl
<=> X0 = lookup_slb(sK3_skl,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f387,plain,
( sQ27_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f382,f291,f384]) ).
fof(f397,plain,
! [X0,X1,X2,X3,X4] :
( check_cpq(triple(X2,X3,X4))
| ~ check_cpq(triple(X2,X3,X4))
| less_than(X0,X1) ),
inference(resolution,[status(thm)],[f179,f282]) ).
fof(f399,plain,
( sQ3_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f397,f325,f202]) ).
fof(f432,plain,
pair_in_list(sK3_skl,sK0_skl(sK3_skl),sK1_skl(sK3_skl)),
inference(resolution,[status(thm)],[f153,f168]) ).
fof(f438,plain,
! [X0,X1,X2,X3,X4] :
( less_than(sK1_skl(X1),sK0_skl(X1))
| ~ check_cpq(triple(X3,X1,X4))
| check_cpq(triple(X0,X1,X2)) ),
inference(resolution,[status(thm)],[f153,f152]) ).
fof(f441,plain,
! [X0,X1,X2,X3,X4] :
( ~ check_cpq(triple(X3,X1,X4))
| check_cpq(triple(X0,X1,X2)) ),
inference(forward_subsumption_resolution,[status(thm)],[f438,f154]) ).
fof(f466,plain,
! [X0,X1,X2,X3,X4,X5] :
( lookup_slb(insert_slb(X1,pair(X4,X5)),X3) = lookup_slb(X1,X3)
| X4 = X3
| remove_cpq(triple(X0,X1,X2),X3) = triple(X0,X1,bad) ),
inference(resolution,[status(thm)],[f125,f81]) ).
fof(f467,plain,
! [X0,X1,X2,X3,X4,X5] :
( remove_slb(insert_slb(X1,pair(X4,X5)),X3) = insert_slb(remove_slb(X1,X3),pair(X4,X5))
| X4 = X3
| remove_cpq(triple(X0,X1,X2),X3) = triple(X0,X1,bad) ),
inference(resolution,[status(thm)],[f125,f77]) ).
fof(f470,plain,
! [X0,X1,X2,X3,X4] :
( remove_cpq(triple(X3,insert_slb(X0,pair(X1,X2)),X4),X1) = triple(remove_pqp(X3,X1),remove_slb(insert_slb(X0,pair(X1,X2)),X1),X4)
| ~ less_than(lookup_slb(insert_slb(X0,pair(X1,X2)),X1),X1) ),
inference(resolution,[status(thm)],[f128,f170]) ).
fof(f471,plain,
! [X0,X1] :
( remove_cpq(triple(X0,sK3_skl,X1),sK5_skl) = triple(remove_pqp(X0,sK5_skl),remove_slb(sK3_skl,sK5_skl),X1)
| ~ less_than(lookup_slb(sK3_skl,sK5_skl),sK5_skl) ),
inference(resolution,[status(thm)],[f128,f174]) ).
fof(f473,plain,
! [X0,X1,X2,X3,X4] :
( remove_cpq(triple(X2,insert_slb(X3,pair(X1,X0)),X4),X1) = triple(remove_pqp(X2,X1),remove_slb(insert_slb(X3,pair(X1,X0)),X1),X4)
| ~ less_than(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f78,f470]) ).
fof(f474,plain,
! [X0,X1,X2,X3,X4] :
( remove_cpq(triple(X2,insert_slb(X3,pair(X1,X0)),X4),X1) = triple(remove_pqp(X2,X1),X3,X4)
| ~ less_than(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f74,f473]) ).
fof(f475,definition,
( sQ30_spl
<=> less_than(lookup_slb(sK3_skl,sK5_skl),sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f478,definition,
! [X0,X1] :
( sQ31_spl
<=> remove_cpq(triple(X0,sK3_skl,X1),sK5_skl) = triple(remove_pqp(X0,sK5_skl),remove_slb(sK3_skl,sK5_skl),X1) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f479,plain,
! [X0,X1] :
( ~ sQ31_spl
| remove_cpq(triple(X0,sK3_skl,X1),sK5_skl) = triple(remove_pqp(X0,sK5_skl),remove_slb(sK3_skl,sK5_skl),X1) ),
inference(component_clause,[status(thm)],[f478]) ).
fof(f481,plain,
( sQ31_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f471,f475,f478]) ).
fof(f486,plain,
! [X0,X1] :
( less_than(sK1_skl(sK3_skl),sK0_skl(sK3_skl))
| ~ check_cpq(triple(X0,sK3_skl,X1)) ),
inference(resolution,[status(thm)],[f432,f152]) ).
fof(f487,plain,
! [X0,X1] : pair_in_list(insert_slb(sK3_skl,pair(X0,X1)),sK0_skl(sK3_skl),sK1_skl(sK3_skl)),
inference(resolution,[status(thm)],[f432,f72]) ).
fof(f488,plain,
! [X0,X1] :
( less_than(sK1_skl(sK3_skl),sK0_skl(sK3_skl))
| ~ ok(remove_cpq(triple(X0,sK3_skl,X1),sK0_skl(sK3_skl)))
| ~ check_cpq(remove_cpq(triple(X0,sK3_skl,X1),sK0_skl(sK3_skl))) ),
inference(resolution,[status(thm)],[f432,f159]) ).
fof(f489,definition,
! [X0,X1] :
( sQ32_spl
<=> ~ check_cpq(triple(X0,sK3_skl,X1)) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f490,plain,
! [X0,X1] :
( ~ sQ32_spl
| ~ check_cpq(triple(X0,sK3_skl,X1)) ),
inference(component_clause,[status(thm)],[f489]) ).
fof(f492,definition,
( sQ33_spl
<=> less_than(sK1_skl(sK3_skl),sK0_skl(sK3_skl)) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f493,plain,
( ~ sQ33_spl
| less_than(sK1_skl(sK3_skl),sK0_skl(sK3_skl)) ),
inference(component_clause,[status(thm)],[f492]) ).
fof(f494,plain,
( sQ33_spl
| ~ less_than(sK1_skl(sK3_skl),sK0_skl(sK3_skl)) ),
inference(component_clause,[status(thm)],[f492]) ).
fof(f495,plain,
( sQ33_spl
| sQ32_spl ),
inference(split_clause,[status(thm)],[f486,f489,f492]) ).
fof(f496,definition,
! [X0,X1] :
( sQ34_spl
<=> ( ~ ok(remove_cpq(triple(X0,sK3_skl,X1),sK0_skl(sK3_skl)))
| ~ check_cpq(remove_cpq(triple(X0,sK3_skl,X1),sK0_skl(sK3_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f497,plain,
! [X0,X1] :
( ~ sQ34_spl
| ~ ok(remove_cpq(triple(X0,sK3_skl,X1),sK0_skl(sK3_skl)))
| ~ check_cpq(remove_cpq(triple(X0,sK3_skl,X1),sK0_skl(sK3_skl))) ),
inference(component_clause,[status(thm)],[f496]) ).
fof(f499,plain,
( sQ33_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f488,f496,f492]) ).
fof(f500,plain,
! [X0,X1] :
( ~ sQ33_spl
| check_cpq(triple(X0,sK3_skl,X1)) ),
inference(resolution,[status(thm)],[f493,f154]) ).
fof(f502,plain,
( ~ sQ33_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f168,f500]) ).
fof(f503,plain,
~ sQ33_spl,
inference(contradiction_clause,[status(thm)],[f502]) ).
fof(f508,plain,
! [X0] :
( sQ33_spl
| ~ less_than(X0,sK0_skl(sK3_skl))
| ~ less_than(sK1_skl(sK3_skl),X0) ),
inference(resolution,[status(thm)],[f494,f50]) ).
fof(f532,plain,
! [X0] :
( sQ33_spl
| less_than(X0,sK1_skl(sK3_skl))
| ~ less_than(X0,sK0_skl(sK3_skl)) ),
inference(resolution,[status(thm)],[f508,f51]) ).
fof(f535,plain,
! [X0,X1] :
( sQ33_spl
| ~ less_than(X1,X0)
| ~ less_than(sK1_skl(sK3_skl),X1)
| ~ less_than(X0,sK0_skl(sK3_skl)) ),
inference(resolution,[status(thm)],[f508,f50]) ).
fof(f542,definition,
( sQ35_spl
<=> less_than(sK1_skl(sK3_skl),sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f544,plain,
( sQ35_spl
| ~ less_than(sK1_skl(sK3_skl),sK5_skl) ),
inference(component_clause,[status(thm)],[f542]) ).
fof(f554,plain,
( sQ33_spl
| ~ sQ21_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f494,f326]) ).
fof(f591,plain,
! [X0] :
( X0 = sK0_skl(sK3_skl)
| pair_in_list(sK3_skl,sK0_skl(sK3_skl),sK1_skl(sK3_skl)) ),
inference(resolution,[status(thm)],[f487,f70]) ).
fof(f593,definition,
( sQ40_spl
<=> pair_in_list(sK3_skl,sK0_skl(sK3_skl),sK1_skl(sK3_skl)) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f600,definition,
! [X0] :
( sQ42_spl
<=> X0 = sK0_skl(sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f601,plain,
! [X0] :
( ~ sQ42_spl
| X0 = sK0_skl(sK3_skl) ),
inference(component_clause,[status(thm)],[f600]) ).
fof(f603,plain,
( sQ42_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f591,f593,f600]) ).
fof(f608,plain,
! [X0,X1,X2] :
( ~ sQ42_spl
| pair_in_list(sK3_skl,X2,sK1_skl(sK3_skl))
| check_cpq(triple(X0,sK3_skl,X1)) ),
inference(paramodulation,[status(thm)],[f601,f153]) ).
fof(f609,definition,
! [X0,X1] :
( sQ43_spl
<=> check_cpq(triple(X0,sK3_skl,X1)) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f610,plain,
! [X0,X1] :
( ~ sQ43_spl
| check_cpq(triple(X0,sK3_skl,X1)) ),
inference(component_clause,[status(thm)],[f609]) ).
fof(f612,definition,
! [X2] :
( sQ44_spl
<=> pair_in_list(sK3_skl,X2,sK1_skl(sK3_skl)) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f613,plain,
! [X0] :
( ~ sQ44_spl
| pair_in_list(sK3_skl,X0,sK1_skl(sK3_skl)) ),
inference(component_clause,[status(thm)],[f612]) ).
fof(f615,plain,
( ~ sQ42_spl
| sQ44_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f608,f609,f612,f600]) ).
fof(f616,plain,
( ~ sQ43_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f610,f490]) ).
fof(f617,plain,
( ~ sQ43_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f616]) ).
fof(f630,definition,
! [X2] :
( sQ46_spl
<=> less_than(sK1_skl(sK3_skl),X2) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f631,plain,
! [X0] :
( ~ sQ46_spl
| less_than(sK1_skl(sK3_skl),X0) ),
inference(component_clause,[status(thm)],[f630]) ).
fof(f635,plain,
( sQ33_spl
| ~ sQ46_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f494,f631]) ).
fof(f704,definition,
! [X2] :
( sQ47_spl
<=> less_than(X2,sK0_skl(sK3_skl)) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f705,plain,
! [X0] :
( ~ sQ47_spl
| less_than(X0,sK0_skl(sK3_skl)) ),
inference(component_clause,[status(thm)],[f704]) ).
fof(f736,definition,
! [X0,X1,X2,X3] :
( sQ48_spl
<=> ~ check_cpq(triple(X0,insert_slb(sK3_skl,pair(X1,X2)),X3)) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f740,plain,
( sQ35_spl
| less_than(sK5_skl,sK1_skl(sK3_skl)) ),
inference(resolution,[status(thm)],[f544,f51]) ).
fof(f750,plain,
( sQ33_spl
| ~ sQ46_spl ),
inference(contradiction_clause,[status(thm)],[f635]) ).
fof(f753,plain,
( sQ33_spl
| ~ sQ47_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f494,f705]) ).
fof(f798,plain,
! [X0,X1] :
( ~ sQ6_spl
| ~ sQ20_spl
| ~ less_than(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f218,f322]) ).
fof(f799,plain,
( sQ35_spl
| ~ sQ6_spl
| ~ sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f740,f798]) ).
fof(f800,plain,
( sQ35_spl
| ~ sQ6_spl
| ~ sQ20_spl ),
inference(contradiction_clause,[status(thm)],[f799]) ).
fof(f801,plain,
( sQ33_spl
| ~ sQ47_spl ),
inference(contradiction_clause,[status(thm)],[f753]) ).
fof(f834,plain,
( ~ sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f206,f58]) ).
fof(f835,plain,
~ sQ4_spl,
inference(contradiction_clause,[status(thm)],[f834]) ).
fof(f861,plain,
! [X0] :
( less_than(X0,sK5_skl)
| ~ pair_in_list(sK3_skl,sK5_skl,X0)
| ~ check_cpq(remove_cpq(triple(sK2_skl,sK3_skl,sK4_skl),sK5_skl)) ),
inference(resolution,[status(thm)],[f159,f167]) ).
fof(f862,definition,
( sQ49_spl
<=> check_cpq(remove_cpq(triple(sK2_skl,sK3_skl,sK4_skl),sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f864,plain,
( sQ49_spl
| ~ check_cpq(remove_cpq(triple(sK2_skl,sK3_skl,sK4_skl),sK5_skl)) ),
inference(component_clause,[status(thm)],[f862]) ).
fof(f865,definition,
! [X0] :
( sQ50_spl
<=> ( less_than(X0,sK5_skl)
| ~ pair_in_list(sK3_skl,sK5_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f866,plain,
! [X0] :
( ~ sQ50_spl
| less_than(X0,sK5_skl)
| ~ pair_in_list(sK3_skl,sK5_skl,X0) ),
inference(component_clause,[status(thm)],[f865]) ).
fof(f868,plain,
( sQ50_spl
| ~ sQ49_spl ),
inference(split_clause,[status(thm)],[f861,f862,f865]) ).
fof(f869,plain,
( sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f864,f166]) ).
fof(f870,plain,
sQ49_spl,
inference(contradiction_clause,[status(thm)],[f869]) ).
fof(f903,plain,
( ~ sQ50_spl
| ~ sQ44_spl
| less_than(sK1_skl(sK3_skl),sK5_skl) ),
inference(resolution,[status(thm)],[f613,f866]) ).
fof(f906,plain,
( ~ sQ50_spl
| ~ sQ44_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f903,f542,f612,f865]) ).
fof(f921,plain,
! [X0] :
( sQ35_spl
| ~ less_than(X0,sK5_skl)
| ~ less_than(sK1_skl(sK3_skl),X0) ),
inference(resolution,[status(thm)],[f50,f544]) ).
fof(f926,plain,
! [X0,X1] :
( sQ35_spl
| ~ less_than(X1,X0)
| ~ less_than(sK1_skl(sK3_skl),X1)
| ~ less_than(X0,sK5_skl) ),
inference(resolution,[status(thm)],[f921,f50]) ).
fof(f977,plain,
! [X0] :
( sQ35_spl
| ~ less_than(X0,bottom)
| ~ less_than(sK1_skl(sK3_skl),X0) ),
inference(resolution,[status(thm)],[f926,f58]) ).
fof(f980,plain,
! [X0,X1] :
( sQ35_spl
| less_than(sK5_skl,X1)
| ~ less_than(X0,X1)
| ~ less_than(sK1_skl(sK3_skl),X0) ),
inference(resolution,[status(thm)],[f926,f51]) ).
fof(f985,plain,
! [X0,X1] :
( sQ35_spl
| ~ less_than(X1,bottom)
| ~ less_than(X0,X1)
| ~ less_than(sK1_skl(sK3_skl),X0) ),
inference(resolution,[status(thm)],[f977,f50]) ).
fof(f1002,plain,
! [X0,X1,X2,X3] :
( ~ sQ31_spl
| ~ check_cpq(triple(X2,remove_slb(sK3_skl,sK5_skl),X3))
| check_cpq(remove_cpq(triple(X0,sK3_skl,X1),sK5_skl)) ),
inference(paramodulation,[status(thm)],[f479,f441]) ).
fof(f1008,definition,
! [X0,X1] :
( sQ51_spl
<=> check_cpq(remove_cpq(triple(X0,sK3_skl,X1),sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f1009,plain,
! [X0,X1] :
( ~ sQ51_spl
| check_cpq(remove_cpq(triple(X0,sK3_skl,X1),sK5_skl)) ),
inference(component_clause,[status(thm)],[f1008]) ).
fof(f1015,definition,
( sQ53_spl
<=> remove_slb(sK3_skl,sK5_skl) = create_slb ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f1016,plain,
( ~ sQ53_spl
| remove_slb(sK3_skl,sK5_skl) = create_slb ),
inference(component_clause,[status(thm)],[f1015]) ).
fof(f1030,definition,
! [X2,X3] :
( sQ57_spl
<=> ~ check_cpq(triple(X2,remove_slb(sK3_skl,sK5_skl),X3)) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f1031,plain,
! [X0,X1] :
( ~ sQ57_spl
| ~ check_cpq(triple(X0,remove_slb(sK3_skl,sK5_skl),X1)) ),
inference(component_clause,[status(thm)],[f1030]) ).
fof(f1033,plain,
( ~ sQ31_spl
| sQ57_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f1002,f1008,f1030,f478]) ).
fof(f1043,plain,
! [X0,X1] :
( ~ sQ53_spl
| remove_slb(insert_slb(sK3_skl,pair(X0,X1)),sK5_skl) = insert_slb(create_slb,pair(X0,X1))
| X0 = sK5_skl ),
inference(backward_demodulation,[status(thm)],[f1016,f287]) ).
fof(f1107,plain,
! [X0,X1,X2,X3] :
( less_than(sK1_skl(sK3_skl),sK0_skl(sK3_skl))
| ~ check_cpq(triple(X0,insert_slb(sK3_skl,pair(X1,X2)),X3)) ),
inference(resolution,[status(thm)],[f487,f152]) ).
fof(f1109,plain,
( sQ33_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f1107,f736,f492]) ).
fof(f1211,plain,
! [X0,X1,X2,X3] :
( less_than(lookup_slb(X0,X1),X1)
| remove_cpq(triple(X2,X0,X3),X1) = triple(remove_pqp(X2,X1),remove_slb(X0,X1),bad)
| ~ contains_slb(X0,X1) ),
inference(resolution,[status(thm)],[f131,f169]) ).
fof(f1225,plain,
! [X0,X1] :
( sQ35_spl
| ~ less_than(X1,sK5_skl)
| ~ less_than(sK1_skl(sK3_skl),X1)
| ~ less_than(X0,sK5_skl)
| ~ less_than(sK1_skl(sK3_skl),X0) ),
inference(resolution,[status(thm)],[f980,f926]) ).
fof(f1227,definition,
! [X0] :
( sQ63_spl
<=> ( ~ less_than(X0,bottom)
| ~ less_than(sK1_skl(sK3_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f1231,definition,
! [X0] :
( sQ64_spl
<=> ( ~ less_than(X0,sK5_skl)
| ~ less_than(sK1_skl(sK3_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f1232,plain,
! [X0] :
( ~ sQ64_spl
| ~ less_than(X0,sK5_skl)
| ~ less_than(sK1_skl(sK3_skl),X0) ),
inference(component_clause,[status(thm)],[f1231]) ).
fof(f1234,plain,
( sQ35_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f1225,f1231,f542]) ).
fof(f1239,plain,
! [X0,X1] :
( sQ35_spl
| less_than(X0,sK1_skl(sK3_skl))
| ~ less_than(X1,bottom)
| ~ less_than(X0,X1) ),
inference(resolution,[status(thm)],[f985,f51]) ).
fof(f1300,plain,
! [X0,X1] :
( sQ35_spl
| ~ less_than(X1,bottom)
| ~ less_than(sK1_skl(sK3_skl),X1)
| ~ less_than(X0,bottom)
| ~ less_than(sK1_skl(sK3_skl),X0) ),
inference(resolution,[status(thm)],[f1239,f985]) ).
fof(f1304,plain,
( sQ35_spl
| sQ63_spl ),
inference(split_clause,[status(thm)],[f1300,f1227,f542]) ).
fof(f1377,plain,
! [X0] :
( ~ sQ53_spl
| sK3_skl = insert_slb(create_slb,pair(sK5_skl,X0))
| sK5_skl = sK5_skl ),
inference(paramodulation,[status(thm)],[f74,f1043]) ).
fof(f1379,definition,
! [X0] :
( sQ72_spl
<=> sK3_skl = insert_slb(create_slb,pair(sK5_skl,X0)) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f1382,plain,
( ~ sQ53_spl
| sQ72_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f1377,f291,f1379,f1015]) ).
fof(f1438,definition,
( sQ75_spl
<=> less_than(sK1_skl(sK3_skl),bottom) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f1465,plain,
! [X0,X1] :
( X0 = sK5_skl
| pair_in_list(remove_slb(sK3_skl,sK5_skl),X0,X1)
| ~ pair_in_list(sK3_skl,X0,X1) ),
inference(resolution,[status(thm)],[f156,f174]) ).
fof(f1469,plain,
! [X0,X1] :
( ~ sQ53_spl
| X0 = sK5_skl
| pair_in_list(create_slb,X0,X1)
| ~ pair_in_list(sK3_skl,X0,X1) ),
inference(forward_demodulation,[status(thm)],[f1016,f1465]) ).
fof(f1470,plain,
! [X0,X1] :
( ~ sQ53_spl
| X0 = sK5_skl
| ~ pair_in_list(sK3_skl,X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1469,f67]) ).
fof(f1476,plain,
! [X0,X1] :
( ~ sQ53_spl
| check_cpq(triple(X0,sK3_skl,X1))
| sK0_skl(sK3_skl) = sK5_skl ),
inference(resolution,[status(thm)],[f1470,f153]) ).
fof(f1490,definition,
( sQ76_spl
<=> sK0_skl(sK3_skl) = sK5_skl ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f1491,plain,
( ~ sQ76_spl
| sK0_skl(sK3_skl) = sK5_skl ),
inference(component_clause,[status(thm)],[f1490]) ).
fof(f1493,plain,
( ~ sQ53_spl
| sQ43_spl
| sQ76_spl ),
inference(split_clause,[status(thm)],[f1476,f1490,f609,f1015]) ).
fof(f1569,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( less_than(X3,X2)
| ~ check_cpq(triple(X0,insert_slb(insert_slb(X1,pair(X2,X3)),pair(X4,X5)),X6)) ),
inference(resolution,[status(thm)],[f284,f152]) ).
fof(f1605,definition,
( sQ79_spl
<=> less_than(sK5_skl,sK1_skl(sK3_skl)) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1704,plain,
! [X0] :
( sQ33_spl
| ~ less_than(X0,bottom)
| ~ less_than(sK1_skl(sK3_skl),X0) ),
inference(resolution,[status(thm)],[f535,f58]) ).
fof(f1707,plain,
! [X0,X1] :
( sQ33_spl
| less_than(sK0_skl(sK3_skl),X1)
| ~ less_than(X0,X1)
| ~ less_than(sK1_skl(sK3_skl),X0) ),
inference(resolution,[status(thm)],[f535,f51]) ).
fof(f1727,plain,
! [X0,X1,X2,X3] :
( less_than(X1,X0)
| ~ check_cpq(triple(X2,remove_slb(sK3_skl,sK5_skl),X3))
| X0 = sK5_skl
| ~ pair_in_list(sK3_skl,X0,X1) ),
inference(resolution,[status(thm)],[f1465,f152]) ).
fof(f1729,definition,
! [X0,X1] :
( sQ86_spl
<=> ( less_than(X1,X0)
| X0 = sK5_skl
| ~ pair_in_list(sK3_skl,X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f1730,plain,
! [X0,X1] :
( ~ sQ86_spl
| less_than(X1,X0)
| X0 = sK5_skl
| ~ pair_in_list(sK3_skl,X0,X1) ),
inference(component_clause,[status(thm)],[f1729]) ).
fof(f1732,plain,
( sQ57_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f1727,f1729,f1030]) ).
fof(f1783,plain,
! [X0] :
( sQ33_spl
| less_than(X0,sK1_skl(sK3_skl))
| ~ less_than(X0,bottom) ),
inference(resolution,[status(thm)],[f1704,f51]) ).
fof(f1832,plain,
( sQ33_spl
| ~ less_than(sK1_skl(sK3_skl),bottom)
| ~ less_than(sK1_skl(sK3_skl),bottom) ),
inference(resolution,[status(thm)],[f1783,f1704]) ).
fof(f1836,plain,
( sQ33_spl
| ~ sQ75_spl ),
inference(split_clause,[status(thm)],[f1832,f1438,f492]) ).
fof(f1841,plain,
! [X0] :
( ~ sQ64_spl
| less_than(sK5_skl,X0)
| ~ less_than(sK1_skl(sK3_skl),X0) ),
inference(resolution,[status(thm)],[f1232,f51]) ).
fof(f1856,plain,
! [X0] :
( ~ sQ64_spl
| less_than(X0,sK1_skl(sK3_skl))
| less_than(sK5_skl,X0) ),
inference(resolution,[status(thm)],[f1841,f51]) ).
fof(f1888,plain,
( ~ sQ64_spl
| less_than(sK5_skl,sK1_skl(sK3_skl))
| less_than(sK5_skl,sK1_skl(sK3_skl)) ),
inference(resolution,[status(thm)],[f1856,f1841]) ).
fof(f1894,plain,
( ~ sQ64_spl
| sQ79_spl ),
inference(split_clause,[status(thm)],[f1888,f1605,f1231]) ).
fof(f1898,plain,
! [X0,X1] :
( ~ sQ86_spl
| check_cpq(triple(X0,sK3_skl,X1))
| less_than(sK1_skl(sK3_skl),sK0_skl(sK3_skl))
| sK0_skl(sK3_skl) = sK5_skl ),
inference(resolution,[status(thm)],[f1730,f153]) ).
fof(f1900,plain,
( ~ sQ86_spl
| sQ43_spl
| sQ33_spl
| sQ76_spl ),
inference(split_clause,[status(thm)],[f1898,f1490,f492,f609,f1729]) ).
fof(f1903,plain,
! [X0,X1] :
( ~ sQ34_spl
| ~ sQ76_spl
| ~ ok(remove_cpq(triple(X0,sK3_skl,X1),sK5_skl))
| ~ check_cpq(remove_cpq(triple(X0,sK3_skl,X1),sK0_skl(sK3_skl))) ),
inference(backward_demodulation,[status(thm)],[f1491,f497]) ).
fof(f1907,plain,
( sQ33_spl
| ~ sQ76_spl
| ~ less_than(sK1_skl(sK3_skl),sK5_skl) ),
inference(backward_demodulation,[status(thm)],[f1491,f494]) ).
fof(f1918,plain,
! [X0,X1] :
( ~ sQ34_spl
| ~ sQ76_spl
| ~ ok(remove_cpq(triple(X0,sK3_skl,X1),sK5_skl))
| ~ check_cpq(remove_cpq(triple(X0,sK3_skl,X1),sK5_skl)) ),
inference(forward_demodulation,[status(thm)],[f1491,f1903]) ).
fof(f1971,plain,
( sQ33_spl
| ~ sQ76_spl
| ~ sQ35_spl ),
inference(split_clause,[status(thm)],[f1907,f542,f1490,f492]) ).
fof(f2000,plain,
( ~ sQ34_spl
| ~ sQ76_spl
| ~ sQ51_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f167,f2002]) ).
fof(f2002,plain,
! [X0,X1] :
( ~ sQ34_spl
| ~ sQ76_spl
| ~ sQ51_spl
| ~ ok(remove_cpq(triple(X0,sK3_skl,X1),sK5_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1918,f1009]) ).
fof(f2021,plain,
( ~ sQ34_spl
| ~ sQ76_spl
| ~ sQ51_spl ),
inference(contradiction_clause,[status(thm)],[f2000]) ).
fof(f2090,plain,
! [X0,X1] :
( remove_slb(insert_slb(sK3_skl,pair(X0,X1)),sK5_skl) = insert_slb(remove_slb(sK3_skl,sK5_skl),pair(X0,X1))
| X0 = sK5_skl
| check_cpq(triple(sK2_skl,sK3_skl,bad)) ),
inference(paramodulation,[status(thm)],[f467,f166]) ).
fof(f2110,definition,
! [X0,X1] :
( sQ91_spl
<=> ( remove_slb(insert_slb(sK3_skl,pair(X0,X1)),sK5_skl) = insert_slb(remove_slb(sK3_skl,sK5_skl),pair(X0,X1))
| X0 = sK5_skl ) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f2114,definition,
( sQ92_spl
<=> check_cpq(triple(sK2_skl,sK3_skl,bad)) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f2115,plain,
( ~ sQ92_spl
| check_cpq(triple(sK2_skl,sK3_skl,bad)) ),
inference(component_clause,[status(thm)],[f2114]) ).
fof(f2117,plain,
( sQ91_spl
| sQ92_spl ),
inference(split_clause,[status(thm)],[f2090,f2114,f2110]) ).
fof(f2125,plain,
! [X0,X1] :
( lookup_slb(insert_slb(sK3_skl,pair(X0,X1)),sK5_skl) = lookup_slb(sK3_skl,sK5_skl)
| X0 = sK5_skl
| check_cpq(triple(sK2_skl,sK3_skl,bad)) ),
inference(paramodulation,[status(thm)],[f466,f166]) ).
fof(f2140,definition,
! [X0,X1] :
( sQ94_spl
<=> ( lookup_slb(insert_slb(sK3_skl,pair(X0,X1)),sK5_skl) = lookup_slb(sK3_skl,sK5_skl)
| X0 = sK5_skl ) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f2144,plain,
( sQ94_spl
| sQ92_spl ),
inference(split_clause,[status(thm)],[f2125,f2114,f2140]) ).
fof(f2148,plain,
( ~ sQ92_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2115,f490]) ).
fof(f2149,plain,
( ~ sQ92_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f2148]) ).
fof(f2202,definition,
( sQ99_spl
<=> less_than(sK0_skl(sK3_skl),sK1_skl(sK3_skl)) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f2270,definition,
( sQ100_spl
<=> less_than(sK5_skl,sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f2272,plain,
( sQ100_spl
| ~ less_than(sK5_skl,sK5_skl) ),
inference(component_clause,[status(thm)],[f2270]) ).
fof(f2359,plain,
! [X0] :
( sQ33_spl
| less_than(sK0_skl(sK3_skl),X0)
| ~ less_than(sK1_skl(sK3_skl),X0) ),
inference(resolution,[status(thm)],[f508,f51]) ).
fof(f2382,plain,
! [X0] :
( sQ33_spl
| less_than(sK0_skl(sK3_skl),X0)
| less_than(X0,sK1_skl(sK3_skl)) ),
inference(resolution,[status(thm)],[f532,f51]) ).
fof(f2451,plain,
( sQ33_spl
| less_than(sK0_skl(sK3_skl),sK1_skl(sK3_skl))
| less_than(sK0_skl(sK3_skl),sK1_skl(sK3_skl)) ),
inference(resolution,[status(thm)],[f2382,f2359]) ).
fof(f2472,plain,
( sQ33_spl
| sQ99_spl ),
inference(split_clause,[status(thm)],[f2451,f2202,f492]) ).
fof(f2550,plain,
! [X0,X1,X2,X3] :
( lookup_slb(insert_slb(insert_slb(sK3_skl,pair(X1,X2)),pair(X0,X3)),sK5_skl) = lookup_slb(insert_slb(sK3_skl,pair(X1,X2)),sK5_skl)
| X0 = sK5_skl ),
inference(resolution,[status(thm)],[f370,f174]) ).
fof(f2594,plain,
! [X0,X1,X2] :
( X0 = lookup_slb(insert_slb(sK3_skl,pair(X1,X2)),sK5_skl)
| sK5_skl = sK5_skl ),
inference(paramodulation,[status(thm)],[f78,f2550]) ).
fof(f2606,definition,
! [X0,X1,X2] :
( sQ110_spl
<=> X0 = lookup_slb(insert_slb(sK3_skl,pair(X1,X2)),sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f2609,plain,
( sQ110_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f2594,f291,f2606]) ).
fof(f2673,definition,
! [X0] :
( sQ112_spl
<=> ( less_than(X0,sK1_skl(sK3_skl))
| less_than(sK0_skl(sK3_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f3016,plain,
( sQ100_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2272,f52]) ).
fof(f3017,plain,
sQ100_spl,
inference(contradiction_clause,[status(thm)],[f3016]) ).
fof(f3116,plain,
! [X0,X1,X2,X3] :
( remove_slb(insert_slb(insert_slb(sK3_skl,pair(X1,X2)),pair(X0,X3)),sK5_skl) = insert_slb(remove_slb(insert_slb(sK3_skl,pair(X1,X2)),sK5_skl),pair(X0,X3))
| X0 = sK5_skl ),
inference(resolution,[status(thm)],[f285,f174]) ).
fof(f3213,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ check_cpq(triple(X4,insert_slb(X5,pair(X1,X0)),X6))
| less_than(X2,X3)
| less_than(X0,X1) ),
inference(resolution,[status(thm)],[f1569,f179]) ).
fof(f3231,definition,
! [X0,X1,X5,X6,X7] :
( sQ153_spl
<=> ( ~ check_cpq(triple(X5,insert_slb(X6,pair(X1,X0)),X7))
| less_than(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f3235,plain,
( sQ21_spl
| sQ153_spl ),
inference(split_clause,[status(thm)],[f3213,f3231,f325]) ).
fof(f3273,plain,
! [X0,X1] :
( sQ33_spl
| less_than(X0,sK1_skl(sK3_skl))
| less_than(sK0_skl(sK3_skl),X1)
| ~ less_than(X0,X1) ),
inference(resolution,[status(thm)],[f1707,f51]) ).
fof(f3640,plain,
( sQ33_spl
| ~ sQ21_spl ),
inference(contradiction_clause,[status(thm)],[f554]) ).
fof(f4212,plain,
! [X0,X1] :
( sQ33_spl
| less_than(X0,X1)
| less_than(X1,sK1_skl(sK3_skl))
| less_than(sK0_skl(sK3_skl),X0) ),
inference(resolution,[status(thm)],[f3273,f51]) ).
fof(f4257,plain,
! [X0,X1,X2] :
( insert_slb(sK3_skl,pair(X0,X1)) = insert_slb(remove_slb(insert_slb(sK3_skl,pair(X0,X1)),sK5_skl),pair(sK5_skl,X2))
| sK5_skl = sK5_skl ),
inference(paramodulation,[status(thm)],[f74,f3116]) ).
fof(f4260,definition,
! [X0,X1,X2] :
( sQ195_spl
<=> insert_slb(sK3_skl,pair(X0,X1)) = insert_slb(remove_slb(insert_slb(sK3_skl,pair(X0,X1)),sK5_skl),pair(sK5_skl,X2)) ),
introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition]) ).
fof(f4263,plain,
( sQ195_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f4257,f291,f4260]) ).
fof(f4440,plain,
! [X0,X1,X2] :
( sQ33_spl
| ~ less_than(X2,sK0_skl(sK3_skl))
| update_slb(insert_slb(X0,pair(X1,sK1_skl(sK3_skl))),X2) = insert_slb(update_slb(X0,X2),pair(X1,sK1_skl(sK3_skl)))
| less_than(sK1_skl(sK3_skl),sK0_skl(sK3_skl)) ),
inference(resolution,[status(thm)],[f4212,f380]) ).
fof(f4442,plain,
! [X0,X1,X2] :
( sQ33_spl
| remove_cpq(triple(X0,insert_slb(X1,pair(sK1_skl(sK3_skl),sK0_skl(sK3_skl))),X2),sK1_skl(sK3_skl)) = triple(remove_pqp(X0,sK1_skl(sK3_skl)),X1,X2)
| less_than(sK1_skl(sK3_skl),sK0_skl(sK3_skl)) ),
inference(resolution,[status(thm)],[f4212,f474]) ).
fof(f4444,plain,
! [X0,X1] :
( sQ33_spl
| update_slb(insert_slb(X0,pair(X1,sK1_skl(sK3_skl))),sK0_skl(sK3_skl)) = insert_slb(update_slb(X0,sK0_skl(sK3_skl)),pair(X1,sK1_skl(sK3_skl)))
| less_than(sK1_skl(sK3_skl),sK0_skl(sK3_skl)) ),
inference(resolution,[status(thm)],[f4212,f88]) ).
fof(f4502,plain,
! [X0,X1] :
( sQ33_spl
| less_than(X0,sK1_skl(sK3_skl))
| less_than(sK0_skl(sK3_skl),X1)
| less_than(X1,sK1_skl(sK3_skl))
| less_than(sK0_skl(sK3_skl),X0) ),
inference(resolution,[status(thm)],[f4212,f3273]) ).
fof(f4526,definition,
! [X0,X1,X2] :
( sQ202_spl
<=> ( ~ less_than(X2,sK0_skl(sK3_skl))
| update_slb(insert_slb(X0,pair(X1,sK1_skl(sK3_skl))),X2) = insert_slb(update_slb(X0,X2),pair(X1,sK1_skl(sK3_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition]) ).
fof(f4529,plain,
( sQ202_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f4440,f492,f4526]) ).
fof(f4530,definition,
! [X0,X1,X2] :
( sQ203_spl
<=> remove_cpq(triple(X0,insert_slb(X1,pair(sK1_skl(sK3_skl),sK0_skl(sK3_skl))),X2),sK1_skl(sK3_skl)) = triple(remove_pqp(X0,sK1_skl(sK3_skl)),X1,X2) ),
introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition]) ).
fof(f4533,plain,
( sQ203_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f4442,f492,f4530]) ).
fof(f4534,definition,
! [X0,X1] :
( sQ204_spl
<=> update_slb(insert_slb(X0,pair(X1,sK1_skl(sK3_skl))),sK0_skl(sK3_skl)) = insert_slb(update_slb(X0,sK0_skl(sK3_skl)),pair(X1,sK1_skl(sK3_skl))) ),
introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition]) ).
fof(f4537,plain,
( sQ204_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f4444,f492,f4534]) ).
fof(f4600,plain,
( sQ33_spl
| sQ112_spl ),
inference(split_clause,[status(thm)],[f4502,f2673,f492]) ).
fof(f4669,plain,
! [X0,X1] :
( ~ sQ31_spl
| ~ sQ57_spl
| ~ check_cpq(remove_cpq(triple(X0,sK3_skl,X1),sK5_skl)) ),
inference(paramodulation,[status(thm)],[f479,f1031]) ).
fof(f4787,plain,
( ~ sQ31_spl
| ~ sQ57_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f166,f4669]) ).
fof(f4788,plain,
( ~ sQ31_spl
| ~ sQ57_spl ),
inference(contradiction_clause,[status(thm)],[f4787]) ).
fof(f5033,plain,
! [X0,X1] :
( less_than(lookup_slb(sK3_skl,sK5_skl),sK5_skl)
| remove_cpq(triple(X0,sK3_skl,X1),sK5_skl) = triple(remove_pqp(X0,sK5_skl),remove_slb(sK3_skl,sK5_skl),bad) ),
inference(resolution,[status(thm)],[f1211,f174]) ).
fof(f5040,definition,
! [X0,X1] :
( sQ230_spl
<=> remove_cpq(triple(X0,sK3_skl,X1),sK5_skl) = triple(remove_pqp(X0,sK5_skl),remove_slb(sK3_skl,sK5_skl),bad) ),
introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition]) ).
fof(f5041,plain,
! [X0,X1] :
( ~ sQ230_spl
| remove_cpq(triple(X0,sK3_skl,X1),sK5_skl) = triple(remove_pqp(X0,sK5_skl),remove_slb(sK3_skl,sK5_skl),bad) ),
inference(component_clause,[status(thm)],[f5040]) ).
fof(f5043,plain,
( sQ30_spl
| sQ230_spl ),
inference(split_clause,[status(thm)],[f5033,f5040,f475]) ).
fof(f5166,plain,
! [X0,X1] :
( ~ sQ230_spl
| ~ sQ57_spl
| ~ check_cpq(remove_cpq(triple(X0,sK3_skl,X1),sK5_skl)) ),
inference(paramodulation,[status(thm)],[f5041,f1031]) ).
fof(f5207,plain,
! [X0,X1,X2,X3] :
( ~ sQ230_spl
| ~ check_cpq(triple(X2,remove_slb(sK3_skl,sK5_skl),X3))
| check_cpq(remove_cpq(triple(X0,sK3_skl,X1),sK5_skl)) ),
inference(paramodulation,[status(thm)],[f5041,f441]) ).
fof(f5228,plain,
( ~ sQ230_spl
| ~ sQ57_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f166,f5166]) ).
fof(f5274,plain,
( ~ sQ230_spl
| sQ57_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f5207,f1008,f1030,f5040]) ).
fof(f5277,plain,
( ~ sQ230_spl
| ~ sQ57_spl ),
inference(contradiction_clause,[status(thm)],[f5228]) ).
fof(f5278,plain,
$false,
inference(sat_refutation,[status(thm)],[f191,f193,f199,f230,f236,f242,f248,f254,f260,f266,f272,f278,f297,f319,f335,f339,f343,f352,f359,f387,f399,f481,f495,f499,f503,f603,f615,f617,f750,f800,f801,f835,f868,f870,f906,f1033,f1109,f1234,f1304,f1382,f1493,f1732,f1836,f1894,f1900,f1971,f2021,f2117,f2144,f2149,f2472,f2609,f3017,f3235,f3640,f4263,f4529,f4533,f4537,f4600,f4788,f5043,f5274,f5277]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV391+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n016.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 08:49:23 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 10.26/1.78 % Refutation found
% 10.26/1.78 % SZS status Theorem for theBenchmark: Theorem is valid
% 10.26/1.78 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.58/1.81 % Elapsed time: 1.434266 seconds
% 1.58/1.81 % CPU time: 11.045152 seconds
% 1.58/1.81 % Total memory used: 194.602 MB
% 1.58/1.81 % Net memory used: 175.803 MB
%------------------------------------------------------------------------------