%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV408+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:13:10 PM UTC 2026
% Result : Theorem 45.98s 7.11s
% Output : Proof 45.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 4
% Syntax : Number of formulae : 33 ( 10 unt; 0 def)
% Number of atoms : 87 ( 17 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 80 ( 26 ~; 36 |; 14 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-3 aty)
% Number of variables : 54 ( 4 sgn 33 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f41,lemma,
! [U,V,W] :
( ( strictly_less_than(V,W)
& contains_slb(U,V) )
=> ( ? [X] :
( less_than(W,X)
& pair_in_list(update_slb(U,W),V,X) )
| pair_in_list(update_slb(U,W),V,W) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l44_l45) ).
fof(f41_nnf,plain,
! [U,V,W] :
( ? [X] :
( less_than(W,X)
& pair_in_list(update_slb(U,W),V,X) )
| pair_in_list(update_slb(U,W),V,W)
| ~ strictly_less_than(V,W)
| ~ contains_slb(U,V) ),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [U,V,W] :
( ( less_than(W,sk0(U,V,W))
& pair_in_list(update_slb(U,W),V,sk0(U,V,W)) )
| pair_in_list(update_slb(U,W),V,W)
| ~ strictly_less_than(V,W)
| ~ contains_slb(U,V) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f41_nnf]) ).
cnf(c52,plain,
( pair_in_list(update_slb(X0,X2),X1,sk0(X0,X1,X2))
| pair_in_list(update_slb(X0,X2),X1,X2)
| ~ strictly_less_than(X1,X2)
| ~ contains_slb(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
fof(f42,conjecture,
! [U,V,W,X] :
( ( strictly_less_than(X,findmin_cpq_res(triple(U,V,W)))
& contains_slb(V,X) )
=> ( ? [Y] :
( less_than(findmin_pqp_res(U),Y)
& pair_in_list(update_slb(V,findmin_pqp_res(U)),X,Y) )
| pair_in_list(update_slb(V,findmin_pqp_res(U)),X,findmin_pqp_res(U)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l44_co) ).
fof(f42_neg,negated_conjecture,
~ ! [U,V,W,X] :
( ( strictly_less_than(X,findmin_cpq_res(triple(U,V,W)))
& contains_slb(V,X) )
=> ( ? [Y] :
( less_than(findmin_pqp_res(U),Y)
& pair_in_list(update_slb(V,findmin_pqp_res(U)),X,Y) )
| pair_in_list(update_slb(V,findmin_pqp_res(U)),X,findmin_pqp_res(U)) ) ),
inference(negated_conjecture,[status(cth)],[f42]) ).
fof(f42_nnf,plain,
? [U,V,W,X] :
( ! [Y] :
( ~ less_than(findmin_pqp_res(U),Y)
| ~ pair_in_list(update_slb(V,findmin_pqp_res(U)),X,Y) )
& ~ pair_in_list(update_slb(V,findmin_pqp_res(U)),X,findmin_pqp_res(U))
& strictly_less_than(X,findmin_cpq_res(triple(U,V,W)))
& contains_slb(V,X) ),
inference(nnf_transformation,[status(thm)],[f42_neg]) ).
fof(f42_sk,plain,
! [Y] :
( ( ~ less_than(findmin_pqp_res(sk1),Y)
| ~ pair_in_list(update_slb(sk2,findmin_pqp_res(sk1)),sk4,Y) )
& ~ pair_in_list(update_slb(sk2,findmin_pqp_res(sk1)),sk4,findmin_pqp_res(sk1))
& strictly_less_than(sk4,findmin_cpq_res(triple(sk1,sk2,sk3)))
& contains_slb(sk2,sk4) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk1,sk2,sk3,sk4])],[f42_nnf]) ).
cnf(c54,plain,
contains_slb(sk2,sk4),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(p788,plain,
( pair_in_list(update_slb(sk2,X0),sk4,sk0(sk2,sk4,X0))
| pair_in_list(update_slb(sk2,X0),sk4,X0)
| ~ strictly_less_than(sk4,X0) ),
inference(resolution,[status(thm)],[c52,c54]) ).
fof(f38,axiom,
! [U,V,W,X] :
( V != create_slb
=> findmin_cpq_res(triple(U,V,W)) = findmin_pqp_res(U) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax51) ).
fof(f38_nnf,plain,
! [U,V,W,X] :
( findmin_cpq_res(triple(U,V,W)) = findmin_pqp_res(U)
| V = create_slb ),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [V,U,W] :
( findmin_cpq_res(triple(U,V,W)) = findmin_pqp_res(U)
| V = create_slb ),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c49,plain,
( findmin_cpq_res(triple(X0,X1,X2)) = findmin_pqp_res(X0)
| X1 = create_slb ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(c55,plain,
strictly_less_than(sk4,findmin_cpq_res(triple(sk1,sk2,sk3))),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(p709,plain,
( strictly_less_than(sk4,findmin_pqp_res(sk1))
| sk2 = create_slb ),
inference(superposition,[status(thm)],[c49,c55]) ).
cnf(p906,plain,
( sk2 = create_slb
| pair_in_list(update_slb(sk2,findmin_pqp_res(sk1)),sk4,sk0(sk2,sk4,findmin_pqp_res(sk1)))
| pair_in_list(update_slb(sk2,findmin_pqp_res(sk1)),sk4,findmin_pqp_res(sk1)) ),
inference(resolution,[status(thm)],[p788,p709]) ).
cnf(c57,plain,
( ~ less_than(findmin_pqp_res(sk1),X4)
| ~ pair_in_list(update_slb(sk2,findmin_pqp_res(sk1)),sk4,X4) ),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(p6189,plain,
( ~ less_than(findmin_pqp_res(sk1),sk0(sk2,sk4,findmin_pqp_res(sk1)))
| sk2 = create_slb
| pair_in_list(update_slb(sk2,findmin_pqp_res(sk1)),sk4,findmin_pqp_res(sk1)) ),
inference(resolution,[status(thm)],[p906,c57]) ).
cnf(c53,plain,
( less_than(X2,sk0(X0,X1,X2))
| pair_in_list(update_slb(X0,X2),X1,X2)
| ~ strictly_less_than(X1,X2)
| ~ contains_slb(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p825,plain,
( less_than(X0,sk0(sk2,sk4,X0))
| pair_in_list(update_slb(sk2,X0),sk4,X0)
| ~ strictly_less_than(sk4,X0) ),
inference(resolution,[status(thm)],[c53,c54]) ).
cnf(p847,plain,
( sk2 = create_slb
| less_than(findmin_pqp_res(sk1),sk0(sk2,sk4,findmin_pqp_res(sk1)))
| pair_in_list(update_slb(sk2,findmin_pqp_res(sk1)),sk4,findmin_pqp_res(sk1)) ),
inference(resolution,[status(thm)],[p825,p709]) ).
cnf(c56,plain,
~ pair_in_list(update_slb(sk2,findmin_pqp_res(sk1)),sk4,findmin_pqp_res(sk1)),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(p932,plain,
( sk2 = create_slb
| less_than(findmin_pqp_res(sk1),sk0(sk2,sk4,findmin_pqp_res(sk1))) ),
inference(resolution,[status(thm)],[p847,c56]) ).
cnf(p6192,plain,
( sk2 = create_slb
| sk2 = create_slb
| pair_in_list(update_slb(sk2,findmin_pqp_res(sk1)),sk4,findmin_pqp_res(sk1)) ),
inference(resolution,[status(thm)],[p6189,p932]) ).
cnf(p6196,plain,
( sk2 = create_slb
| pair_in_list(update_slb(sk2,findmin_pqp_res(sk1)),sk4,findmin_pqp_res(sk1)) ),
inference(factoring,[status(thm)],[p6192]) ).
cnf(p6197,plain,
sk2 = create_slb,
inference(resolution,[status(thm)],[p6196,c56]) ).
cnf(p6198,plain,
contains_slb(create_slb,sk4),
inference(demodulation,[status(thm)],[p6197,c54]) ).
fof(f7,axiom,
! [U] : ~ contains_slb(create_slb,U),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax20) ).
fof(f7_nnf,plain,
! [U] : ~ contains_slb(create_slb,U),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [U] : ~ contains_slb(create_slb,U),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c9,plain,
~ contains_slb(create_slb,X0),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p8563,plain,
$false,
inference(resolution,[status(thm)],[p6198,c9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV408+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n002.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Thu Sep 24 19:32:49 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 45.98/7.11 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 45.98/7.11 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------