%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV406+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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 : Sun Sep 27 09:07:39 AM UTC 2026
% Result : Theorem 198.60s 29.37s
% Output : CNFRefutation 198.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 7
% Syntax : Number of formulae : 62 ( 16 unt; 0 def)
% Number of atoms : 164 ( 12 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 153 ( 51 ~; 69 |; 17 &)
% ( 8 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 8 con; 0-3 aty)
% Number of variables : 177 ( 37 sgn 65 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(totality,axiom,
! [U,V] :
( less_than(V,U)
| less_than(U,V) ),
file('theBenchmark.p',totality) ).
fof(stricly_smaller_definition,axiom,
! [U,V] :
( strictly_less_than(U,V)
<=> ( ~ less_than(V,U)
& less_than(U,V) ) ),
file('theBenchmark.p',stricly_smaller_definition) ).
fof(ax23,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('theBenchmark.p',ax23) ).
fof(ax36,axiom,
! [U,V] : check_cpq(triple(U,create_slb,V)),
file('theBenchmark.p',ax36) ).
fof(ax37,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('theBenchmark.p',ax37) ).
fof(ax38,axiom,
! [U,V,W,X,Y] :
( strictly_less_than(X,Y)
=> ( check_cpq(triple(U,insert_slb(V,pair(X,Y)),W))
<=> $false ) ),
file('theBenchmark.p',ax38) ).
fof(l42_co,conjecture,
! [U] :
( ! [V,W] :
( check_cpq(triple(V,U,W))
<=> ! [X,Y] :
( pair_in_list(U,X,Y)
=> less_than(Y,X) ) )
=> ! [Z,X1,X2,X3] :
( check_cpq(triple(Z,insert_slb(U,pair(X2,X3)),X1))
<=> ! [X4,X5] :
( pair_in_list(insert_slb(U,pair(X2,X3)),X4,X5)
=> less_than(X5,X4) ) ) ),
file('theBenchmark.p',l42_co) ).
fof(l42_co_neg,negated_conjecture,
~ ! [U] :
( ! [V,W] :
( check_cpq(triple(V,U,W))
<=> ! [X,Y] :
( pair_in_list(U,X,Y)
=> less_than(Y,X) ) )
=> ! [Z,X1,X2,X3] :
( check_cpq(triple(Z,insert_slb(U,pair(X2,X3)),X1))
<=> ! [X4,X5] :
( pair_in_list(insert_slb(U,pair(X2,X3)),X4,X5)
=> less_than(X5,X4) ) ) ),
inference(assume_negation,[status(cth)],[l42_co]) ).
cnf(c_43,plain,
( less_than(B,A)
| less_than(A,B) ),
inference(clausify,[status(thm)],[totality]) ).
cnf(c_47,plain,
( less_than(B,A)
| ~ less_than(A,B)
| strictly_less_than(A,B) ),
inference(clausify,[status(thm)],[stricly_smaller_definition]) ).
cnf(c_56,plain,
( D = B
| pair_in_list(A,D,E)
| ~ pair_in_list(insert_slb(A,pair(B,C)),D,E) ),
inference(clausify,[status(thm)],[ax23]) ).
cnf(c_57,plain,
( E = C
| pair_in_list(A,D,E)
| ~ pair_in_list(insert_slb(A,pair(B,C)),D,E) ),
inference(clausify,[status(thm)],[ax23]) ).
cnf(c_58,plain,
( ~ pair_in_list(A,D,E)
| pair_in_list(insert_slb(A,pair(B,C)),D,E) ),
inference(clausify,[status(thm)],[ax23]) ).
cnf(c_59,plain,
( E != C
| D != B
| pair_in_list(insert_slb(A,pair(B,C)),D,E) ),
inference(clausify,[status(thm)],[ax23]) ).
cnf(c_72,plain,
check_cpq(triple(A,create_slb,B)),
inference(clausify,[status(thm)],[ax36]) ).
cnf(c_73,plain,
( check_cpq(triple(C,D,E))
| ~ check_cpq(triple(C,insert_slb(D,pair(B,A)),E))
| ~ less_than(A,B) ),
inference(clausify,[status(thm)],[ax37]) ).
cnf(c_74,plain,
( ~ check_cpq(triple(C,D,E))
| check_cpq(triple(C,insert_slb(D,pair(B,A)),E))
| ~ less_than(A,B) ),
inference(clausify,[status(thm)],[ax37]) ).
cnf(c_75,plain,
( ~ check_cpq(triple(C,insert_slb(D,pair(A,B)),E))
| ~ strictly_less_than(A,B) ),
inference(clausify,[status(thm)],[ax38]) ).
fof(nnf_41,plain,
? [U] :
( ? [Z,X1,X2,X3] :
( ( ? [X4,X5] :
( ~ less_than(X5,X4)
& pair_in_list(insert_slb(U,pair(X2,X3)),X4,X5) )
| ~ check_cpq(triple(Z,insert_slb(U,pair(X2,X3)),X1)) )
& ( ! [X7,X8] :
( less_than(X8,X7)
| ~ pair_in_list(insert_slb(U,pair(X2,X3)),X7,X8) )
| check_cpq(triple(Z,insert_slb(U,pair(X2,X3)),X1)) ) )
& ! [V,W] :
( ( ? [X,Y] :
( ~ less_than(Y,X)
& pair_in_list(U,X,Y) )
| check_cpq(triple(V,U,W)) )
& ( ! [X0,X6] :
( less_than(X6,X0)
| ~ pair_in_list(U,X0,X6) )
| ~ check_cpq(triple(V,U,W)) ) ) ),
inference(fof_nnf,[status(thm)],[l42_co_neg]) ).
fof(sk_l42_co_neg_sk,plain,
( ( ( ~ less_than(sK8,sK7)
& pair_in_list(insert_slb(sK0,pair(sK4,sK5)),sK7,sK8) )
| ~ check_cpq(triple(sK3,insert_slb(sK0,pair(sK4,sK5)),sK6)) )
& ( ! [X7,X8] :
( less_than(X8,X7)
| ~ pair_in_list(insert_slb(sK0,pair(sK4,sK5)),X7,X8) )
| check_cpq(triple(sK3,insert_slb(sK0,pair(sK4,sK5)),sK6)) )
& ! [V,W] :
( ( ( ~ less_than(sK2(V,W),sK1(V,W))
& pair_in_list(sK0,sK1(V,W),sK2(V,W)) )
| check_cpq(triple(V,sK0,W)) )
& ( ! [X0,X6] :
( less_than(X6,X0)
| ~ pair_in_list(sK0,X0,X6) )
| ~ check_cpq(triple(V,sK0,W)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7,sK8]),skolemize(U,sK0),skolemize(X,sK1(V,W)),skolemize(Y,sK2(V,W)),skolemize(Z,sK3),skolemize(X1,sK6),skolemize(X2,sK4),skolemize(X3,sK5),skolemize(X4,sK7),skolemize(X5,sK8)],[nnf_41]) ).
fof(sk_l42_co_neg,plain,
( ( ~ less_than(sK8,sK7)
| ~ check_cpq(triple(sK3,insert_slb(sK0,pair(sK4,sK5)),sK6)) )
& ( pair_in_list(insert_slb(sK0,pair(sK4,sK5)),sK7,sK8)
| ~ check_cpq(triple(sK3,insert_slb(sK0,pair(sK4,sK5)),sK6)) )
& ! [VAR_0,VAR_1] :
( less_than(VAR_1,VAR_0)
| ~ pair_in_list(insert_slb(sK0,pair(sK4,sK5)),VAR_0,VAR_1)
| check_cpq(triple(sK3,insert_slb(sK0,pair(sK4,sK5)),sK6)) )
& ! [VAR_0,VAR_1] :
( ~ less_than(sK2(VAR_0,VAR_1),sK1(VAR_0,VAR_1))
| check_cpq(triple(VAR_0,sK0,VAR_1)) )
& ! [VAR_0,VAR_1] :
( pair_in_list(sK0,sK1(VAR_0,VAR_1),sK2(VAR_0,VAR_1))
| check_cpq(triple(VAR_0,sK0,VAR_1)) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( less_than(VAR_3,VAR_2)
| ~ pair_in_list(sK0,VAR_2,VAR_3)
| ~ check_cpq(triple(VAR_0,sK0,VAR_1)) ) ),
inference(cnf_transformation,[status(thm)],[sk_l42_co_neg_sk]) ).
cnf(c_97,negated_conjecture,
( less_than(D,C)
| ~ pair_in_list(sK0,C,D)
| ~ check_cpq(triple(A,sK0,B)) ),
inference(split_conjunct,[status(thm)],[sk_l42_co_neg]) ).
cnf(c_98,negated_conjecture,
( pair_in_list(sK0,sK1(A,B),sK2(A,B))
| check_cpq(triple(A,sK0,B)) ),
inference(split_conjunct,[status(thm)],[sk_l42_co_neg]) ).
cnf(c_99,negated_conjecture,
( ~ less_than(sK2(A,B),sK1(A,B))
| check_cpq(triple(A,sK0,B)) ),
inference(split_conjunct,[status(thm)],[sk_l42_co_neg]) ).
cnf(c_100,negated_conjecture,
( less_than(B,A)
| ~ pair_in_list(insert_slb(sK0,pair(sK4,sK5)),A,B)
| check_cpq(triple(sK3,insert_slb(sK0,pair(sK4,sK5)),sK6)) ),
inference(split_conjunct,[status(thm)],[sk_l42_co_neg]) ).
cnf(c_101,negated_conjecture,
( pair_in_list(insert_slb(sK0,pair(sK4,sK5)),sK7,sK8)
| ~ check_cpq(triple(sK3,insert_slb(sK0,pair(sK4,sK5)),sK6)) ),
inference(split_conjunct,[status(thm)],[sk_l42_co_neg]) ).
cnf(c_102,negated_conjecture,
( ~ less_than(sK8,sK7)
| ~ check_cpq(triple(sK3,insert_slb(sK0,pair(sK4,sK5)),sK6)) ),
inference(split_conjunct,[status(thm)],[sk_l42_co_neg]) ).
cnf(c_9338,plain,
( less_than(B,A)
| less_than(B,A)
| strictly_less_than(A,B) ),
inference(resolve,[status(thm)],[c_47,c_43]) ).
cnf(c_108,plain,
( less_than(B,A)
| strictly_less_than(A,B) ),
inference(copy,[status(thm)],[c_9338]) ).
cnf(c_9339,plain,
( D != C
| pair_in_list(insert_slb(A,pair(B,C)),B,D) ),
inference(xxres,[status(thm)],[c_59]) ).
cnf(c_114,plain,
pair_in_list(insert_slb(A,pair(B,C)),B,C),
inference(xxres,[status(thm)],[c_9339]) ).
cnf(c_127,plain,
( check_cpq(triple(C,insert_slb(create_slb,pair(B,A)),D))
| ~ less_than(A,B) ),
inference(resolve,[status(thm)],[c_74,c_72]) ).
cnf(c_241,plain,
( pair_in_list(insert_slb(sK0,pair(C,D)),sK1(A,B),sK2(A,B))
| check_cpq(triple(A,sK0,B)) ),
inference(resolve,[status(thm)],[c_98,c_58]) ).
cnf(c_275,plain,
( ~ check_cpq(triple(C,insert_slb(D,pair(B,A)),E))
| less_than(A,B) ),
inference(resolve,[status(thm)],[c_108,c_75]) ).
cnf(c_311,plain,
( less_than(sK5,sK4)
| check_cpq(triple(sK3,insert_slb(sK0,pair(sK4,sK5)),sK6)) ),
inference(resolve,[status(thm)],[c_114,c_100]) ).
cnf(c_1021,plain,
( check_cpq(triple(A,insert_slb(create_slb,pair(sK4,sK5)),B))
| check_cpq(triple(sK3,insert_slb(sK0,pair(sK4,sK5)),sK6)) ),
inference(resolve,[status(thm)],[c_311,c_127]) ).
cnf(c_1294,plain,
( less_than(sK2(A,B),sK1(A,B))
| check_cpq(triple(sK3,insert_slb(sK0,pair(sK4,sK5)),sK6))
| check_cpq(triple(A,sK0,B)) ),
inference(resolve,[status(thm)],[c_241,c_100]) ).
cnf(c_6841,plain,
( less_than(sK5,sK4)
| check_cpq(triple(A,insert_slb(create_slb,pair(sK4,sK5)),B)) ),
inference(resolve,[status(thm)],[c_1021,c_275]) ).
cnf(c_6922,plain,
( check_cpq(triple(C,insert_slb(create_slb,pair(sK4,sK5)),D))
| check_cpq(triple(A,insert_slb(create_slb,pair(sK4,sK5)),B)) ),
inference(resolve,[status(thm)],[c_6841,c_127]) ).
cnf(c_6947,plain,
check_cpq(triple(A,insert_slb(create_slb,pair(sK4,sK5)),B)),
inference(factor,[status(thm)],[c_6922]) ).
cnf(c_6953,plain,
less_than(sK5,sK4),
inference(resolve,[status(thm)],[c_6947,c_275]) ).
cnf(c_6989,plain,
( ~ check_cpq(triple(A,B,C))
| check_cpq(triple(A,insert_slb(B,pair(sK4,sK5)),C)) ),
inference(resolve,[status(thm)],[c_6953,c_74]) ).
cnf(c_6990,plain,
( check_cpq(triple(A,B,C))
| ~ check_cpq(triple(A,insert_slb(B,pair(sK4,sK5)),C)) ),
inference(resolve,[status(thm)],[c_6953,c_73]) ).
cnf(c_9340,negated_conjecture,
( check_cpq(triple(A,sK0,B))
| check_cpq(triple(sK3,insert_slb(sK0,pair(sK4,sK5)),sK6))
| check_cpq(triple(A,sK0,B)) ),
inference(resolve,[status(thm)],[c_1294,c_99]) ).
cnf(c_8501,negated_conjecture,
( check_cpq(triple(sK3,insert_slb(sK0,pair(sK4,sK5)),sK6))
| check_cpq(triple(A,sK0,B)) ),
inference(copy,[status(thm)],[c_9340]) ).
cnf(c_8507,plain,
( check_cpq(triple(A,insert_slb(sK0,pair(sK4,sK5)),B))
| check_cpq(triple(sK3,insert_slb(sK0,pair(sK4,sK5)),sK6)) ),
inference(resolve,[status(thm)],[c_8501,c_6989]) ).
cnf(c_8517,plain,
( check_cpq(triple(sK3,sK0,sK6))
| check_cpq(triple(A,sK0,B)) ),
inference(resolve,[status(thm)],[c_8501,c_6990]) ).
cnf(c_8603,plain,
check_cpq(triple(sK3,insert_slb(sK0,pair(sK4,sK5)),sK6)),
inference(factor,[status(thm)],[c_8507]) ).
cnf(c_8604,plain,
check_cpq(triple(sK3,sK0,sK6)),
inference(factor,[status(thm)],[c_8517]) ).
cnf(c_8652,negated_conjecture,
~ less_than(sK8,sK7),
inference(resolve,[status(thm)],[c_8603,c_102]) ).
cnf(c_8653,negated_conjecture,
pair_in_list(insert_slb(sK0,pair(sK4,sK5)),sK7,sK8),
inference(resolve,[status(thm)],[c_8603,c_101]) ).
cnf(c_8743,plain,
( less_than(B,A)
| ~ pair_in_list(sK0,A,B) ),
inference(resolve,[status(thm)],[c_8604,c_97]) ).
cnf(c_9055,negated_conjecture,
~ pair_in_list(sK0,sK7,sK8),
inference(resolve,[status(thm)],[c_8743,c_8652]) ).
cnf(c_9341,negated_conjecture,
( sK8 = sK5
| pair_in_list(sK0,sK7,sK8) ),
inference(resolve,[status(thm)],[c_8653,c_57]) ).
cnf(c_9057,negated_conjecture,
sK8 = sK5,
inference(resolve,[status(thm)],[c_9055,c_9341]) ).
cnf(c_9342,negated_conjecture,
( sK7 = sK4
| pair_in_list(sK0,sK7,sK8) ),
inference(resolve,[status(thm)],[c_8653,c_56]) ).
cnf(c_9058,negated_conjecture,
( sK7 = sK4
| pair_in_list(sK0,sK7,sK5) ),
inference(paramod,[status(thm)],[c_9057,c_9342]) ).
cnf(c_9060,negated_conjecture,
~ pair_in_list(sK0,sK7,sK5),
inference(paramod,[status(thm)],[c_9057,c_9055]) ).
cnf(c_9249,negated_conjecture,
~ less_than(sK5,sK7),
inference(paramod,[status(thm)],[c_9057,c_8652]) ).
cnf(c_9293,negated_conjecture,
sK7 = sK4,
inference(resolve,[status(thm)],[c_9060,c_9058]) ).
cnf(c_9343,negated_conjecture,
~ less_than(sK5,sK4),
inference(paramod,[status(thm)],[c_9293,c_9249]) ).
cnf(c_9337,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_6953,c_9343]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV406+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n026.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Sat Sep 26 13:44:10 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.45 % Process 1134445 was started by sandbox on n026,
% 0.18/0.45 % Sat Sep 26 13:44:10 2026
% 0.18/0.45 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.18/0.47
% 0.18/0.47 % From the command line: assign(max_seconds, 300).
% 198.60/29.37
% 198.60/29.37 % given #500 (A,wt=18): 415 check_cpq(triple(A,insert_slb(create_slb,pair(c7,c6)),B)) | -check_cpq(triple(c2,insert_slb(c1,pair(c4,c5)),c3)). [resolve(130,b,102,b)].
% 198.60/29.37
% 198.60/29.37 % given #1000 (T,wt=14): 2097 succ_cpq(A,findmin_cpq_eff(insert_cpq(remove_cpq(insert_cpq(findmin_cpq_eff(insert_cpq(findmin_cpq_eff(A),B)),C),D),E))). [resolve(797,a,70,a)].
% 198.60/29.37
% 198.60/29.37 % given #1500 (F,wt=23): 6770 -ok(insert_cpq(insert_cpq(remove_cpq(remove_cpq(insert_cpq(triple(A,insert_slb(B,pair(C,bottom)),bad),D),D),C),E),F)). [para(80(a,1),4275(a,1,1,1,1,1))].
% 198.60/29.37
% 198.60/29.37 % SZS status Theorem for theBenchmark
% 198.60/29.37
% 198.60/29.37 % Proof 1 at 3.73 (+ 1.03) seconds.
% 198.60/29.37 % Length of proof is 52.
% 198.60/29.37 % Level of proof is 17.
% 198.60/29.37 % Maximum clause weight is 21.000.
% 198.60/29.37 % Given clauses 1947.
% 198.60/29.37
% 198.60/29.37 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------