%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV415+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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:50:44 PM UTC 2026
% Result : Theorem 13.49s 2.14s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV415+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n014.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 : Mon Sep 21 08:45:20 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 13.49/2.14 % Refutation found
% 13.49/2.14 % SZS status Theorem for theBenchmark: Theorem is valid
% 13.49/2.14 % SZS output start CNFRefutation for theBenchmark
% 13.49/2.14 fof(f5,axiom,(
% 13.49/2.14 (! [U] : less_than(bottom,U) )),
% 13.49/2.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.49/2.14 fof(f42,axiom,(
% 13.49/2.14 (! [U,V,W,X] : insert_cpq(triple(U,V,W),X) = triple(insert_pqp(U,X),insert_slb(V,pair(X,bottom)),W) )),
% 13.49/2.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.49/2.14 fof(f54,axiom,(
% 13.49/2.14 (! [U,V] : i(triple(U,create_slb,V)) = create_pq )),
% 13.49/2.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.49/2.14 fof(f55,axiom,(
% 13.49/2.14 (! [U,V,W,X,Y] : i(triple(U,insert_slb(V,pair(X,Y)),W)) = insert_pq(i(triple(U,V,W)),X) )),
% 13.49/2.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.49/2.14 fof(f63,axiom,(
% 13.49/2.14 ( ( (! [U,V,W,X] : i(triple(U,create_slb,W)) = i(triple(V,create_slb,X)))& (! [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)) )) ))=> (! [X10,X11,X12,X13,X14] : i(triple(X10,X12,X13)) = i(triple(X11,X12,X14)) )) ),
% 13.49/2.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.49/2.14 fof(f64,conjecture,(
% 13.49/2.14 (! [U,V,W,X] : i(insert_cpq(triple(U,V,W),X)) = insert_pq(i(triple(U,V,W)),X) )),
% 13.49/2.14 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 13.49/2.14 fof(f65,negated_conjecture,(
% 13.49/2.14 ~((! [U,V,W,X] : i(insert_cpq(triple(U,V,W),X)) = insert_pq(i(triple(U,V,W)),X) ))),
% 13.49/2.14 inference(negated_conjecture,[status(cth)],[f64])).
% 13.49/2.14 fof(f76,plain,(
% 13.49/2.14 ![X0]: (less_than(bottom,X0))),
% 13.49/2.14 inference(cnf_transformation,[status(thm)],[f5])).
% 13.49/2.14 fof(f167,plain,(
% 13.49/2.14 ![X0,X1,X2,X3]: (insert_cpq(triple(X0,X1,X2),X3)=triple(insert_pqp(X0,X3),insert_slb(X1,pair(X3,bottom)),X2))),
% 13.49/2.14 inference(cnf_transformation,[status(thm)],[f42])).
% 13.49/2.14 fof(f193,plain,(
% 13.49/2.14 ![X0,X1]: (i(triple(X0,create_slb,X1))=create_pq)),
% 13.49/2.14 inference(cnf_transformation,[status(thm)],[f54])).
% 13.49/2.14 fof(f194,plain,(
% 13.49/2.14 ![X0,X1,X2,X3,X4]: (i(triple(X0,insert_slb(X1,pair(X2,X3)),X4))=insert_pq(i(triple(X0,X1,X4)),X2))),
% 13.49/2.14 inference(cnf_transformation,[status(thm)],[f55])).
% 13.49/2.14 fof(f230,plain,(
% 13.49/2.14 ((?[U,V,W,X]: ~i(triple(U,create_slb,W))=i(triple(V,create_slb,X)))|(?[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))))))|(![X10,X11,X12,X13,X14]: i(triple(X10,X12,X13))=i(triple(X11,X12,X14)))),
% 13.49/2.14 inference(pre_NNF_transformation,[status(thm)],[f63])).
% 13.49/2.14 fof(f231,plain,(
% 13.49/2.14 (~i(triple(sK4_skl,create_slb,sK6_skl))=i(triple(sK5_skl,create_slb,sK7_skl))|((![Z,X1,X2,X3]: i(triple(Z,sK8_skl,X2))=i(triple(X1,sK8_skl,X3)))&~i(triple(sK9_skl,insert_slb(sK8_skl,pair(sK13_skl,sK14_skl)),sK11_skl))=i(triple(sK10_skl,insert_slb(sK8_skl,pair(sK13_skl,sK14_skl)),sK12_skl))))|(![X10,X11,X12,X13,X14]: i(triple(X10,X12,X13))=i(triple(X11,X12,X14)))),
% 13.49/2.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl,sK11_skl,sK12_skl,sK13_skl,sK14_skl]),skolemize(U,sK4_skl),skolemize(V,sK5_skl),skolemize(W,sK6_skl),skolemize(X,sK7_skl),skolemize(Y,sK8_skl),skolemize(X4,sK9_skl),skolemize(X5,sK10_skl),skolemize(X6,sK11_skl),skolemize(X7,sK12_skl),skolemize(X8,sK13_skl),skolemize(X9,sK14_skl)],[f230])).
% 13.49/2.14 fof(f232,plain,(
% 13.49/2.14 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~i(triple(sK4_skl,create_slb,sK6_skl))=i(triple(sK5_skl,create_slb,sK7_skl))|i(triple(X0,sK8_skl,X1))=i(triple(X2,sK8_skl,X3))|i(triple(X4,X5,X6))=i(triple(X7,X5,X8)))),
% 13.49/2.14 inference(cnf_transformation,[status(thm)],[f231])).
% 13.49/2.14 fof(f233,plain,(
% 13.49/2.14 ![X0,X1,X2,X3,X4]: (~i(triple(sK4_skl,create_slb,sK6_skl))=i(triple(sK5_skl,create_slb,sK7_skl))|~i(triple(sK9_skl,insert_slb(sK8_skl,pair(sK13_skl,sK14_skl)),sK11_skl))=i(triple(sK10_skl,insert_slb(sK8_skl,pair(sK13_skl,sK14_skl)),sK12_skl))|i(triple(X0,X1,X2))=i(triple(X3,X1,X4)))),
% 13.49/2.14 inference(cnf_transformation,[status(thm)],[f231])).
% 13.49/2.14 fof(f234,plain,(
% 13.49/2.14 (?[U,V,W,X]: ~i(insert_cpq(triple(U,V,W),X))=insert_pq(i(triple(U,V,W)),X))),
% 13.49/2.14 inference(pre_NNF_transformation,[status(thm)],[f65])).
% 13.49/2.14 fof(f235,plain,(
% 13.49/2.14 ~i(insert_cpq(triple(sK15_skl,sK16_skl,sK17_skl),sK18_skl))=insert_pq(i(triple(sK15_skl,sK16_skl,sK17_skl)),sK18_skl)),
% 13.49/2.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl,sK17_skl,sK18_skl]),skolemize(U,sK15_skl),skolemize(V,sK16_skl),skolemize(W,sK17_skl),skolemize(X,sK18_skl)],[f234])).
% 13.49/2.14 fof(f236,plain,(
% 13.49/2.14 ~i(insert_cpq(triple(sK15_skl,sK16_skl,sK17_skl),sK18_skl))=insert_pq(i(triple(sK15_skl,sK16_skl,sK17_skl)),sK18_skl)),
% 13.49/2.14 inference(cnf_transformation,[status(thm)],[f235])).
% 13.49/2.14 fof(f237,definition,(
% 13.49/2.14 sQ0_spl <=> (i(triple(sK4_skl,create_slb,sK6_skl))=i(triple(sK5_skl,create_slb,sK7_skl)))),
% 13.49/2.14 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 13.49/2.14 fof(f239,plain,(
% 13.49/2.14 ~i(triple(sK4_skl,create_slb,sK6_skl))=i(triple(sK5_skl,create_slb,sK7_skl))|sQ0_spl),
% 13.49/2.14 inference(component_clause,[status(thm)],[f237])).
% 13.49/2.14 fof(f240,definition,(
% 13.49/2.14 ![X0,X1,X2,X3]: (sQ1_spl <=> (i(triple(X0,sK8_skl,X1))=i(triple(X2,sK8_skl,X3))))),
% 13.49/2.14 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 13.49/2.14 fof(f241,plain,(
% 13.49/2.14 ![X0,X1,X2,X3]: (i(triple(X0,sK8_skl,X1))=i(triple(X2,sK8_skl,X3))|~sQ1_spl)),
% 13.49/2.14 inference(component_clause,[status(thm)],[f240])).
% 13.49/2.14 fof(f243,definition,(
% 13.49/2.14 ![X4,X5,X6,X7,X8]: (sQ2_spl <=> (i(triple(X4,X5,X6))=i(triple(X7,X5,X8))))),
% 13.49/2.14 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 13.49/2.14 fof(f244,plain,(
% 13.49/2.14 ![X0,X1,X2,X3,X4]: (i(triple(X0,X1,X2))=i(triple(X3,X1,X4))|~sQ2_spl)),
% 13.49/2.14 inference(component_clause,[status(thm)],[f243])).
% 13.49/2.14 fof(f246,plain,(
% 13.49/2.14 ~sQ0_spl|sQ1_spl|sQ2_spl),
% 13.49/2.14 inference(split_clause,[status(thm)],[f232,f237,f240,f243])).
% 13.49/2.14 fof(f247,definition,(
% 13.49/2.14 sQ3_spl <=> (i(triple(sK9_skl,insert_slb(sK8_skl,pair(sK13_skl,sK14_skl)),sK11_skl))=i(triple(sK10_skl,insert_slb(sK8_skl,pair(sK13_skl,sK14_skl)),sK12_skl)))),
% 13.49/2.14 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 13.49/2.14 fof(f249,plain,(
% 13.49/2.14 ~i(triple(sK9_skl,insert_slb(sK8_skl,pair(sK13_skl,sK14_skl)),sK11_skl))=i(triple(sK10_skl,insert_slb(sK8_skl,pair(sK13_skl,sK14_skl)),sK12_skl))|sQ3_spl),
% 13.49/2.14 inference(component_clause,[status(thm)],[f247])).
% 13.49/2.14 fof(f250,plain,(
% 13.49/2.14 ~sQ0_spl|~sQ3_spl|sQ2_spl),
% 13.49/2.14 inference(split_clause,[status(thm)],[f233,f237,f247,f243])).
% 13.49/2.14 fof(f2920,plain,(
% 13.49/2.14 ![X0,X1,X2,X3]: (i(insert_cpq(triple(X0,X1,X2),X3))=insert_pq(i(triple(insert_pqp(X0,X3),X1,X2)),X3))),
% 13.49/2.14 inference(paramodulation,[status(thm)],[f167,f194])).
% 13.49/2.14 fof(f5225,plain,(
% 13.49/2.14 ![X0,X1]: (~i(insert_cpq(triple(sK15_skl,sK16_skl,sK17_skl),sK18_skl))=insert_pq(i(triple(X0,sK16_skl,X1)),sK18_skl)|~sQ2_spl)),
% 13.49/2.14 inference(paramodulation,[status(thm)],[f244,f236])).
% 13.49/2.14 fof(f5246,plain,(
% 13.49/2.14 $false|~sQ2_spl),
% 13.49/2.14 inference(resolution,[status(thm)],[f5225,f2920])).
% 13.49/2.14 fof(f5250,plain,(
% 13.49/2.14 ~sQ2_spl),
% 13.49/2.14 inference(contradiction_clause,[status(thm)],[f5246])).
% 13.49/2.14 fof(f5251,plain,(
% 13.49/2.14 ~create_pq=i(triple(sK5_skl,create_slb,sK7_skl))|sQ0_spl),
% 13.49/2.14 inference(forward_demodulation,[status(thm)],[f193,f239])).
% 13.49/2.14 fof(f5252,plain,(
% 13.49/2.14 ~create_pq=create_pq|sQ0_spl),
% 13.49/2.14 inference(forward_demodulation,[status(thm)],[f193,f5251])).
% 13.49/2.14 fof(f5253,plain,(
% 13.49/2.14 $false|sQ0_spl),
% 13.49/2.14 inference(trivial_equality_resolution,[status(thm)],[f5252])).
% 13.49/2.14 fof(f5254,plain,(
% 13.49/2.14 sQ0_spl),
% 13.49/2.14 inference(contradiction_clause,[status(thm)],[f5253])).
% 13.49/2.14 fof(f5255,plain,(
% 13.49/2.14 ~insert_pq(i(triple(sK9_skl,sK8_skl,sK11_skl)),sK13_skl)=i(triple(sK10_skl,insert_slb(sK8_skl,pair(sK13_skl,sK14_skl)),sK12_skl))|sQ3_spl),
% 13.49/2.14 inference(forward_demodulation,[status(thm)],[f194,f249])).
% 13.49/2.14 fof(f5256,plain,(
% 13.49/2.14 ~insert_pq(i(triple(sK9_skl,sK8_skl,sK11_skl)),sK13_skl)=insert_pq(i(triple(sK10_skl,sK8_skl,sK12_skl)),sK13_skl)|sQ3_spl),
% 13.49/2.14 inference(forward_demodulation,[status(thm)],[f194,f5255])).
% 13.49/2.14 fof(f6535,definition,(
% 13.49/2.14 ![X1]: (sQ14_spl <=> (~less_than(X1,bottom)))),
% 13.49/2.14 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 13.49/2.14 fof(f6536,plain,(
% 13.49/2.14 ![X0]: (~less_than(X0,bottom)|~sQ14_spl)),
% 13.49/2.14 inference(component_clause,[status(thm)],[f6535])).
% 13.49/2.14 fof(f6569,plain,(
% 13.49/2.14 $false|~sQ14_spl),
% 13.49/2.14 inference(resolution,[status(thm)],[f6536,f76])).
% 13.49/2.14 fof(f6591,plain,(
% 13.49/2.14 ~sQ14_spl),
% 13.49/2.14 inference(contradiction_clause,[status(thm)],[f6569])).
% 13.49/2.15 fof(f6621,plain,(
% 13.49/2.15 ![X0,X1]: (~insert_pq(i(triple(X0,sK8_skl,X1)),sK13_skl)=insert_pq(i(triple(sK10_skl,sK8_skl,sK12_skl)),sK13_skl)|sQ3_spl|~sQ1_spl)),
% 13.49/2.15 inference(paramodulation,[status(thm)],[f241,f5256])).
% 13.49/2.15 fof(f6739,plain,(
% 13.49/2.15 $false|sQ3_spl|~sQ1_spl),
% 13.49/2.15 inference(equality_resolution,[status(thm)],[f6621])).
% 13.49/2.15 fof(f6740,plain,(
% 13.49/2.15 sQ3_spl|~sQ1_spl),
% 13.49/2.15 inference(contradiction_clause,[status(thm)],[f6739])).
% 13.49/2.15 fof(f6741,plain,(
% 13.49/2.15 $false),
% 13.49/2.15 inference(sat_refutation,[status(thm)],[f246,f250,f5250,f5254,f6591,f6740])).
% 13.49/2.15 % SZS output end CNFRefutation for theBenchmark.p
% 13.49/2.18 % Elapsed time: 1.802192 seconds
% 13.49/2.18 % CPU time: 13.854042 seconds
% 13.49/2.18 % Total memory used: 146.572 MB
% 13.49/2.18 % Net memory used: 143.821 MB
%------------------------------------------------------------------------------