%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV415+2 : 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 : 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 : Sun Sep 27 09:07:40 AM UTC 2026
% Result : Theorem 1.09s 0.57s
% Output : CNFRefutation 1.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 5
% Syntax : Number of formulae : 34 ( 20 unt; 0 def)
% Number of atoms : 64 ( 63 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 57 ( 27 ~; 24 |; 4 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 18 con; 0-3 aty)
% Number of variables : 182 ( 66 sgn 71 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ax42,axiom,
! [U,V,W,X] : insert_cpq(triple(U,V,W),X) = triple(insert_pqp(U,X),insert_slb(V,pair(X,bottom)),W),
file('theBenchmark.p',ax42) ).
fof(ax54,axiom,
! [U,V] : i(triple(U,create_slb,V)) = create_pq,
file('theBenchmark.p',ax54) ).
fof(ax55,axiom,
! [U,V,W,X,Y] : i(triple(U,insert_slb(V,pair(X,Y)),W)) = insert_pq(i(triple(U,V,W)),X),
file('theBenchmark.p',ax55) ).
fof(big2_induction,axiom,
( ( ! [Y] :
( ! [Z,X1,X2,X3] : i(triple(Z,Y,X2)) = i(triple(X1,Y,X3))
=> ! [X4,X5,X6,X7,X8,X9] : i(triple(X4,insert_slb(Y,pair(X8,X9)),X6)) = i(triple(X5,insert_slb(Y,pair(X8,X9)),X7)) )
& ! [U,V,W,X] : i(triple(U,create_slb,W)) = i(triple(V,create_slb,X)) )
=> ! [X10,X11,X12,X13,X14] : i(triple(X10,X12,X13)) = i(triple(X11,X12,X14)) ),
file('theBenchmark.p',big2_induction) ).
fof(co2,conjecture,
! [U,V,W,X] : i(insert_cpq(triple(U,V,W),X)) = insert_pq(i(triple(U,V,W)),X),
file('theBenchmark.p',co2) ).
fof(co2_neg,negated_conjecture,
~ ! [U,V,W,X] : i(insert_cpq(triple(U,V,W),X)) = insert_pq(i(triple(U,V,W)),X),
inference(assume_negation,[status(cth)],[co2]) ).
fof(nnf_62,plain,
? [U,V,W,X] : i(insert_cpq(triple(U,V,W),X)) != insert_pq(i(triple(U,V,W)),X),
inference(fof_nnf,[status(thm)],[co2_neg]) ).
fof(sk_co2_neg,plain,
i(insert_cpq(triple(sK0,sK1,sK2),sK3)) != insert_pq(i(triple(sK0,sK1,sK2)),sK3),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(U,sK0),skolemize(V,sK1),skolemize(W,sK2),skolemize(X,sK3)],[nnf_62]) ).
cnf(c_133,negated_conjecture,
i(insert_cpq(triple(sK0,sK1,sK2),sK3)) != insert_pq(i(triple(sK0,sK1,sK2)),sK3),
inference(split_conjunct,[status(thm)],[sk_co2_neg]) ).
fof(nnf_61,plain,
( ! [X10,X11,X12,X13,X14] : i(triple(X11,X12,X14)) = i(triple(X10,X12,X13))
| ? [Y] :
( ? [X4,X5,X6,X7,X8,X9] : i(triple(X5,insert_slb(Y,pair(X8,X9)),X7)) != i(triple(X4,insert_slb(Y,pair(X8,X9)),X6))
& ! [Z,X1,X2,X3] : i(triple(X1,Y,X3)) = i(triple(Z,Y,X2)) )
| ? [U,V,W,X] : i(triple(V,create_slb,X)) != i(triple(U,create_slb,W)) ),
inference(fof_nnf,[status(thm)],[big2_induction]) ).
fof(sk_big2_induction_sk,plain,
( ! [X10,X11,X12,X13,X14] : i(triple(X11,X12,X14)) = i(triple(X10,X12,X13))
| ( i(triple(sK8,insert_slb(sK9,pair(sK10,sK11)),sK12)) != i(triple(sK13,insert_slb(sK9,pair(sK10,sK11)),sK14))
& ! [Z,X1,X2,X3] : i(triple(X1,sK9,X3)) = i(triple(Z,sK9,X2)) )
| i(triple(sK4,create_slb,sK5)) != i(triple(sK6,create_slb,sK7)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5,sK6,sK7,sK9,sK8,sK10,sK11,sK12,sK13,sK14]),skolemize(U,sK6),skolemize(V,sK4),skolemize(W,sK7),skolemize(X,sK5),skolemize(Y,sK9),skolemize(X4,sK13),skolemize(X5,sK8),skolemize(X6,sK14),skolemize(X7,sK12),skolemize(X8,sK10),skolemize(X9,sK11)],[nnf_61]) ).
fof(sk_big2_induction,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( i(triple(VAR_0,VAR_1,VAR_2)) = i(triple(VAR_3,VAR_1,VAR_4))
| i(triple(sK8,insert_slb(sK9,pair(sK10,sK11)),sK12)) != i(triple(sK13,insert_slb(sK9,pair(sK10,sK11)),sK14))
| i(triple(sK4,create_slb,sK5)) != i(triple(sK6,create_slb,sK7)) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_8] :
( i(triple(VAR_4,VAR_5,VAR_6)) = i(triple(VAR_7,VAR_5,VAR_8))
| i(triple(VAR_0,sK9,VAR_1)) = i(triple(VAR_2,sK9,VAR_3))
| i(triple(sK4,create_slb,sK5)) != i(triple(sK6,create_slb,sK7)) ) ),
inference(cnf_transformation,[status(thm)],[sk_big2_induction_sk]) ).
cnf(c_134,plain,
( i(triple(A,B,C)) = i(triple(D,B,E))
| i(triple(sK8,insert_slb(sK9,pair(sK10,sK11)),sK12)) != i(triple(sK13,insert_slb(sK9,pair(sK10,sK11)),sK14))
| i(triple(sK4,create_slb,sK5)) != i(triple(sK6,create_slb,sK7)) ),
inference(split_conjunct,[status(thm)],[sk_big2_induction]) ).
cnf(c_135,plain,
( i(triple(E,F,V6)) = i(triple(V7,F,V8))
| i(triple(A,sK9,B)) = i(triple(C,sK9,D))
| i(triple(sK4,create_slb,sK5)) != i(triple(sK6,create_slb,sK7)) ),
inference(split_conjunct,[status(thm)],[sk_big2_induction]) ).
cnf(c_137,plain,
i(triple(A,insert_slb(B,pair(C,D)),E)) = insert_pq(i(triple(A,B,E)),C),
inference(clausify,[status(thm)],[ax55]) ).
cnf(c_138,plain,
i(triple(A,create_slb,B)) = create_pq,
inference(clausify,[status(thm)],[ax54]) ).
cnf(c_152,plain,
triple(insert_pqp(A,B),insert_slb(C,pair(B,bottom)),D) = insert_cpq(triple(A,C,D),B),
inference(clausify,[status(thm)],[ax42]) ).
cnf(c_629,plain,
( i(triple(A,sK9,B)) = i(triple(C,sK9,D))
| i(triple(sK4,create_slb,sK5)) != i(triple(sK6,create_slb,sK7)) ),
inference(factor,[status(thm)],[c_135]) ).
cnf(c_630,plain,
( i(triple(A,sK9,B)) = i(triple(C,sK9,D))
| create_pq != i(triple(sK6,create_slb,sK7)) ),
inference(paramod,[status(thm)],[c_138,c_629]) ).
cnf(c_631,plain,
( i(triple(A,sK9,B)) = i(triple(C,sK9,D))
| create_pq != create_pq ),
inference(paramod,[status(thm)],[c_138,c_630]) ).
cnf(c_203,plain,
i(triple(A,sK9,B)) = i(triple(C,sK9,D)),
inference(copy,[status(thm)],[c_631]) ).
cnf(c_632,plain,
( i(triple(A,B,C)) = i(triple(D,B,E))
| i(triple(sK8,insert_slb(sK9,pair(sK10,sK11)),sK12)) != i(triple(sK13,insert_slb(sK9,pair(sK10,sK11)),sK14))
| create_pq != i(triple(sK6,create_slb,sK7)) ),
inference(paramod,[status(thm)],[c_138,c_134]) ).
cnf(c_633,plain,
( i(triple(A,B,C)) = i(triple(D,B,E))
| i(triple(sK8,insert_slb(sK9,pair(sK10,sK11)),sK12)) != i(triple(sK13,insert_slb(sK9,pair(sK10,sK11)),sK14))
| create_pq != create_pq ),
inference(paramod,[status(thm)],[c_138,c_632]) ).
cnf(c_634,plain,
( i(triple(A,B,C)) = i(triple(D,B,E))
| insert_pq(i(triple(sK8,sK9,sK12)),sK10) != i(triple(sK13,insert_slb(sK9,pair(sK10,sK11)),sK14))
| create_pq != create_pq ),
inference(paramod,[status(thm)],[c_137,c_633]) ).
cnf(c_635,plain,
( i(triple(A,B,C)) = i(triple(D,B,E))
| insert_pq(i(triple(sK8,sK9,sK12)),sK10) != insert_pq(i(triple(sK13,sK9,sK14)),sK10)
| create_pq != create_pq ),
inference(paramod,[status(thm)],[c_137,c_634]) ).
cnf(c_204,plain,
( i(triple(A,B,C)) = i(triple(D,B,E))
| insert_pq(i(triple(sK8,sK9,sK12)),sK10) != insert_pq(i(triple(sK13,sK9,sK14)),sK10) ),
inference(copy,[status(thm)],[c_635]) ).
cnf(c_636,plain,
i(insert_cpq(triple(A,B,C),D)) = insert_pq(i(triple(insert_pqp(A,D),B,C)),D),
inference(paramod,[status(thm)],[c_152,c_137]) ).
cnf(c_214,plain,
insert_pq(i(triple(insert_pqp(A,B),C,D)),B) = i(insert_cpq(triple(A,C,D),B)),
inference(copy,[status(thm)],[c_636]) ).
cnf(c_637,plain,
i(triple(A,insert_slb(sK9,pair(B,C)),D)) = insert_pq(i(triple(E,sK9,F)),B),
inference(paramod,[status(thm)],[c_203,c_137]) ).
cnf(c_291,plain,
insert_pq(i(triple(A,sK9,B)),C) = insert_pq(i(triple(D,sK9,E)),C),
inference(paramod,[status(thm)],[c_137,c_637]) ).
cnf(c_292,plain,
i(triple(A,B,C)) = i(triple(D,B,E)),
inference(resolve,[status(thm)],[c_291,c_204]) ).
cnf(c_627,plain,
i(insert_cpq(triple(sK0,sK1,sK2),sK3)) != insert_pq(i(triple(A,sK1,B)),sK3),
inference(paramod,[status(thm)],[c_292,c_133]) ).
cnf(c_638,plain,
i(insert_cpq(triple(A,C,D),B)) = insert_pq(i(triple(insert_pqp(A,B),C,D)),B),
inference(copy,[status(thm)],[c_214]) ).
cnf(c_628,plain,
$false,
inference(resolve,[status(thm)],[c_627,c_638]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV415+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n020.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 26 13:43:04 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.35 % Process 1710262 was started by sandbox on n020,
% 0.09/0.35 % Sat Sep 26 13:43:04 2026
% 0.09/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.37
% 0.09/0.37 % From the command line: assign(max_seconds, 300).
% 1.09/0.57
% 1.09/0.57 % SZS status Theorem for theBenchmark
% 1.09/0.57
% 1.09/0.57 % Proof 1 at 0.12 (+ 0.03) seconds.
% 1.09/0.57 % Length of proof is 18.
% 1.09/0.57 % Level of proof is 6.
% 1.09/0.57 % Maximum clause weight is 66.000.
% 1.09/0.57 % Given clauses 191.
% 1.09/0.57
% 1.09/0.57 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------