%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV384+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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:36 AM UTC 2026
% Result : Theorem 2.18s 0.76s
% Output : CNFRefutation 2.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 5
% Syntax : Number of formulae : 68 ( 11 unt; 0 def)
% Number of atoms : 253 ( 9 equ)
% Maximal formula atoms : 42 ( 3 avg)
% Number of connectives : 322 ( 137 ~; 152 |; 21 &)
% ( 1 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 13 con; 0-3 aty)
% Number of variables : 151 ( 4 sgn 92 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax40,axiom,
! [U,V] :
( ok(triple(U,V,bad))
<=> $false ),
file('theBenchmark.p',ax40) ).
fof(ax41,axiom,
! [U,V,W] :
( ~ ok(triple(U,V,W))
=> W = bad ),
file('theBenchmark.p',ax41) ).
fof(l20_induction,axiom,
( ! [U,V,W,X,Y,Z] :
( succ_cpq(triple(U,V,W),triple(X,Y,Z))
=> ( ( ~ ok(triple(X,Y,Z))
| ~ check_cpq(triple(X,Y,Z)) )
=> ( ~ ok(im_succ_cpq(triple(X,Y,Z)))
| ~ check_cpq(im_succ_cpq(triple(X,Y,Z))) ) ) )
=> ! [X1,X2,X3] :
( ( ~ ok(triple(X1,X2,X3))
| ~ check_cpq(triple(X1,X2,X3)) )
=> ! [X4,X5,X6] :
( succ_cpq(triple(X1,X2,X3),triple(X4,X5,X6))
=> ( ~ check_cpq(triple(X4,X5,X6))
| ~ ok(triple(X4,X5,X6)) ) ) ) ),
file('theBenchmark.p',l20_induction) ).
fof(l12_l13,axiom,
! [U,V,W] :
( ( ~ ok(triple(U,V,W))
| ~ check_cpq(triple(U,V,W)) )
=> ( ~ ok(im_succ_cpq(triple(U,V,W)))
| ~ check_cpq(im_succ_cpq(triple(U,V,W))) ) ),
file('theBenchmark.p',l12_l13) ).
fof(l20_co,conjecture,
! [U,V,W] :
( ( ~ ok(triple(U,V,W))
| ~ check_cpq(triple(U,V,W)) )
=> ! [X,Y,Z] :
( succ_cpq(triple(U,V,W),triple(X,Y,Z))
=> ( ~ check_cpq(triple(X,Y,Z))
| ~ ok(triple(X,Y,Z)) ) ) ),
file('theBenchmark.p',l20_co) ).
fof(l20_co_neg,negated_conjecture,
~ ! [U,V,W] :
( ( ~ ok(triple(U,V,W))
| ~ check_cpq(triple(U,V,W)) )
=> ! [X,Y,Z] :
( succ_cpq(triple(U,V,W),triple(X,Y,Z))
=> ( ~ check_cpq(triple(X,Y,Z))
| ~ ok(triple(X,Y,Z)) ) ) ),
inference(assume_negation,[status(cth)],[l20_co]) ).
cnf(c_80,plain,
~ ok(triple(A,B,bad)),
inference(clausify,[status(thm)],[ax40]) ).
cnf(c_81,plain,
( bad = C
| ok(triple(A,B,C)) ),
inference(clausify,[status(thm)],[ax41]) ).
fof(nnf_41,plain,
( ! [X1,X2,X3] :
( ! [X4,X5,X6] :
( ~ check_cpq(triple(X4,X5,X6))
| ~ ok(triple(X4,X5,X6))
| ~ succ_cpq(triple(X1,X2,X3),triple(X4,X5,X6)) )
| ( ok(triple(X1,X2,X3))
& check_cpq(triple(X1,X2,X3)) ) )
| ? [U,V,W,X,Y,Z] :
( ok(im_succ_cpq(triple(X,Y,Z)))
& check_cpq(im_succ_cpq(triple(X,Y,Z)))
& ( ~ ok(triple(X,Y,Z))
| ~ check_cpq(triple(X,Y,Z)) )
& succ_cpq(triple(U,V,W),triple(X,Y,Z)) ) ),
inference(fof_nnf,[status(thm)],[l20_induction]) ).
fof(sk_l20_induction_sk,plain,
( ! [X1,X2,X3] :
( ! [X4,X5,X6] :
( ~ check_cpq(triple(X4,X5,X6))
| ~ ok(triple(X4,X5,X6))
| ~ succ_cpq(triple(X1,X2,X3),triple(X4,X5,X6)) )
| ( ok(triple(X1,X2,X3))
& check_cpq(triple(X1,X2,X3)) ) )
| ( ok(im_succ_cpq(triple(sK0,sK1,sK2)))
& check_cpq(im_succ_cpq(triple(sK0,sK1,sK2)))
& ( ~ ok(triple(sK0,sK1,sK2))
| ~ check_cpq(triple(sK0,sK1,sK2)) )
& succ_cpq(triple(sK9,sK10,sK11),triple(sK0,sK1,sK2)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK10,sK11,sK0,sK1,sK2]),skolemize(U,sK9),skolemize(V,sK10),skolemize(W,sK11),skolemize(X,sK0),skolemize(Y,sK1),skolemize(Z,sK2)],[nnf_41]) ).
fof(sk_l20_induction,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( ~ check_cpq(triple(VAR_3,VAR_4,VAR_5))
| ~ ok(triple(VAR_3,VAR_4,VAR_5))
| ~ succ_cpq(triple(VAR_0,VAR_1,VAR_2),triple(VAR_3,VAR_4,VAR_5))
| ok(triple(VAR_0,VAR_1,VAR_2))
| ok(im_succ_cpq(triple(sK0,sK1,sK2))) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( ~ check_cpq(triple(VAR_3,VAR_4,VAR_5))
| ~ ok(triple(VAR_3,VAR_4,VAR_5))
| ~ succ_cpq(triple(VAR_0,VAR_1,VAR_2),triple(VAR_3,VAR_4,VAR_5))
| check_cpq(triple(VAR_0,VAR_1,VAR_2))
| ok(im_succ_cpq(triple(sK0,sK1,sK2))) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( ~ check_cpq(triple(VAR_3,VAR_4,VAR_5))
| ~ ok(triple(VAR_3,VAR_4,VAR_5))
| ~ succ_cpq(triple(VAR_0,VAR_1,VAR_2),triple(VAR_3,VAR_4,VAR_5))
| ok(triple(VAR_0,VAR_1,VAR_2))
| check_cpq(im_succ_cpq(triple(sK0,sK1,sK2))) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( ~ check_cpq(triple(VAR_3,VAR_4,VAR_5))
| ~ ok(triple(VAR_3,VAR_4,VAR_5))
| ~ succ_cpq(triple(VAR_0,VAR_1,VAR_2),triple(VAR_3,VAR_4,VAR_5))
| check_cpq(triple(VAR_0,VAR_1,VAR_2))
| check_cpq(im_succ_cpq(triple(sK0,sK1,sK2))) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( ~ check_cpq(triple(VAR_3,VAR_4,VAR_5))
| ~ ok(triple(VAR_3,VAR_4,VAR_5))
| ~ succ_cpq(triple(VAR_0,VAR_1,VAR_2),triple(VAR_3,VAR_4,VAR_5))
| ok(triple(VAR_0,VAR_1,VAR_2))
| ~ ok(triple(sK0,sK1,sK2))
| ~ check_cpq(triple(sK0,sK1,sK2)) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( ~ check_cpq(triple(VAR_3,VAR_4,VAR_5))
| ~ ok(triple(VAR_3,VAR_4,VAR_5))
| ~ succ_cpq(triple(VAR_0,VAR_1,VAR_2),triple(VAR_3,VAR_4,VAR_5))
| check_cpq(triple(VAR_0,VAR_1,VAR_2))
| ~ ok(triple(sK0,sK1,sK2))
| ~ check_cpq(triple(sK0,sK1,sK2)) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( ~ check_cpq(triple(VAR_3,VAR_4,VAR_5))
| ~ ok(triple(VAR_3,VAR_4,VAR_5))
| ~ succ_cpq(triple(VAR_0,VAR_1,VAR_2),triple(VAR_3,VAR_4,VAR_5))
| ok(triple(VAR_0,VAR_1,VAR_2))
| succ_cpq(triple(sK9,sK10,sK11),triple(sK0,sK1,sK2)) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( ~ check_cpq(triple(VAR_3,VAR_4,VAR_5))
| ~ ok(triple(VAR_3,VAR_4,VAR_5))
| ~ succ_cpq(triple(VAR_0,VAR_1,VAR_2),triple(VAR_3,VAR_4,VAR_5))
| check_cpq(triple(VAR_0,VAR_1,VAR_2))
| succ_cpq(triple(sK9,sK10,sK11),triple(sK0,sK1,sK2)) ) ),
inference(cnf_transformation,[status(thm)],[sk_l20_induction_sk]) ).
cnf(c_101,plain,
( ~ check_cpq(triple(D,E,F))
| ~ ok(triple(D,E,F))
| ~ succ_cpq(triple(A,B,C),triple(D,E,F))
| check_cpq(triple(A,B,C))
| ~ ok(triple(sK0,sK1,sK2))
| ~ check_cpq(triple(sK0,sK1,sK2)) ),
inference(split_conjunct,[status(thm)],[sk_l20_induction]) ).
cnf(c_102,plain,
( ~ check_cpq(triple(D,E,F))
| ~ ok(triple(D,E,F))
| ~ succ_cpq(triple(A,B,C),triple(D,E,F))
| ok(triple(A,B,C))
| ~ ok(triple(sK0,sK1,sK2))
| ~ check_cpq(triple(sK0,sK1,sK2)) ),
inference(split_conjunct,[status(thm)],[sk_l20_induction]) ).
cnf(c_103,plain,
( ~ check_cpq(triple(D,E,F))
| ~ ok(triple(D,E,F))
| ~ succ_cpq(triple(A,B,C),triple(D,E,F))
| check_cpq(triple(A,B,C))
| check_cpq(im_succ_cpq(triple(sK0,sK1,sK2))) ),
inference(split_conjunct,[status(thm)],[sk_l20_induction]) ).
cnf(c_104,plain,
( ~ check_cpq(triple(D,E,F))
| ~ ok(triple(D,E,F))
| ~ succ_cpq(triple(A,B,C),triple(D,E,F))
| ok(triple(A,B,C))
| check_cpq(im_succ_cpq(triple(sK0,sK1,sK2))) ),
inference(split_conjunct,[status(thm)],[sk_l20_induction]) ).
cnf(c_105,plain,
( ~ check_cpq(triple(D,E,F))
| ~ ok(triple(D,E,F))
| ~ succ_cpq(triple(A,B,C),triple(D,E,F))
| check_cpq(triple(A,B,C))
| ok(im_succ_cpq(triple(sK0,sK1,sK2))) ),
inference(split_conjunct,[status(thm)],[sk_l20_induction]) ).
cnf(c_106,plain,
( ~ check_cpq(triple(D,E,F))
| ~ ok(triple(D,E,F))
| ~ succ_cpq(triple(A,B,C),triple(D,E,F))
| ok(triple(A,B,C))
| ok(im_succ_cpq(triple(sK0,sK1,sK2))) ),
inference(split_conjunct,[status(thm)],[sk_l20_induction]) ).
cnf(c_107,plain,
( ~ ok(im_succ_cpq(triple(A,B,C)))
| ~ check_cpq(im_succ_cpq(triple(A,B,C)))
| check_cpq(triple(A,B,C)) ),
inference(clausify,[status(thm)],[l12_l13]) ).
cnf(c_108,plain,
( ~ ok(im_succ_cpq(triple(A,B,C)))
| ~ check_cpq(im_succ_cpq(triple(A,B,C)))
| ok(triple(A,B,C)) ),
inference(clausify,[status(thm)],[l12_l13]) ).
fof(nnf_43,plain,
? [U,V,W] :
( ? [X,Y,Z] :
( check_cpq(triple(X,Y,Z))
& ok(triple(X,Y,Z))
& succ_cpq(triple(U,V,W),triple(X,Y,Z)) )
& ( ~ ok(triple(U,V,W))
| ~ check_cpq(triple(U,V,W)) ) ),
inference(fof_nnf,[status(thm)],[l20_co_neg]) ).
fof(sk_l20_co_neg,plain,
( check_cpq(triple(sK6,sK7,sK8))
& ok(triple(sK6,sK7,sK8))
& succ_cpq(triple(sK3,sK4,sK5),triple(sK6,sK7,sK8))
& ( ~ ok(triple(sK3,sK4,sK5))
| ~ check_cpq(triple(sK3,sK4,sK5)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5,sK6,sK7,sK8]),skolemize(U,sK3),skolemize(V,sK4),skolemize(W,sK5),skolemize(X,sK6),skolemize(Y,sK7),skolemize(Z,sK8)],[nnf_43]) ).
cnf(c_109,negated_conjecture,
( ~ ok(triple(sK3,sK4,sK5))
| ~ check_cpq(triple(sK3,sK4,sK5)) ),
inference(split_conjunct,[status(thm)],[sk_l20_co_neg]) ).
cnf(c_110,negated_conjecture,
succ_cpq(triple(sK3,sK4,sK5),triple(sK6,sK7,sK8)),
inference(split_conjunct,[status(thm)],[sk_l20_co_neg]) ).
cnf(c_111,negated_conjecture,
ok(triple(sK6,sK7,sK8)),
inference(split_conjunct,[status(thm)],[sk_l20_co_neg]) ).
cnf(c_112,negated_conjecture,
check_cpq(triple(sK6,sK7,sK8)),
inference(split_conjunct,[status(thm)],[sk_l20_co_neg]) ).
cnf(c_785,negated_conjecture,
( bad = sK5
| ~ check_cpq(triple(sK3,sK4,sK5)) ),
inference(resolve,[status(thm)],[c_109,c_81]) ).
cnf(c_251,negated_conjecture,
( sK5 = bad
| ~ check_cpq(triple(sK3,sK4,sK5)) ),
inference(copy,[status(thm)],[c_785]) ).
cnf(c_786,negated_conjecture,
( ~ check_cpq(triple(sK6,sK7,sK8))
| ~ ok(triple(sK6,sK7,sK8))
| ok(triple(sK3,sK4,sK5))
| ok(im_succ_cpq(triple(sK0,sK1,sK2))) ),
inference(resolve,[status(thm)],[c_110,c_106]) ).
cnf(c_787,negated_conjecture,
( ~ check_cpq(triple(sK6,sK7,sK8))
| ok(triple(sK3,sK4,sK5))
| ok(im_succ_cpq(triple(sK0,sK1,sK2))) ),
inference(resolve,[status(thm)],[c_111,c_786]) ).
cnf(c_252,negated_conjecture,
( ok(triple(sK3,sK4,sK5))
| ok(im_succ_cpq(triple(sK0,sK1,sK2))) ),
inference(resolve,[status(thm)],[c_112,c_787]) ).
cnf(c_788,negated_conjecture,
( ~ check_cpq(triple(sK6,sK7,sK8))
| ~ ok(triple(sK6,sK7,sK8))
| check_cpq(triple(sK3,sK4,sK5))
| ok(im_succ_cpq(triple(sK0,sK1,sK2))) ),
inference(resolve,[status(thm)],[c_110,c_105]) ).
cnf(c_789,negated_conjecture,
( ~ check_cpq(triple(sK6,sK7,sK8))
| check_cpq(triple(sK3,sK4,sK5))
| ok(im_succ_cpq(triple(sK0,sK1,sK2))) ),
inference(resolve,[status(thm)],[c_111,c_788]) ).
cnf(c_253,negated_conjecture,
( check_cpq(triple(sK3,sK4,sK5))
| ok(im_succ_cpq(triple(sK0,sK1,sK2))) ),
inference(resolve,[status(thm)],[c_112,c_789]) ).
cnf(c_790,negated_conjecture,
( ~ check_cpq(triple(sK6,sK7,sK8))
| ~ ok(triple(sK6,sK7,sK8))
| ok(triple(sK3,sK4,sK5))
| check_cpq(im_succ_cpq(triple(sK0,sK1,sK2))) ),
inference(resolve,[status(thm)],[c_110,c_104]) ).
cnf(c_791,negated_conjecture,
( ~ check_cpq(triple(sK6,sK7,sK8))
| ok(triple(sK3,sK4,sK5))
| check_cpq(im_succ_cpq(triple(sK0,sK1,sK2))) ),
inference(resolve,[status(thm)],[c_111,c_790]) ).
cnf(c_254,negated_conjecture,
( ok(triple(sK3,sK4,sK5))
| check_cpq(im_succ_cpq(triple(sK0,sK1,sK2))) ),
inference(resolve,[status(thm)],[c_112,c_791]) ).
cnf(c_792,negated_conjecture,
( ~ check_cpq(triple(sK6,sK7,sK8))
| ~ ok(triple(sK6,sK7,sK8))
| check_cpq(triple(sK3,sK4,sK5))
| check_cpq(im_succ_cpq(triple(sK0,sK1,sK2))) ),
inference(resolve,[status(thm)],[c_110,c_103]) ).
cnf(c_793,negated_conjecture,
( ~ check_cpq(triple(sK6,sK7,sK8))
| check_cpq(triple(sK3,sK4,sK5))
| check_cpq(im_succ_cpq(triple(sK0,sK1,sK2))) ),
inference(resolve,[status(thm)],[c_111,c_792]) ).
cnf(c_255,negated_conjecture,
( check_cpq(triple(sK3,sK4,sK5))
| check_cpq(im_succ_cpq(triple(sK0,sK1,sK2))) ),
inference(resolve,[status(thm)],[c_112,c_793]) ).
cnf(c_794,negated_conjecture,
( ~ check_cpq(triple(sK6,sK7,sK8))
| ~ ok(triple(sK6,sK7,sK8))
| ok(triple(sK3,sK4,sK5))
| ~ ok(triple(sK0,sK1,sK2))
| ~ check_cpq(triple(sK0,sK1,sK2)) ),
inference(resolve,[status(thm)],[c_110,c_102]) ).
cnf(c_795,negated_conjecture,
( ~ check_cpq(triple(sK6,sK7,sK8))
| ok(triple(sK3,sK4,sK5))
| ~ ok(triple(sK0,sK1,sK2))
| ~ check_cpq(triple(sK0,sK1,sK2)) ),
inference(resolve,[status(thm)],[c_111,c_794]) ).
cnf(c_256,negated_conjecture,
( ok(triple(sK3,sK4,sK5))
| ~ ok(triple(sK0,sK1,sK2))
| ~ check_cpq(triple(sK0,sK1,sK2)) ),
inference(resolve,[status(thm)],[c_112,c_795]) ).
cnf(c_796,negated_conjecture,
( ~ check_cpq(triple(sK6,sK7,sK8))
| ~ ok(triple(sK6,sK7,sK8))
| check_cpq(triple(sK3,sK4,sK5))
| ~ ok(triple(sK0,sK1,sK2))
| ~ check_cpq(triple(sK0,sK1,sK2)) ),
inference(resolve,[status(thm)],[c_110,c_101]) ).
cnf(c_797,negated_conjecture,
( ~ check_cpq(triple(sK6,sK7,sK8))
| check_cpq(triple(sK3,sK4,sK5))
| ~ ok(triple(sK0,sK1,sK2))
| ~ check_cpq(triple(sK0,sK1,sK2)) ),
inference(resolve,[status(thm)],[c_111,c_796]) ).
cnf(c_257,negated_conjecture,
( check_cpq(triple(sK3,sK4,sK5))
| ~ ok(triple(sK0,sK1,sK2))
| ~ check_cpq(triple(sK0,sK1,sK2)) ),
inference(resolve,[status(thm)],[c_112,c_797]) ).
cnf(c_486,plain,
( ~ check_cpq(im_succ_cpq(triple(sK0,sK1,sK2)))
| ok(triple(sK0,sK1,sK2))
| check_cpq(triple(sK3,sK4,sK5)) ),
inference(resolve,[status(thm)],[c_253,c_108]) ).
cnf(c_487,plain,
( ~ check_cpq(im_succ_cpq(triple(sK0,sK1,sK2)))
| check_cpq(triple(sK0,sK1,sK2))
| check_cpq(triple(sK3,sK4,sK5)) ),
inference(resolve,[status(thm)],[c_253,c_107]) ).
cnf(c_488,plain,
( ~ check_cpq(triple(sK3,sK4,sK5))
| check_cpq(im_succ_cpq(triple(sK0,sK1,sK2))) ),
inference(resolve,[status(thm)],[c_254,c_109]) ).
cnf(c_798,plain,
( check_cpq(im_succ_cpq(triple(sK0,sK1,sK2)))
| check_cpq(im_succ_cpq(triple(sK0,sK1,sK2))) ),
inference(resolve,[status(thm)],[c_488,c_255]) ).
cnf(c_585,plain,
check_cpq(im_succ_cpq(triple(sK0,sK1,sK2))),
inference(copy,[status(thm)],[c_798]) ).
cnf(c_586,plain,
( check_cpq(triple(sK0,sK1,sK2))
| check_cpq(triple(sK3,sK4,sK5)) ),
inference(resolve,[status(thm)],[c_585,c_487]) ).
cnf(c_587,plain,
( ok(triple(sK0,sK1,sK2))
| check_cpq(triple(sK3,sK4,sK5)) ),
inference(resolve,[status(thm)],[c_585,c_486]) ).
cnf(c_589,plain,
( sK5 = bad
| check_cpq(triple(sK0,sK1,sK2)) ),
inference(resolve,[status(thm)],[c_586,c_251]) ).
cnf(c_799,plain,
( check_cpq(triple(sK3,sK4,sK5))
| ~ check_cpq(triple(sK0,sK1,sK2))
| check_cpq(triple(sK3,sK4,sK5)) ),
inference(resolve,[status(thm)],[c_587,c_257]) ).
cnf(c_607,plain,
( ~ check_cpq(triple(sK0,sK1,sK2))
| check_cpq(triple(sK3,sK4,sK5)) ),
inference(copy,[status(thm)],[c_799]) ).
cnf(c_714,plain,
( sK5 = bad
| check_cpq(triple(sK3,sK4,sK5)) ),
inference(resolve,[status(thm)],[c_607,c_589]) ).
cnf(c_800,plain,
( sK5 = bad
| sK5 = bad ),
inference(resolve,[status(thm)],[c_714,c_251]) ).
cnf(c_716,plain,
sK5 = bad,
inference(copy,[status(thm)],[c_800]) ).
cnf(c_801,negated_conjecture,
( ok(triple(sK3,sK4,bad))
| ~ ok(triple(sK0,sK1,sK2))
| ~ check_cpq(triple(sK0,sK1,sK2)) ),
inference(paramod,[status(thm)],[c_716,c_256]) ).
cnf(c_754,negated_conjecture,
( ~ ok(triple(sK0,sK1,sK2))
| ~ check_cpq(triple(sK0,sK1,sK2)) ),
inference(resolve,[status(thm)],[c_80,c_801]) ).
cnf(c_802,negated_conjecture,
( ok(triple(sK3,sK4,bad))
| ok(im_succ_cpq(triple(sK0,sK1,sK2))) ),
inference(paramod,[status(thm)],[c_716,c_252]) ).
cnf(c_756,negated_conjecture,
ok(im_succ_cpq(triple(sK0,sK1,sK2))),
inference(resolve,[status(thm)],[c_80,c_802]) ).
cnf(c_803,plain,
( ~ ok(im_succ_cpq(triple(sK0,sK1,sK2)))
| ok(triple(sK0,sK1,sK2)) ),
inference(resolve,[status(thm)],[c_585,c_108]) ).
cnf(c_782,plain,
ok(triple(sK0,sK1,sK2)),
inference(resolve,[status(thm)],[c_756,c_803]) ).
cnf(c_804,plain,
( ~ ok(im_succ_cpq(triple(sK0,sK1,sK2)))
| check_cpq(triple(sK0,sK1,sK2)) ),
inference(resolve,[status(thm)],[c_585,c_107]) ).
cnf(c_783,plain,
check_cpq(triple(sK0,sK1,sK2)),
inference(resolve,[status(thm)],[c_756,c_804]) ).
cnf(c_805,negated_conjecture,
~ ok(triple(sK0,sK1,sK2)),
inference(resolve,[status(thm)],[c_783,c_754]) ).
cnf(c_784,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_782,c_805]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV384+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.40 % Computer : n011.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 : Sat Sep 26 13:40:29 UTC 2026
% 0.13/0.41 % CPUTime :
% 0.13/0.41 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.41 % Process 684782 was started by sandbox2 on n011,
% 0.13/0.41 % Sat Sep 26 13:40:29 2026
% 0.13/0.41 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.13/0.43
% 0.13/0.43 % From the command line: assign(max_seconds, 300).
% 2.18/0.76
% 2.18/0.76 % SZS status Theorem for theBenchmark
% 2.18/0.76
% 2.18/0.76 % Proof 1 at 0.26 (+ 0.07) seconds.
% 2.18/0.76 % Length of proof is 41.
% 2.18/0.76 % Level of proof is 11.
% 2.18/0.76 % Maximum clause weight is 45.000.
% 2.18/0.76 % Given clauses 175.
% 2.18/0.76
% 2.18/0.76 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------