%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ALG226+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /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 : Thu Sep 24 11:49:02 AM UTC 2026
% Result : Theorem 56.12s 16.15s
% Output : CNFRefutation 29.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 3
% Syntax : Number of formulae : 34 ( 14 unt; 0 def)
% Number of atoms : 99 ( 28 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 99 ( 34 ~; 29 |; 23 &)
% ( 2 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 31 ( 28 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8280,axiom,
! [A,B,C] :
( ( m1_pboole(C,A)
& m1_pboole(B,A) )
=> ( r6_pboole(A,B,C)
<=> B = C ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42810,axiom,
! [A] :
( ~ v1_xboole_0(A)
=> ! [B] :
( ( m1_pboole(B,A)
& v2_relat_1(B) )
=> B = k1_funct_4(k1_pboole(A),k7_relat_1(B,k1_closure3(A,B))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42811,conjecture,
! [A] :
( ~ v1_xboole_0(A)
=> ! [B] :
( ( m1_pboole(B,A)
& v2_relat_1(B) )
=> ! [C] :
( ( m1_pboole(C,A)
& v2_relat_1(C) )
=> ( ( k7_relat_1(B,k1_closure3(A,B)) = k7_relat_1(C,k1_closure3(A,C))
& k1_closure3(A,B) = k1_closure3(A,C) )
=> r6_pboole(A,B,C) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42812,negated_conjecture,
~ ! [A] :
( ~ v1_xboole_0(A)
=> ! [B] :
( ( m1_pboole(B,A)
& v2_relat_1(B) )
=> ! [C] :
( ( m1_pboole(C,A)
& v2_relat_1(C) )
=> ( ( k7_relat_1(B,k1_closure3(A,B)) = k7_relat_1(C,k1_closure3(A,C))
& k1_closure3(A,B) = k1_closure3(A,C) )
=> r6_pboole(A,B,C) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f42811]) ).
fof(f66597,plain,
! [A,B,C] :
( ( r6_pboole(A,B,C)
<=> B = C )
| ~ m1_pboole(C,A)
| ~ m1_pboole(B,A) ),
inference(pre_NNF_transformation,[status(thm)],[f8280]) ).
fof(f66598,plain,
! [A,B,C] :
( ( ( B != C
| r6_pboole(A,B,C) )
& ( B = C
| ~ r6_pboole(A,B,C) ) )
| ~ m1_pboole(C,A)
| ~ m1_pboole(B,A) ),
inference(NNF_transformation,[status(thm)],[f66597]) ).
fof(f66600,plain,
! [X0,X1,X2] :
( X0 != X2
| r6_pboole(X1,X0,X2)
| ~ m1_pboole(X2,X1)
| ~ m1_pboole(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f66598]) ).
fof(f195240,plain,
! [A] :
( ! [B] :
( B = k1_funct_4(k1_pboole(A),k7_relat_1(B,k1_closure3(A,B)))
| ~ m1_pboole(B,A)
| ~ v2_relat_1(B) )
| v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f42810]) ).
fof(f195241,plain,
! [X0,X1] :
( X1 = k1_funct_4(k1_pboole(X0),k7_relat_1(X1,k1_closure3(X0,X1)))
| ~ m1_pboole(X1,X0)
| ~ v2_relat_1(X1)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f195240]) ).
fof(f195242,plain,
? [A] :
( ? [B] :
( ? [C] :
( ~ r6_pboole(A,B,C)
& k7_relat_1(B,k1_closure3(A,B)) = k7_relat_1(C,k1_closure3(A,C))
& k1_closure3(A,B) = k1_closure3(A,C)
& m1_pboole(C,A)
& v2_relat_1(C) )
& m1_pboole(B,A)
& v2_relat_1(B) )
& ~ v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f42812]) ).
fof(f195243,plain,
( ~ r6_pboole(sK15195_skl,sK15196_skl,sK15197_skl)
& k7_relat_1(sK15196_skl,k1_closure3(sK15195_skl,sK15196_skl)) = k7_relat_1(sK15197_skl,k1_closure3(sK15195_skl,sK15197_skl))
& k1_closure3(sK15195_skl,sK15196_skl) = k1_closure3(sK15195_skl,sK15197_skl)
& m1_pboole(sK15197_skl,sK15195_skl)
& v2_relat_1(sK15197_skl)
& m1_pboole(sK15196_skl,sK15195_skl)
& v2_relat_1(sK15196_skl)
& ~ v1_xboole_0(sK15195_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15195_skl,sK15196_skl,sK15197_skl]),skolemize(A,sK15195_skl),skolemize(B,sK15196_skl),skolemize(C,sK15197_skl)],[f195242]) ).
fof(f195244,plain,
~ v1_xboole_0(sK15195_skl),
inference(cnf_transformation,[status(thm)],[f195243]) ).
fof(f195245,plain,
v2_relat_1(sK15196_skl),
inference(cnf_transformation,[status(thm)],[f195243]) ).
fof(f195246,plain,
m1_pboole(sK15196_skl,sK15195_skl),
inference(cnf_transformation,[status(thm)],[f195243]) ).
fof(f195247,plain,
v2_relat_1(sK15197_skl),
inference(cnf_transformation,[status(thm)],[f195243]) ).
fof(f195248,plain,
m1_pboole(sK15197_skl,sK15195_skl),
inference(cnf_transformation,[status(thm)],[f195243]) ).
fof(f195249,plain,
k1_closure3(sK15195_skl,sK15196_skl) = k1_closure3(sK15195_skl,sK15197_skl),
inference(cnf_transformation,[status(thm)],[f195243]) ).
fof(f195250,plain,
k7_relat_1(sK15196_skl,k1_closure3(sK15195_skl,sK15196_skl)) = k7_relat_1(sK15197_skl,k1_closure3(sK15195_skl,sK15197_skl)),
inference(cnf_transformation,[status(thm)],[f195243]) ).
fof(f195251,plain,
~ r6_pboole(sK15195_skl,sK15196_skl,sK15197_skl),
inference(cnf_transformation,[status(thm)],[f195243]) ).
fof(f216164,plain,
! [X2,X1] :
( r6_pboole(X1,X2,X2)
| ~ m1_pboole(X2,X1)
| ~ m1_pboole(X2,X1) ),
inference(destructive_equality_resolution,[status(thm)],[f66600]) ).
fof(f216165,plain,
! [X0,X1] :
( r6_pboole(X1,X0,X0)
| ~ m1_pboole(X0,X1) ),
inference(duplicate_literals_removal,[status(thm)],[f216164]) ).
fof(f218453,plain,
k7_relat_1(sK15196_skl,k1_closure3(sK15195_skl,sK15196_skl)) = k7_relat_1(sK15197_skl,k1_closure3(sK15195_skl,sK15196_skl)),
inference(forward_demodulation,[status(thm)],[f195249,f195250]) ).
fof(f225737,plain,
r6_pboole(sK15195_skl,sK15196_skl,sK15196_skl),
inference(resolution,[status(thm)],[f216165,f195246]) ).
fof(f229733,plain,
( sK15197_skl = k1_funct_4(k1_pboole(sK15195_skl),k7_relat_1(sK15197_skl,k1_closure3(sK15195_skl,sK15197_skl)))
| ~ v2_relat_1(sK15197_skl)
| v1_xboole_0(sK15195_skl) ),
inference(resolution,[status(thm)],[f195241,f195248]) ).
fof(f229734,plain,
( sK15196_skl = k1_funct_4(k1_pboole(sK15195_skl),k7_relat_1(sK15196_skl,k1_closure3(sK15195_skl,sK15196_skl)))
| ~ v2_relat_1(sK15196_skl)
| v1_xboole_0(sK15195_skl) ),
inference(resolution,[status(thm)],[f195241,f195246]) ).
fof(f229736,plain,
( sK15197_skl = k1_funct_4(k1_pboole(sK15195_skl),k7_relat_1(sK15197_skl,k1_closure3(sK15195_skl,sK15196_skl)))
| ~ v2_relat_1(sK15197_skl)
| v1_xboole_0(sK15195_skl) ),
inference(forward_demodulation,[status(thm)],[f195249,f229733]) ).
fof(f229737,plain,
( sK15197_skl = k1_funct_4(k1_pboole(sK15195_skl),k7_relat_1(sK15196_skl,k1_closure3(sK15195_skl,sK15196_skl)))
| ~ v2_relat_1(sK15197_skl)
| v1_xboole_0(sK15195_skl) ),
inference(forward_demodulation,[status(thm)],[f218453,f229736]) ).
fof(f229738,plain,
( sK15197_skl = k1_funct_4(k1_pboole(sK15195_skl),k7_relat_1(sK15196_skl,k1_closure3(sK15195_skl,sK15196_skl)))
| ~ v2_relat_1(sK15197_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f229737,f195244]) ).
fof(f229739,plain,
( sK15196_skl = k1_funct_4(k1_pboole(sK15195_skl),k7_relat_1(sK15196_skl,k1_closure3(sK15195_skl,sK15196_skl)))
| ~ v2_relat_1(sK15196_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f229734,f195244]) ).
fof(f229810,plain,
sK15197_skl = k1_funct_4(k1_pboole(sK15195_skl),k7_relat_1(sK15196_skl,k1_closure3(sK15195_skl,sK15196_skl))),
inference(forward_subsumption_resolution,[status(thm)],[f229738,f195247]) ).
fof(f229949,plain,
( sK15196_skl = sK15197_skl
| ~ v2_relat_1(sK15196_skl) ),
inference(forward_demodulation,[status(thm)],[f229810,f229739]) ).
fof(f229984,plain,
~ r6_pboole(sK15195_skl,sK15196_skl,sK15196_skl),
inference(backward_demodulation,[status(thm)],[f229987,f195251]) ).
fof(f229987,plain,
sK15196_skl = sK15197_skl,
inference(forward_subsumption_resolution,[status(thm)],[f229949,f195245]) ).
fof(f230001,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f229984,f225737]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ALG226+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n011.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Mon Sep 21 13:06:31 UTC 2026
% 0.17/0.42 % CPUTime :
% 9.97/10.24 % Drodi V4.1.1
% 56.12/16.15 % Refutation found
% 56.12/16.15 % SZS status Theorem for theBenchmark: Theorem is valid
% 56.12/16.15 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 11.80/17.26 % Elapsed time: 16.683854 seconds
% 11.80/17.26 % CPU time: 57.568547 seconds
% 11.80/17.26 % Total memory used: 12.979 GB
% 11.80/17.26 % Net memory used: 12.868 GB
%------------------------------------------------------------------------------