%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV398+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 : n020.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 97.92s 12.87s
% Output : CNFRefutation 97.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 30
% Syntax : Number of formulae : 166 ( 23 unt; 14 def)
% Number of atoms : 450 ( 58 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 494 ( 210 ~; 218 |; 34 &)
% ( 22 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 22 ( 19 usr; 16 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 6 con; 0-3 aty)
% Number of variables : 448 ( 435 !; 13 ?)
% 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(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(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(f26,axiom,
! [U,V,W,X,Y] :
( strictly_less_than(X,Y)
=> ( check_cpq(triple(U,insert_slb(V,pair(X,Y)),W))
<=> $false ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,axiom,
! [U,V,W,X] :
( ( ~ contains_slb(V,findmin_pqp_res(U))
& V != create_slb )
=> findmin_cpq_eff(triple(U,V,W)) = triple(U,update_slb(V,findmin_pqp_res(U)),bad) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [U,V,W,X] :
( ( strictly_less_than(findmin_pqp_res(U),lookup_slb(V,findmin_pqp_res(U)))
& contains_slb(V,findmin_pqp_res(U))
& V != create_slb )
=> findmin_cpq_eff(triple(U,V,W)) = triple(U,update_slb(V,findmin_pqp_res(U)),bad) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [U,V,W,X] :
( ( less_than(lookup_slb(V,findmin_pqp_res(U)),findmin_pqp_res(U))
& contains_slb(V,findmin_pqp_res(U))
& V != create_slb )
=> findmin_cpq_eff(triple(U,V,W)) = triple(U,update_slb(V,findmin_pqp_res(U)),W) ),
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] :
( strictly_less_than(V,W)
& pair_in_list(U,V,W) )
=> ! [X] :
? [Y,Z] :
( strictly_less_than(Y,Z)
& pair_in_list(update_slb(U,X),Y,Z) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,conjecture,
! [U,V,W] :
( ~ check_cpq(triple(U,V,W))
=> ~ check_cpq(findmin_cpq_eff(triple(U,V,W))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,negated_conjecture,
~ ! [U,V,W] :
( ~ check_cpq(triple(U,V,W))
=> ~ check_cpq(findmin_cpq_eff(triple(U,V,W))) ),
inference(negated_conjecture,[status(cth)],[f44]) ).
fof(f46,plain,
! [U,V,W] :
( less_than(U,W)
| ~ less_than(V,W)
| ~ less_than(U,V) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f47,plain,
! [U,W] :
( less_than(U,W)
| ! [V] :
( ~ less_than(V,W)
| ~ less_than(U,V) ) ),
inference(miniscoping,[status(thm)],[f46]) ).
fof(f48,plain,
! [X0,X1,X2] :
( less_than(X0,X2)
| ~ less_than(X1,X2)
| ~ less_than(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f49,plain,
! [X0,X1] :
( less_than(X1,X0)
| less_than(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f50,plain,
! [X0] : less_than(X0,X0),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f51,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(f52,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)],[f51]) ).
fof(f53,plain,
! [X0,X1] :
( ~ strictly_less_than(X0,X1)
| less_than(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f55,plain,
! [X0,X1] :
( ~ less_than(X0,X1)
| less_than(X1,X0)
| strictly_less_than(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f56,plain,
! [X0] : less_than(bottom,X0),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f65,plain,
! [X0,X1] : ~ pair_in_list(create_slb,X0,X1),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f66,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(f67,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)],[f66]) ).
fof(f70,plain,
! [X0,X1,X2,X3,X4] :
( pair_in_list(insert_slb(X0,pair(X3,X4)),X1,X2)
| ~ pair_in_list(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f71,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)],[f67]) ).
fof(f98,plain,
! [X0,X1] : check_cpq(triple(X0,create_slb,X1)),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f99,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(f100,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)],[f99]) ).
fof(f101,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)],[f100]) ).
fof(f102,plain,
! [X0,X1,X2,X3,X4] :
( ~ check_cpq(triple(X0,insert_slb(X1,pair(X4,X3)),X2))
| ~ less_than(X3,X4)
| check_cpq(triple(X0,X1,X2)) ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f103,plain,
! [X0,X1,X2,X3,X4] :
( ~ check_cpq(triple(X0,X1,X4))
| ~ less_than(X3,X2)
| check_cpq(triple(X0,insert_slb(X1,pair(X2,X3)),X4)) ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f104,plain,
! [U,V,W,X,Y] :
( ( check_cpq(triple(U,insert_slb(V,pair(X,Y)),W))
<=> $false )
| ~ strictly_less_than(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f105,plain,
! [U,V,W,X,Y] :
( ( ( $true
| check_cpq(triple(U,insert_slb(V,pair(X,Y)),W)) )
& ( $false
| ~ check_cpq(triple(U,insert_slb(V,pair(X,Y)),W)) ) )
| ~ strictly_less_than(X,Y) ),
inference(NNF_transformation,[status(thm)],[f104]) ).
fof(f106,plain,
! [X,Y] :
( ( ( $true
| ! [U,V,W] : check_cpq(triple(U,insert_slb(V,pair(X,Y)),W)) )
& ( $false
| ! [U,V,W] : ~ check_cpq(triple(U,insert_slb(V,pair(X,Y)),W)) ) )
| ~ strictly_less_than(X,Y) ),
inference(miniscoping,[status(thm)],[f105]) ).
fof(f107,plain,
! [X,Y] :
( ! [U,V,W] : ~ check_cpq(triple(U,insert_slb(V,pair(X,Y)),W))
| ~ strictly_less_than(X,Y) ),
inference(true_and_false_simplification,[status(thm)],[f106]) ).
fof(f108,plain,
! [X0,X1,X2,X3,X4] :
( ~ check_cpq(triple(X2,insert_slb(X3,pair(X0,X1)),X4))
| ~ strictly_less_than(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f107]) ).
fof(f131,plain,
! [U,V,W,X] :
( findmin_cpq_eff(triple(U,V,W)) = triple(U,update_slb(V,findmin_pqp_res(U)),bad)
| contains_slb(V,findmin_pqp_res(U))
| V = create_slb ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f132,plain,
! [U,V] :
( ! [W] : findmin_cpq_eff(triple(U,V,W)) = triple(U,update_slb(V,findmin_pqp_res(U)),bad)
| contains_slb(V,findmin_pqp_res(U))
| V = create_slb ),
inference(miniscoping,[status(thm)],[f131]) ).
fof(f133,plain,
! [X0,X1,X2] :
( contains_slb(X0,findmin_pqp_res(X1))
| triple(X1,update_slb(X0,findmin_pqp_res(X1)),bad) = findmin_cpq_eff(triple(X1,X0,X2))
| X0 = create_slb ),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f134,plain,
! [U,V,W,X] :
( findmin_cpq_eff(triple(U,V,W)) = triple(U,update_slb(V,findmin_pqp_res(U)),bad)
| ~ strictly_less_than(findmin_pqp_res(U),lookup_slb(V,findmin_pqp_res(U)))
| ~ contains_slb(V,findmin_pqp_res(U))
| V = create_slb ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f135,plain,
! [U,V] :
( ! [W] : findmin_cpq_eff(triple(U,V,W)) = triple(U,update_slb(V,findmin_pqp_res(U)),bad)
| ~ strictly_less_than(findmin_pqp_res(U),lookup_slb(V,findmin_pqp_res(U)))
| ~ contains_slb(V,findmin_pqp_res(U))
| V = create_slb ),
inference(miniscoping,[status(thm)],[f134]) ).
fof(f136,plain,
! [X0,X1,X2] :
( findmin_cpq_eff(triple(X1,X0,X2)) = triple(X1,update_slb(X0,findmin_pqp_res(X1)),bad)
| ~ contains_slb(X0,findmin_pqp_res(X1))
| ~ strictly_less_than(findmin_pqp_res(X1),lookup_slb(X0,findmin_pqp_res(X1)))
| create_slb = X0 ),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f137,plain,
! [U,V,W,X] :
( findmin_cpq_eff(triple(U,V,W)) = triple(U,update_slb(V,findmin_pqp_res(U)),W)
| ~ less_than(lookup_slb(V,findmin_pqp_res(U)),findmin_pqp_res(U))
| ~ contains_slb(V,findmin_pqp_res(U))
| V = create_slb ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f138,plain,
! [U,V] :
( ! [W] : findmin_cpq_eff(triple(U,V,W)) = triple(U,update_slb(V,findmin_pqp_res(U)),W)
| ~ less_than(lookup_slb(V,findmin_pqp_res(U)),findmin_pqp_res(U))
| ~ contains_slb(V,findmin_pqp_res(U))
| V = create_slb ),
inference(miniscoping,[status(thm)],[f137]) ).
fof(f139,plain,
! [X0,X1,X2] :
( X0 = create_slb
| ~ contains_slb(X0,findmin_pqp_res(X1))
| findmin_cpq_eff(triple(X1,X0,X2)) = triple(X1,update_slb(X0,findmin_pqp_res(X1)),X2)
| ~ less_than(lookup_slb(X0,findmin_pqp_res(X1)),findmin_pqp_res(X1)) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f146,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(f147,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)],[f146]) ).
fof(f148,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)],[f147]) ).
fof(f149,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))],[f148]) ).
fof(f150,plain,
! [X0,X1,X2,X3,X4] :
( ~ pair_in_list(X3,X1,X0)
| ~ check_cpq(triple(X2,X3,X4))
| less_than(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f151,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)],[f149]) ).
fof(f152,plain,
! [X0,X1,X2] :
( check_cpq(triple(X1,X0,X2))
| ~ less_than(sK1_skl(X0),sK0_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f153,plain,
! [U] :
( ! [X] :
? [Y,Z] :
( strictly_less_than(Y,Z)
& pair_in_list(update_slb(U,X),Y,Z) )
| ! [V,W] :
( ~ strictly_less_than(V,W)
| ~ pair_in_list(U,V,W) ) ),
inference(pre_NNF_transformation,[status(thm)],[f43]) ).
fof(f154,plain,
! [U] :
( ! [X] :
( strictly_less_than(sK2_skl(X,U),sK3_skl(X,U))
& pair_in_list(update_slb(U,X),sK2_skl(X,U),sK3_skl(X,U)) )
| ! [V,W] :
( ~ strictly_less_than(V,W)
| ~ pair_in_list(U,V,W) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(Y,sK2_skl(X,U)),skolemize(Z,sK3_skl(X,U))],[f153]) ).
fof(f155,plain,
! [X0,X1,X2,X3] :
( ~ strictly_less_than(X1,X2)
| pair_in_list(update_slb(X0,X3),sK2_skl(X3,X0),sK3_skl(X3,X0))
| ~ pair_in_list(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f156,plain,
! [X0,X1,X2,X3] :
( ~ strictly_less_than(X2,X3)
| ~ pair_in_list(X1,X2,X3)
| strictly_less_than(sK2_skl(X0,X1),sK3_skl(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f157,plain,
? [U,V,W] :
( check_cpq(findmin_cpq_eff(triple(U,V,W)))
& ~ check_cpq(triple(U,V,W)) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f158,plain,
( check_cpq(findmin_cpq_eff(triple(sK4_skl,sK5_skl,sK6_skl)))
& ~ check_cpq(triple(sK4_skl,sK5_skl,sK6_skl)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl]),skolemize(U,sK4_skl),skolemize(V,sK5_skl),skolemize(W,sK6_skl)],[f157]) ).
fof(f159,plain,
~ check_cpq(triple(sK4_skl,sK5_skl,sK6_skl)),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f160,plain,
check_cpq(findmin_cpq_eff(triple(sK4_skl,sK5_skl,sK6_skl))),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f162,plain,
! [X0,X1,X2] : pair_in_list(insert_slb(X0,pair(X1,X2)),X1,X2),
inference(destructive_equality_resolution,[status(thm)],[f71]) ).
fof(f165,plain,
! [X0,X1,X2,X3] :
( ~ less_than(lookup_slb(X0,findmin_pqp_res(X1)),findmin_pqp_res(X1))
| create_slb = X0
| findmin_cpq_eff(triple(X1,X0,X3)) = triple(X1,update_slb(X0,findmin_pqp_res(X1)),X3)
| findmin_cpq_eff(triple(X1,X0,X2)) = triple(X1,update_slb(X0,findmin_pqp_res(X1)),bad)
| create_slb = X0 ),
inference(resolution,[status(thm)],[f133,f139]) ).
fof(f166,plain,
! [X0,X1,X2,X3] :
( findmin_cpq_eff(triple(X0,X1,X3)) = triple(X0,update_slb(X1,findmin_pqp_res(X0)),X3)
| ~ less_than(lookup_slb(X1,findmin_pqp_res(X0)),findmin_pqp_res(X0))
| X1 = create_slb
| findmin_cpq_eff(triple(X0,X1,X2)) = triple(X0,update_slb(X1,findmin_pqp_res(X0)),bad) ),
inference(duplicate_literals_removal,[status(thm)],[f165]) ).
fof(f174,plain,
! [X0,X1,X2] :
( ~ strictly_less_than(findmin_pqp_res(X1),lookup_slb(X0,findmin_pqp_res(X1)))
| triple(X1,update_slb(X0,findmin_pqp_res(X1)),bad) = findmin_cpq_eff(triple(X1,X0,X2))
| create_slb = X0 ),
inference(forward_subsumption_resolution,[status(thm)],[f136,f133]) ).
fof(f176,plain,
! [X0,X1,X2,X3] :
( check_cpq(triple(X2,insert_slb(create_slb,pair(X1,X0)),X3))
| ~ less_than(X0,X1) ),
inference(resolution,[status(thm)],[f103,f98]) ).
fof(f205,plain,
! [X0,X1,X2] : check_cpq(triple(X0,insert_slb(create_slb,pair(X1,X1)),X2)),
inference(resolution,[status(thm)],[f176,f50]) ).
fof(f230,plain,
! [X0,X1,X2] : check_cpq(triple(X0,insert_slb(create_slb,pair(X1,bottom)),X2)),
inference(resolution,[status(thm)],[f56,f176]) ).
fof(f266,plain,
! [X0,X1,X2,X3,X4] :
( check_cpq(triple(X3,X1,X4))
| less_than(sK1_skl(X1),sK0_skl(X1))
| ~ check_cpq(triple(X0,X1,X2)) ),
inference(resolution,[status(thm)],[f151,f150]) ).
fof(f333,plain,
! [X0,X1,X2,X3,X4] :
( ~ check_cpq(triple(X2,insert_slb(X3,pair(X1,X0)),X4))
| less_than(X0,X1) ),
inference(resolution,[status(thm)],[f162,f150]) ).
fof(f340,plain,
! [X0,X1] :
( less_than(X1,X0)
| strictly_less_than(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f55,f49]) ).
fof(f341,plain,
! [X0,X1,X2] :
( X0 = create_slb
| findmin_cpq_eff(triple(X1,X0,X2)) = triple(X1,update_slb(X0,findmin_pqp_res(X1)),bad)
| less_than(lookup_slb(X0,findmin_pqp_res(X1)),findmin_pqp_res(X1)) ),
inference(resolution,[status(thm)],[f340,f174]) ).
fof(f351,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)],[f102,f333]) ).
fof(f370,plain,
! [X0,X1,X2,X3] :
( X1 = create_slb
| findmin_cpq_eff(triple(X0,X1,X3)) = triple(X0,update_slb(X1,findmin_pqp_res(X0)),X3)
| findmin_cpq_eff(triple(X0,X1,X2)) = triple(X0,update_slb(X1,findmin_pqp_res(X0)),bad) ),
inference(backward_subsumption_resolution,[status(thm)],[f166,f341]) ).
fof(f386,definition,
! [X0,X1] :
( sQ10_spl
<=> ~ less_than(X0,X1) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f387,plain,
! [X0,X1] :
( ~ sQ10_spl
| ~ less_than(X0,X1) ),
inference(component_clause,[status(thm)],[f386]) ).
fof(f404,plain,
! [X0,X1,X2,X3,X4,X5] :
( findmin_cpq_eff(triple(X0,X1,X5)) = triple(X0,update_slb(X1,findmin_pqp_res(X0)),bad)
| ~ less_than(X3,X2)
| ~ check_cpq(findmin_cpq_eff(triple(X0,X1,X4)))
| create_slb = X1
| check_cpq(triple(X0,insert_slb(update_slb(X1,findmin_pqp_res(X0)),pair(X2,X3)),X4)) ),
inference(paramodulation,[status(thm)],[f370,f103]) ).
fof(f424,plain,
( ~ sQ10_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f50,f387]) ).
fof(f425,plain,
~ sQ10_spl,
inference(contradiction_clause,[status(thm)],[f424]) ).
fof(f426,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ pair_in_list(X6,X2,X3)
| ~ check_cpq(triple(X5,X6,X7))
| ~ check_cpq(triple(X0,X1,X4))
| check_cpq(triple(X0,insert_slb(X1,pair(X2,X3)),X4)) ),
inference(resolution,[status(thm)],[f150,f103]) ).
fof(f449,plain,
! [X0,X1] :
( ~ less_than(X1,X0)
| ~ strictly_less_than(X0,X1) ),
inference(resolution,[status(thm)],[f176,f108]) ).
fof(f474,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7] :
( ~ strictly_less_than(X3,X4)
| ~ check_cpq(triple(X5,X6,X7))
| ~ pair_in_list(X1,X3,X4)
| ~ check_cpq(triple(X0,X1,X2)) ),
inference(resolution,[status(thm)],[f426,f108]) ).
fof(f475,definition,
! [X0,X1,X2,X3,X4] :
( sQ14_spl
<=> ( ~ strictly_less_than(X3,X4)
| ~ pair_in_list(X1,X3,X4)
| ~ check_cpq(triple(X0,X1,X2)) ) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f476,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ14_spl
| ~ strictly_less_than(X3,X4)
| ~ pair_in_list(X1,X3,X4)
| ~ check_cpq(triple(X0,X1,X2)) ),
inference(component_clause,[status(thm)],[f475]) ).
fof(f478,definition,
! [X5,X6,X7] :
( sQ15_spl
<=> ~ check_cpq(triple(X5,X6,X7)) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f479,plain,
! [X0,X1,X2] :
( ~ sQ15_spl
| ~ check_cpq(triple(X0,X1,X2)) ),
inference(component_clause,[status(thm)],[f478]) ).
fof(f481,plain,
( sQ15_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f474,f475,f478]) ).
fof(f526,plain,
( ~ sQ15_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f230,f479]) ).
fof(f532,plain,
~ sQ15_spl,
inference(contradiction_clause,[status(thm)],[f526]) ).
fof(f545,plain,
! [X0,X1,X2] :
( check_cpq(triple(X1,X0,X2))
| strictly_less_than(sK0_skl(X0),sK1_skl(X0)) ),
inference(resolution,[status(thm)],[f152,f340]) ).
fof(f713,plain,
! [X0,X1,X2,X3,X4] :
( ~ check_cpq(triple(X3,X1,X4))
| check_cpq(triple(X0,X1,X2)) ),
inference(forward_subsumption_resolution,[status(thm)],[f266,f152]) ).
fof(f714,plain,
! [X0,X1] : ~ check_cpq(triple(X0,sK5_skl,X1)),
inference(resolution,[status(thm)],[f713,f159]) ).
fof(f715,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ check_cpq(triple(X3,insert_slb(X1,pair(X4,X5)),X6))
| check_cpq(triple(X0,X1,X2)) ),
inference(resolution,[status(thm)],[f713,f351]) ).
fof(f732,plain,
strictly_less_than(sK0_skl(sK5_skl),sK1_skl(sK5_skl)),
inference(resolution,[status(thm)],[f545,f714]) ).
fof(f767,plain,
! [X0,X1,X2] :
( ~ sQ14_spl
| ~ pair_in_list(X1,sK0_skl(sK5_skl),sK1_skl(sK5_skl))
| ~ check_cpq(triple(X0,X1,X2)) ),
inference(resolution,[status(thm)],[f732,f476]) ).
fof(f770,plain,
! [X0,X1] :
( ~ pair_in_list(X0,sK0_skl(sK5_skl),sK1_skl(sK5_skl))
| pair_in_list(update_slb(X0,X1),sK2_skl(X1,X0),sK3_skl(X1,X0)) ),
inference(resolution,[status(thm)],[f732,f155]) ).
fof(f771,plain,
~ less_than(sK1_skl(sK5_skl),sK0_skl(sK5_skl)),
inference(resolution,[status(thm)],[f732,f449]) ).
fof(f774,plain,
! [X0,X1] :
( ~ pair_in_list(X1,sK0_skl(sK5_skl),sK1_skl(sK5_skl))
| strictly_less_than(sK2_skl(X0,X1),sK3_skl(X0,X1)) ),
inference(resolution,[status(thm)],[f732,f156]) ).
fof(f780,plain,
! [X0] :
( ~ less_than(X0,sK0_skl(sK5_skl))
| ~ less_than(sK1_skl(sK5_skl),X0) ),
inference(resolution,[status(thm)],[f771,f48]) ).
fof(f811,plain,
! [X0] :
( strictly_less_than(X0,sK1_skl(sK5_skl))
| ~ less_than(X0,sK0_skl(sK5_skl)) ),
inference(resolution,[status(thm)],[f780,f340]) ).
fof(f812,plain,
! [X0] :
( less_than(X0,sK1_skl(sK5_skl))
| ~ less_than(X0,sK0_skl(sK5_skl)) ),
inference(resolution,[status(thm)],[f780,f49]) ).
fof(f813,plain,
! [X0,X1] :
( ~ less_than(X1,sK0_skl(sK5_skl))
| ~ less_than(sK1_skl(sK5_skl),X0)
| ~ less_than(X0,X1) ),
inference(resolution,[status(thm)],[f780,f48]) ).
fof(f903,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ14_spl
| ~ check_cpq(triple(X1,insert_slb(X0,pair(X2,X3)),X4))
| ~ pair_in_list(X0,sK0_skl(sK5_skl),sK1_skl(sK5_skl)) ),
inference(resolution,[status(thm)],[f767,f70]) ).
fof(f922,plain,
! [X0,X1] :
( ~ less_than(X1,sK0_skl(sK5_skl))
| strictly_less_than(X0,sK1_skl(sK5_skl))
| ~ less_than(X0,X1) ),
inference(resolution,[status(thm)],[f813,f340]) ).
fof(f956,plain,
! [X0] :
( strictly_less_than(X0,sK1_skl(sK5_skl))
| ~ less_than(X0,bottom) ),
inference(resolution,[status(thm)],[f922,f56]) ).
fof(f973,plain,
! [X0] :
( strictly_less_than(X0,sK1_skl(sK5_skl))
| strictly_less_than(bottom,X0) ),
inference(resolution,[status(thm)],[f956,f340]) ).
fof(f994,plain,
! [X0] :
( ~ less_than(sK1_skl(sK5_skl),X0)
| strictly_less_than(bottom,X0) ),
inference(resolution,[status(thm)],[f973,f449]) ).
fof(f995,plain,
! [X0] :
( less_than(X0,sK1_skl(sK5_skl))
| strictly_less_than(bottom,X0) ),
inference(resolution,[status(thm)],[f973,f53]) ).
fof(f1012,definition,
( sQ28_spl
<=> strictly_less_than(bottom,sK1_skl(sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f1021,plain,
! [X0,X1,X2] :
( check_cpq(triple(X1,sK5_skl,X2))
| strictly_less_than(sK2_skl(X0,sK5_skl),sK3_skl(X0,sK5_skl)) ),
inference(resolution,[status(thm)],[f774,f151]) ).
fof(f1022,definition,
! [X0] :
( sQ29_spl
<=> strictly_less_than(sK2_skl(X0,sK5_skl),sK3_skl(X0,sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f1023,plain,
! [X0] :
( ~ sQ29_spl
| strictly_less_than(sK2_skl(X0,sK5_skl),sK3_skl(X0,sK5_skl)) ),
inference(component_clause,[status(thm)],[f1022]) ).
fof(f1025,definition,
! [X1,X2] :
( sQ30_spl
<=> check_cpq(triple(X1,sK5_skl,X2)) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f1026,plain,
! [X0,X1] :
( ~ sQ30_spl
| check_cpq(triple(X0,sK5_skl,X1)) ),
inference(component_clause,[status(thm)],[f1025]) ).
fof(f1028,plain,
( sQ30_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f1021,f1022,f1025]) ).
fof(f1039,plain,
! [X0,X1,X2] :
( check_cpq(triple(X1,sK5_skl,X2))
| pair_in_list(update_slb(sK5_skl,X0),sK2_skl(X0,sK5_skl),sK3_skl(X0,sK5_skl)) ),
inference(resolution,[status(thm)],[f770,f151]) ).
fof(f1040,definition,
! [X0] :
( sQ31_spl
<=> pair_in_list(update_slb(sK5_skl,X0),sK2_skl(X0,sK5_skl),sK3_skl(X0,sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f1041,plain,
! [X0] :
( ~ sQ31_spl
| pair_in_list(update_slb(sK5_skl,X0),sK2_skl(X0,sK5_skl),sK3_skl(X0,sK5_skl)) ),
inference(component_clause,[status(thm)],[f1040]) ).
fof(f1043,plain,
( sQ30_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f1039,f1040,f1025]) ).
fof(f1044,plain,
( ~ sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1026,f714]) ).
fof(f1045,plain,
~ sQ30_spl,
inference(contradiction_clause,[status(thm)],[f1044]) ).
fof(f1053,plain,
( strictly_less_than(bottom,sK1_skl(sK5_skl))
| strictly_less_than(bottom,sK1_skl(sK5_skl)) ),
inference(resolution,[status(thm)],[f995,f994]) ).
fof(f1059,plain,
sQ28_spl,
inference(split_clause,[status(thm)],[f1053,f1012]) ).
fof(f1084,plain,
! [X0,X1,X2,X3] :
( ~ sQ14_spl
| ~ sQ29_spl
| ~ check_cpq(triple(X2,X0,X3))
| ~ pair_in_list(X0,sK2_skl(X1,sK5_skl),sK3_skl(X1,sK5_skl)) ),
inference(resolution,[status(thm)],[f1023,f476]) ).
fof(f1526,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ14_spl
| check_cpq(triple(X4,sK5_skl,X5))
| ~ check_cpq(triple(X0,insert_slb(sK5_skl,pair(X1,X2)),X3)) ),
inference(resolution,[status(thm)],[f903,f151]) ).
fof(f1527,definition,
! [X0,X1,X2,X3] :
( sQ41_spl
<=> ~ check_cpq(triple(X0,insert_slb(sK5_skl,pair(X1,X2)),X3)) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f1528,plain,
! [X0,X1,X2,X3] :
( ~ sQ41_spl
| ~ check_cpq(triple(X0,insert_slb(sK5_skl,pair(X1,X2)),X3)) ),
inference(component_clause,[status(thm)],[f1527]) ).
fof(f1530,plain,
( ~ sQ14_spl
| sQ30_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f1526,f1527,f1025,f475]) ).
fof(f2108,plain,
! [X0,X1,X2] :
( ~ sQ31_spl
| ~ sQ14_spl
| ~ sQ29_spl
| ~ check_cpq(triple(X0,update_slb(sK5_skl,X1),X2)) ),
inference(resolution,[status(thm)],[f1084,f1041]) ).
fof(f2116,definition,
( sQ48_spl
<=> sK5_skl = create_slb ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f2117,plain,
( ~ sQ48_spl
| create_slb = sK5_skl ),
inference(component_clause,[status(thm)],[f2116]) ).
fof(f2153,plain,
! [X0,X1,X2] :
( ~ sQ48_spl
| check_cpq(triple(X0,insert_slb(sK5_skl,pair(X1,X1)),X2)) ),
inference(backward_demodulation,[status(thm)],[f2117,f205]) ).
fof(f2168,plain,
( ~ sQ48_spl
| ~ sQ41_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2153,f1528]) ).
fof(f2169,plain,
( ~ sQ48_spl
| ~ sQ41_spl ),
inference(contradiction_clause,[status(thm)],[f2168]) ).
fof(f3514,definition,
( sQ64_spl
<=> pair_in_list(create_slb,sK0_skl(sK5_skl),sK1_skl(insert_slb(create_slb,pair(sK0_skl(sK5_skl),sK1_skl(sK5_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f3515,plain,
( ~ sQ64_spl
| pair_in_list(create_slb,sK0_skl(sK5_skl),sK1_skl(insert_slb(create_slb,pair(sK0_skl(sK5_skl),sK1_skl(sK5_skl))))) ),
inference(component_clause,[status(thm)],[f3514]) ).
fof(f3534,plain,
( ~ sQ64_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3515,f65]) ).
fof(f3535,plain,
~ sQ64_spl,
inference(contradiction_clause,[status(thm)],[f3534]) ).
fof(f3685,plain,
! [X0,X1,X2] :
( findmin_cpq_eff(triple(sK4_skl,sK5_skl,X2)) = triple(sK4_skl,update_slb(sK5_skl,findmin_pqp_res(sK4_skl)),bad)
| ~ less_than(X1,X0)
| create_slb = sK5_skl
| check_cpq(triple(sK4_skl,insert_slb(update_slb(sK5_skl,findmin_pqp_res(sK4_skl)),pair(X0,X1)),sK6_skl)) ),
inference(resolution,[status(thm)],[f404,f160]) ).
fof(f3697,definition,
! [X0,X1] :
( sQ70_spl
<=> ( ~ less_than(X1,X0)
| check_cpq(triple(sK4_skl,insert_slb(update_slb(sK5_skl,findmin_pqp_res(sK4_skl)),pair(X0,X1)),sK6_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f3698,plain,
! [X0,X1] :
( ~ sQ70_spl
| check_cpq(triple(sK4_skl,insert_slb(update_slb(sK5_skl,findmin_pqp_res(sK4_skl)),pair(X1,X0)),sK6_skl))
| ~ less_than(X0,X1) ),
inference(component_clause,[status(thm)],[f3697]) ).
fof(f3700,definition,
! [X2] :
( sQ71_spl
<=> findmin_cpq_eff(triple(sK4_skl,sK5_skl,X2)) = triple(sK4_skl,update_slb(sK5_skl,findmin_pqp_res(sK4_skl)),bad) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f3701,plain,
! [X0] :
( ~ sQ71_spl
| findmin_cpq_eff(triple(sK4_skl,sK5_skl,X0)) = triple(sK4_skl,update_slb(sK5_skl,findmin_pqp_res(sK4_skl)),bad) ),
inference(component_clause,[status(thm)],[f3700]) ).
fof(f3703,plain,
( sQ71_spl
| sQ48_spl
| sQ70_spl ),
inference(split_clause,[status(thm)],[f3685,f3697,f2116,f3700]) ).
fof(f3726,plain,
! [X0,X1,X2,X3] :
( ~ sQ70_spl
| check_cpq(triple(X2,update_slb(sK5_skl,findmin_pqp_res(sK4_skl)),X3))
| ~ less_than(X0,X1) ),
inference(resolution,[status(thm)],[f3698,f715]) ).
fof(f3735,definition,
! [X2,X3] :
( sQ72_spl
<=> check_cpq(triple(X2,update_slb(sK5_skl,findmin_pqp_res(sK4_skl)),X3)) ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f3736,plain,
! [X0,X1] :
( ~ sQ72_spl
| check_cpq(triple(X0,update_slb(sK5_skl,findmin_pqp_res(sK4_skl)),X1)) ),
inference(component_clause,[status(thm)],[f3735]) ).
fof(f3738,plain,
( ~ sQ70_spl
| sQ72_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f3726,f386,f3735,f3697]) ).
fof(f3739,plain,
( ~ sQ72_spl
| ~ sQ31_spl
| ~ sQ14_spl
| ~ sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3736,f2108]) ).
fof(f3740,plain,
( ~ sQ72_spl
| ~ sQ31_spl
| ~ sQ14_spl
| ~ sQ29_spl ),
inference(contradiction_clause,[status(thm)],[f3739]) ).
fof(f3938,plain,
! [X0] :
( less_than(X0,sK1_skl(sK5_skl))
| less_than(sK0_skl(sK5_skl),X0) ),
inference(resolution,[status(thm)],[f812,f49]) ).
fof(f3951,plain,
! [X0] :
( less_than(sK0_skl(sK5_skl),X0)
| strictly_less_than(X0,sK1_skl(sK5_skl)) ),
inference(resolution,[status(thm)],[f811,f49]) ).
fof(f3969,definition,
( sQ81_spl
<=> less_than(sK0_skl(sK5_skl),sK1_skl(sK5_skl)) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f4001,plain,
! [X0] :
( less_than(sK0_skl(sK5_skl),X0)
| ~ less_than(sK1_skl(sK5_skl),X0) ),
inference(resolution,[status(thm)],[f3951,f449]) ).
fof(f4014,plain,
( less_than(sK0_skl(sK5_skl),sK1_skl(sK5_skl))
| less_than(sK0_skl(sK5_skl),sK1_skl(sK5_skl)) ),
inference(resolution,[status(thm)],[f4001,f3938]) ).
fof(f4020,plain,
sQ81_spl,
inference(split_clause,[status(thm)],[f4014,f3969]) ).
fof(f4030,plain,
! [X0] :
( ~ sQ71_spl
| ~ sQ31_spl
| ~ sQ14_spl
| ~ sQ29_spl
| ~ check_cpq(findmin_cpq_eff(triple(sK4_skl,sK5_skl,X0))) ),
inference(paramodulation,[status(thm)],[f3701,f2108]) ).
fof(f4186,plain,
( ~ sQ71_spl
| ~ sQ31_spl
| ~ sQ14_spl
| ~ sQ29_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f160,f4030]) ).
fof(f4188,plain,
( ~ sQ71_spl
| ~ sQ31_spl
| ~ sQ14_spl
| ~ sQ29_spl ),
inference(contradiction_clause,[status(thm)],[f4186]) ).
fof(f4189,plain,
$false,
inference(sat_refutation,[status(thm)],[f425,f481,f532,f1028,f1043,f1045,f1059,f1530,f2169,f3535,f3703,f3738,f3740,f4020,f4188]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV398+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.40 % Computer : n020.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Mon Sep 21 08:45:47 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.18/0.43 % Drodi V4.1.1
% 97.92/12.87 % Refutation found
% 97.92/12.87 % SZS status Theorem for theBenchmark: Theorem is valid
% 97.92/12.87 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 92.77/14.06 % Elapsed time: 13.430228 seconds
% 92.77/14.06 % CPU time: 96.119393 seconds
% 92.77/14.06 % Total memory used: 415.271 MB
% 92.77/14.06 % Net memory used: 344.457 MB
%------------------------------------------------------------------------------