%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : ALG023+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/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 : Thu Sep 24 11:47:47 AM UTC 2026
% Result : Unsatisfiable 0.10s 0.43s
% Output : CNFRefutation 0.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 12
% Syntax : Number of formulae : 127 ( 32 unt; 3 def)
% Number of atoms : 509 ( 415 equ)
% Maximal formula atoms : 64 ( 4 avg)
% Number of connectives : 516 ( 134 ~; 194 |; 183 &)
% ( 5 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 64 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 4 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 0 ( 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( ( op(e3,e3) = e3
| op(e3,e3) = e2
| op(e3,e3) = e1
| op(e3,e3) = e0 )
& ( op(e3,e2) = e3
| op(e3,e2) = e2
| op(e3,e2) = e1
| op(e3,e2) = e0 )
& ( op(e3,e1) = e3
| op(e3,e1) = e2
| op(e3,e1) = e1
| op(e3,e1) = e0 )
& ( op(e3,e0) = e3
| op(e3,e0) = e2
| op(e3,e0) = e1
| op(e3,e0) = e0 )
& ( op(e2,e3) = e3
| op(e2,e3) = e2
| op(e2,e3) = e1
| op(e2,e3) = e0 )
& ( op(e2,e2) = e3
| op(e2,e2) = e2
| op(e2,e2) = e1
| op(e2,e2) = e0 )
& ( op(e2,e1) = e3
| op(e2,e1) = e2
| op(e2,e1) = e1
| op(e2,e1) = e0 )
& ( op(e2,e0) = e3
| op(e2,e0) = e2
| op(e2,e0) = e1
| op(e2,e0) = e0 )
& ( op(e1,e3) = e3
| op(e1,e3) = e2
| op(e1,e3) = e1
| op(e1,e3) = e0 )
& ( op(e1,e2) = e3
| op(e1,e2) = e2
| op(e1,e2) = e1
| op(e1,e2) = e0 )
& ( op(e1,e1) = e3
| op(e1,e1) = e2
| op(e1,e1) = e1
| op(e1,e1) = e0 )
& ( op(e1,e0) = e3
| op(e1,e0) = e2
| op(e1,e0) = e1
| op(e1,e0) = e0 )
& ( op(e0,e3) = e3
| op(e0,e3) = e2
| op(e0,e3) = e1
| op(e0,e3) = e0 )
& ( op(e0,e2) = e3
| op(e0,e2) = e2
| op(e0,e2) = e1
| op(e0,e2) = e0 )
& ( op(e0,e1) = e3
| op(e0,e1) = e2
| op(e0,e1) = e1
| op(e0,e1) = e0 )
& ( op(e0,e0) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e0,e0) = e0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
( op(op(e3,e3),e3) = op(e3,op(e3,e3))
& op(op(e3,e3),e2) = op(e3,op(e3,e2))
& op(op(e3,e3),e1) = op(e3,op(e3,e1))
& op(op(e3,e3),e0) = op(e3,op(e3,e0))
& op(op(e3,e2),e3) = op(e3,op(e2,e3))
& op(op(e3,e2),e2) = op(e3,op(e2,e2))
& op(op(e3,e2),e1) = op(e3,op(e2,e1))
& op(op(e3,e2),e0) = op(e3,op(e2,e0))
& op(op(e3,e1),e3) = op(e3,op(e1,e3))
& op(op(e3,e1),e2) = op(e3,op(e1,e2))
& op(op(e3,e1),e1) = op(e3,op(e1,e1))
& op(op(e3,e1),e0) = op(e3,op(e1,e0))
& op(op(e3,e0),e3) = op(e3,op(e0,e3))
& op(op(e3,e0),e2) = op(e3,op(e0,e2))
& op(op(e3,e0),e1) = op(e3,op(e0,e1))
& op(op(e3,e0),e0) = op(e3,op(e0,e0))
& op(op(e2,e3),e3) = op(e2,op(e3,e3))
& op(op(e2,e3),e2) = op(e2,op(e3,e2))
& op(op(e2,e3),e1) = op(e2,op(e3,e1))
& op(op(e2,e3),e0) = op(e2,op(e3,e0))
& op(op(e2,e2),e3) = op(e2,op(e2,e3))
& op(op(e2,e2),e2) = op(e2,op(e2,e2))
& op(op(e2,e2),e1) = op(e2,op(e2,e1))
& op(op(e2,e2),e0) = op(e2,op(e2,e0))
& op(op(e2,e1),e3) = op(e2,op(e1,e3))
& op(op(e2,e1),e2) = op(e2,op(e1,e2))
& op(op(e2,e1),e1) = op(e2,op(e1,e1))
& op(op(e2,e1),e0) = op(e2,op(e1,e0))
& op(op(e2,e0),e3) = op(e2,op(e0,e3))
& op(op(e2,e0),e2) = op(e2,op(e0,e2))
& op(op(e2,e0),e1) = op(e2,op(e0,e1))
& op(op(e2,e0),e0) = op(e2,op(e0,e0))
& op(op(e1,e3),e3) = op(e1,op(e3,e3))
& op(op(e1,e3),e2) = op(e1,op(e3,e2))
& op(op(e1,e3),e1) = op(e1,op(e3,e1))
& op(op(e1,e3),e0) = op(e1,op(e3,e0))
& op(op(e1,e2),e3) = op(e1,op(e2,e3))
& op(op(e1,e2),e2) = op(e1,op(e2,e2))
& op(op(e1,e2),e1) = op(e1,op(e2,e1))
& op(op(e1,e2),e0) = op(e1,op(e2,e0))
& op(op(e1,e1),e3) = op(e1,op(e1,e3))
& op(op(e1,e1),e2) = op(e1,op(e1,e2))
& op(op(e1,e1),e1) = op(e1,op(e1,e1))
& op(op(e1,e1),e0) = op(e1,op(e1,e0))
& op(op(e1,e0),e3) = op(e1,op(e0,e3))
& op(op(e1,e0),e2) = op(e1,op(e0,e2))
& op(op(e1,e0),e1) = op(e1,op(e0,e1))
& op(op(e1,e0),e0) = op(e1,op(e0,e0))
& op(op(e0,e3),e3) = op(e0,op(e3,e3))
& op(op(e0,e3),e2) = op(e0,op(e3,e2))
& op(op(e0,e3),e1) = op(e0,op(e3,e1))
& op(op(e0,e3),e0) = op(e0,op(e3,e0))
& op(op(e0,e2),e3) = op(e0,op(e2,e3))
& op(op(e0,e2),e2) = op(e0,op(e2,e2))
& op(op(e0,e2),e1) = op(e0,op(e2,e1))
& op(op(e0,e2),e0) = op(e0,op(e2,e0))
& op(op(e0,e1),e3) = op(e0,op(e1,e3))
& op(op(e0,e1),e2) = op(e0,op(e1,e2))
& op(op(e0,e1),e1) = op(e0,op(e1,e1))
& op(op(e0,e1),e0) = op(e0,op(e1,e0))
& op(op(e0,e0),e3) = op(e0,op(e0,e3))
& op(op(e0,e0),e2) = op(e0,op(e0,e2))
& op(op(e0,e0),e1) = op(e0,op(e0,e1))
& op(op(e0,e0),e0) = op(e0,op(e0,e0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
( op(e3,e2) != op(e3,e3)
& op(e3,e1) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e1)
& op(e2,e2) != op(e2,e3)
& op(e2,e1) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e1)
& op(e1,e2) != op(e1,e3)
& op(e1,e1) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e1)
& op(e0,e2) != op(e0,e3)
& op(e0,e1) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e1)
& op(e2,e3) != op(e3,e3)
& op(e1,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e1,e3)
& op(e2,e2) != op(e3,e2)
& op(e1,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e1,e2)
& op(e2,e1) != op(e3,e1)
& op(e1,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e1,e1)
& op(e2,e0) != op(e3,e0)
& op(e1,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e1,e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
( ( op(e3,e3) = e3
& op(e2,e2) = e3
& op(e1,e1) = e3
& op(e0,e0) = e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e2
& op(e1,e1) = e2
& op(e0,e0) = e2 )
| ( op(e3,e3) = e1
& op(e2,e2) = e1
& op(e1,e1) = e1
& op(e0,e0) = e1 )
| ( op(e3,e3) = e0
& op(e2,e2) = e0
& op(e1,e1) = e0
& op(e0,e0) = e0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
~ ( e2 = op(e1,e3)
& e0 = op(e3,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
~ ( e0 = op(e2,e3)
& e1 = op(e3,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
~ ( e3 = op(e2,e0)
& e1 = op(e0,e0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
~ ( e0 = op(e1,e3)
& e2 = op(e3,e3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
~ ( e1 = op(e0,e2)
& e3 = op(e2,e2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,plain,
( op(e0,e2) = e3
| op(e0,e2) = e2
| op(e0,e2) = e1
| op(e0,e2) = e0 ),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f43,plain,
( op(e1,e3) = e3
| op(e1,e3) = e2
| op(e1,e3) = e1
| op(e1,e3) = e0 ),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f44,plain,
( op(e2,e0) = e3
| op(e2,e0) = e2
| op(e2,e0) = e1
| op(e2,e0) = e0 ),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f47,plain,
( op(e2,e3) = e3
| op(e2,e3) = e2
| op(e2,e3) = e1
| op(e2,e3) = e0 ),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f54,plain,
op(op(e0,e0),e2) = op(e0,op(e0,e2)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f75,plain,
op(op(e1,e1),e3) = op(e1,op(e1,e3)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f92,plain,
op(op(e2,e2),e0) = op(e2,op(e2,e0)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f95,plain,
op(op(e2,e2),e3) = op(e2,op(e2,e3)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f115,plain,
op(op(e3,e3),e3) = op(e3,op(e3,e3)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f166,plain,
op(e0,e0) != op(e2,e0),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f168,plain,
op(e1,e0) != op(e2,e0),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f178,plain,
op(e0,e2) != op(e2,e2),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f179,plain,
op(e0,e2) != op(e3,e2),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f183,plain,
op(e0,e3) != op(e1,e3),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f186,plain,
op(e1,e3) != op(e2,e3),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f187,plain,
op(e1,e3) != op(e3,e3),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f188,plain,
op(e2,e3) != op(e3,e3),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f203,plain,
op(e2,e0) != op(e2,e3),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f209,plain,
op(e3,e0) != op(e3,e3),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f212,plain,
op(e3,e2) != op(e3,e3),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f219,definition,
( sP0_prd
<=> ( ( op(e3,e3) = e2
& op(e2,e2) = e2
& op(e1,e1) = e2
& op(e0,e0) = e2 )
| ( op(e3,e3) = e1
& op(e2,e2) = e1
& op(e1,e1) = e1
& op(e0,e0) = e1 )
| ( op(e3,e3) = e0
& op(e2,e2) = e0
& op(e1,e1) = e0
& op(e0,e0) = e0 ) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f220,plain,
( ( op(e3,e3) = e3
& op(e2,e2) = e3
& op(e1,e1) = e3
& op(e0,e0) = e3 )
| sP0_prd ),
inference(formula_renaming,[status(thm)],[f11,f219]) ).
fof(f221,plain,
( op(e0,e0) = e3
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f223,plain,
( op(e2,e2) = e3
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f224,plain,
( op(e3,e3) = e3
| sP0_prd ),
inference(cnf_transformation,[status(thm)],[f220]) ).
fof(f229,plain,
( e2 != op(e1,e3)
| e0 != op(e3,e3) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f230,plain,
( e2 != op(e1,e3)
| e0 != op(e3,e3) ),
inference(cnf_transformation,[status(thm)],[f229]) ).
fof(f237,plain,
( e0 != op(e2,e3)
| e1 != op(e3,e3) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f238,plain,
( e0 != op(e2,e3)
| e1 != op(e3,e3) ),
inference(cnf_transformation,[status(thm)],[f237]) ).
fof(f247,plain,
( e3 != op(e2,e0)
| e1 != op(e0,e0) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f248,plain,
( e3 != op(e2,e0)
| e1 != op(e0,e0) ),
inference(cnf_transformation,[status(thm)],[f247]) ).
fof(f249,plain,
( e0 != op(e1,e3)
| e2 != op(e3,e3) ),
inference(pre_NNF_transformation,[status(thm)],[f24]) ).
fof(f250,plain,
( e0 != op(e1,e3)
| e2 != op(e3,e3) ),
inference(cnf_transformation,[status(thm)],[f249]) ).
fof(f265,plain,
( e1 != op(e0,e2)
| e3 != op(e2,e2) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f266,plain,
( e1 != op(e0,e2)
| e3 != op(e2,e2) ),
inference(cnf_transformation,[status(thm)],[f265]) ).
fof(f273,definition,
( sP1_prd
<=> ( ( op(e3,e3) = e1
& op(e2,e2) = e1
& op(e1,e1) = e1
& op(e0,e0) = e1 )
| ( op(e3,e3) = e0
& op(e2,e2) = e0
& op(e1,e1) = e0
& op(e0,e0) = e0 ) ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f274,plain,
( sP0_prd
<=> ( ( op(e3,e3) = e2
& op(e2,e2) = e2
& op(e1,e1) = e2
& op(e0,e0) = e2 )
| sP1_prd ) ),
inference(formula_renaming,[status(thm)],[f219,f273]) ).
fof(f275,plain,
( ( ( ( op(e3,e3) != e2
| op(e2,e2) != e2
| op(e1,e1) != e2
| op(e0,e0) != e2 )
& ~ sP1_prd )
| sP0_prd )
& ( ( op(e3,e3) = e2
& op(e2,e2) = e2
& op(e1,e1) = e2
& op(e0,e0) = e2 )
| sP1_prd
| ~ sP0_prd ) ),
inference(NNF_transformation,[status(thm)],[f274]) ).
fof(f277,plain,
( op(e1,e1) = e2
| sP1_prd
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f275]) ).
fof(f279,plain,
( op(e3,e3) = e2
| sP1_prd
| ~ sP0_prd ),
inference(cnf_transformation,[status(thm)],[f275]) ).
fof(f282,definition,
( sP2_prd
<=> ( op(e3,e3) = e0
& op(e2,e2) = e0
& op(e1,e1) = e0
& op(e0,e0) = e0 ) ),
introduced(definition,[new_symbols(definition,[sP2_prd])],[]) ).
fof(f283,plain,
( sP1_prd
<=> ( ( op(e3,e3) = e1
& op(e2,e2) = e1
& op(e1,e1) = e1
& op(e0,e0) = e1 )
| sP2_prd ) ),
inference(formula_renaming,[status(thm)],[f273,f282]) ).
fof(f284,plain,
( ( ( ( op(e3,e3) != e1
| op(e2,e2) != e1
| op(e1,e1) != e1
| op(e0,e0) != e1 )
& ~ sP2_prd )
| sP1_prd )
& ( ( op(e3,e3) = e1
& op(e2,e2) = e1
& op(e1,e1) = e1
& op(e0,e0) = e1 )
| sP2_prd
| ~ sP1_prd ) ),
inference(NNF_transformation,[status(thm)],[f283]) ).
fof(f285,plain,
( op(e0,e0) = e1
| sP2_prd
| ~ sP1_prd ),
inference(cnf_transformation,[status(thm)],[f284]) ).
fof(f287,plain,
( op(e2,e2) = e1
| sP2_prd
| ~ sP1_prd ),
inference(cnf_transformation,[status(thm)],[f284]) ).
fof(f288,plain,
( op(e3,e3) = e1
| sP2_prd
| ~ sP1_prd ),
inference(cnf_transformation,[status(thm)],[f284]) ).
fof(f291,plain,
( ( op(e3,e3) != e0
| op(e2,e2) != e0
| op(e1,e1) != e0
| op(e0,e0) != e0
| sP2_prd )
& ( ( op(e3,e3) = e0
& op(e2,e2) = e0
& op(e1,e1) = e0
& op(e0,e0) = e0 )
| ~ sP2_prd ) ),
inference(NNF_transformation,[status(thm)],[f282]) ).
fof(f293,plain,
( op(e1,e1) = e0
| ~ sP2_prd ),
inference(cnf_transformation,[status(thm)],[f291]) ).
fof(f295,plain,
( op(e3,e3) = e0
| ~ sP2_prd ),
inference(cnf_transformation,[status(thm)],[f291]) ).
fof(f373,plain,
( sP0_prd
| op(e3,e2) = op(e0,op(e0,e2)) ),
inference(paramodulation,[status(thm)],[f221,f54]) ).
fof(f375,plain,
( op(e2,e0) = e3
| op(e2,e0) = e2
| op(e2,e0) = e0
| op(e0,e0) != e1 ),
inference(paramodulation,[status(thm)],[f44,f166]) ).
fof(f395,plain,
( sP0_prd
| op(e0,e2) != e3 ),
inference(paramodulation,[status(thm)],[f223,f178]) ).
fof(f477,plain,
( sP0_prd
| op(e3,e2) != e3 ),
inference(paramodulation,[status(thm)],[f224,f212]) ).
fof(f529,plain,
( sP2_prd
| ~ sP1_prd
| e0 != op(e2,e3) ),
inference(resolution,[status(thm)],[f238,f288]) ).
fof(f552,plain,
( sP1_prd
| ~ sP0_prd
| e0 != op(e1,e3) ),
inference(resolution,[status(thm)],[f250,f279]) ).
fof(f597,plain,
( sP0_prd
| e1 != op(e0,e2) ),
inference(resolution,[status(thm)],[f266,f223]) ).
fof(f603,plain,
( op(e0,e2) = e3
| op(e0,e2) = e2
| op(e0,e2) = e0
| sP0_prd ),
inference(resolution,[status(thm)],[f597,f38]) ).
fof(f605,plain,
( op(e0,e2) = e2
| op(e0,e2) = e0
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f603,f395]) ).
fof(f711,plain,
( op(e0,e2) = e0
| sP0_prd
| sP0_prd
| op(e3,e2) = op(e0,e2) ),
inference(paramodulation,[status(thm)],[f605,f373]) ).
fof(f724,plain,
( op(e0,e2) = e0
| sP0_prd
| op(e3,e2) = op(e0,e2) ),
inference(duplicate_literals_removal,[status(thm)],[f711]) ).
fof(f725,plain,
( op(e0,e2) = e0
| sP0_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f724,f179]) ).
fof(f730,plain,
( sP0_prd
| sP0_prd
| op(e3,e2) = op(e0,e0) ),
inference(paramodulation,[status(thm)],[f725,f373]) ).
fof(f741,plain,
( sP0_prd
| op(e3,e2) = op(e0,e0) ),
inference(duplicate_literals_removal,[status(thm)],[f730]) ).
fof(f753,plain,
( sP0_prd
| sP0_prd
| op(e0,e0) != e3 ),
inference(paramodulation,[status(thm)],[f741,f477]) ).
fof(f761,plain,
( sP0_prd
| op(e0,e0) != e3 ),
inference(duplicate_literals_removal,[status(thm)],[f753]) ).
fof(f762,plain,
sP0_prd,
inference(forward_subsumption_resolution,[status(thm)],[f761,f221]) ).
fof(f767,plain,
( sP1_prd
| e0 != op(e1,e3) ),
inference(backward_subsumption_resolution,[status(thm)],[f552,f762]) ).
fof(f768,plain,
( op(e3,e3) = e2
| sP1_prd ),
inference(backward_subsumption_resolution,[status(thm)],[f279,f762]) ).
fof(f770,plain,
( op(e1,e1) = e2
| sP1_prd ),
inference(backward_subsumption_resolution,[status(thm)],[f277,f762]) ).
fof(f792,plain,
( sP1_prd
| op(e2,e3) != e2 ),
inference(paramodulation,[status(thm)],[f768,f188]) ).
fof(f793,plain,
( sP1_prd
| op(e1,e3) != e2 ),
inference(paramodulation,[status(thm)],[f768,f187]) ).
fof(f821,plain,
( sP1_prd
| op(e2,e3) = op(e1,op(e1,e3)) ),
inference(paramodulation,[status(thm)],[f770,f75]) ).
fof(f855,plain,
( op(e1,e3) = e3
| op(e1,e3) = e1
| op(e1,e3) = e0
| sP1_prd ),
inference(resolution,[status(thm)],[f793,f43]) ).
fof(f857,plain,
( op(e1,e3) = e3
| op(e1,e3) = e1
| sP1_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f855,f767]) ).
fof(f1032,plain,
( op(e1,e3) = e1
| sP1_prd
| sP1_prd
| op(e2,e3) = op(e1,e3) ),
inference(paramodulation,[status(thm)],[f857,f821]) ).
fof(f1046,plain,
( op(e1,e3) = e1
| sP1_prd
| op(e2,e3) = op(e1,e3) ),
inference(duplicate_literals_removal,[status(thm)],[f1032]) ).
fof(f1047,plain,
( op(e1,e3) = e1
| sP1_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f1046,f186]) ).
fof(f1051,plain,
( sP1_prd
| sP1_prd
| op(e2,e3) = op(e1,e1) ),
inference(paramodulation,[status(thm)],[f1047,f821]) ).
fof(f1064,plain,
( sP1_prd
| op(e2,e3) = op(e1,e1) ),
inference(duplicate_literals_removal,[status(thm)],[f1051]) ).
fof(f1103,plain,
( sP1_prd
| sP1_prd
| op(e1,e1) != e2 ),
inference(paramodulation,[status(thm)],[f1064,f792]) ).
fof(f1118,plain,
( sP1_prd
| op(e1,e1) != e2 ),
inference(duplicate_literals_removal,[status(thm)],[f1103]) ).
fof(f1119,plain,
sP1_prd,
inference(forward_subsumption_resolution,[status(thm)],[f1118,f770]) ).
fof(f1126,plain,
( sP2_prd
| e0 != op(e2,e3) ),
inference(backward_subsumption_resolution,[status(thm)],[f529,f1119]) ).
fof(f1127,plain,
( op(e3,e3) = e1
| sP2_prd ),
inference(backward_subsumption_resolution,[status(thm)],[f288,f1119]) ).
fof(f1128,plain,
( op(e2,e2) = e1
| sP2_prd ),
inference(backward_subsumption_resolution,[status(thm)],[f287,f1119]) ).
fof(f1130,plain,
( op(e0,e0) = e1
| sP2_prd ),
inference(backward_subsumption_resolution,[status(thm)],[f285,f1119]) ).
fof(f1145,plain,
( sP2_prd
| op(e2,e3) != e1 ),
inference(paramodulation,[status(thm)],[f1127,f188]) ).
fof(f1153,plain,
( sP2_prd
| op(e1,e3) = op(e2,op(e2,e3)) ),
inference(paramodulation,[status(thm)],[f1128,f95]) ).
fof(f1156,plain,
( sP2_prd
| op(e1,e0) = op(e2,op(e2,e0)) ),
inference(paramodulation,[status(thm)],[f1128,f92]) ).
fof(f1206,plain,
( op(e2,e3) = e3
| op(e2,e3) = e2
| op(e2,e3) = e0
| sP2_prd ),
inference(resolution,[status(thm)],[f1145,f47]) ).
fof(f1208,plain,
( op(e2,e3) = e3
| op(e2,e3) = e2
| sP2_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f1206,f1126]) ).
fof(f1247,plain,
( op(e2,e0) = e2
| op(e2,e0) = e0
| op(e0,e0) != e1 ),
inference(forward_subsumption_resolution,[status(thm)],[f375,f248]) ).
fof(f1463,plain,
( op(e2,e3) = e2
| sP2_prd
| sP2_prd
| op(e1,e3) = op(e2,e3) ),
inference(paramodulation,[status(thm)],[f1208,f1153]) ).
fof(f1479,plain,
( op(e2,e3) = e2
| sP2_prd
| op(e1,e3) = op(e2,e3) ),
inference(duplicate_literals_removal,[status(thm)],[f1463]) ).
fof(f1480,plain,
( op(e2,e3) = e2
| sP2_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f1479,f186]) ).
fof(f1495,plain,
( sP2_prd
| op(e2,e0) != e2 ),
inference(paramodulation,[status(thm)],[f1480,f203]) ).
fof(f1521,plain,
( op(e2,e0) = e0
| op(e0,e0) != e1
| sP2_prd ),
inference(resolution,[status(thm)],[f1495,f1247]) ).
fof(f1524,plain,
( op(e2,e0) = e0
| sP2_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f1521,f1130]) ).
fof(f1546,plain,
( sP2_prd
| sP2_prd
| op(e1,e0) = op(e2,e0) ),
inference(paramodulation,[status(thm)],[f1524,f1156]) ).
fof(f1560,plain,
( sP2_prd
| op(e1,e0) = op(e2,e0) ),
inference(duplicate_literals_removal,[status(thm)],[f1546]) ).
fof(f1561,plain,
sP2_prd,
inference(forward_subsumption_resolution,[status(thm)],[f1560,f168]) ).
fof(f1567,plain,
op(e3,e3) = e0,
inference(backward_subsumption_resolution,[status(thm)],[f295,f1561]) ).
fof(f1569,plain,
op(e1,e1) = e0,
inference(backward_subsumption_resolution,[status(thm)],[f293,f1561]) ).
fof(f1571,plain,
op(op(e3,e3),e3) = op(e3,e0),
inference(backward_demodulation,[status(thm)],[f1567,f115]) ).
fof(f1581,plain,
( e2 != op(e1,e3)
| e0 != e0 ),
inference(backward_demodulation,[status(thm)],[f1567,f230]) ).
fof(f1585,plain,
op(e3,e0) != e0,
inference(backward_demodulation,[status(thm)],[f1567,f209]) ).
fof(f1588,plain,
op(e1,e3) != e0,
inference(backward_demodulation,[status(thm)],[f1567,f187]) ).
fof(f1591,plain,
op(e0,e3) = op(e3,e0),
inference(forward_demodulation,[status(thm)],[f1567,f1571]) ).
fof(f1592,plain,
e2 != op(e1,e3),
inference(trivial_equality_resolution,[status(thm)],[f1581]) ).
fof(f1632,plain,
op(e0,e3) = op(e1,op(e1,e3)),
inference(backward_demodulation,[status(thm)],[f1569,f75]) ).
fof(f1676,plain,
( op(e1,e3) = e3
| op(e1,e3) = e1
| op(e1,e3) = e0 ),
inference(backward_subsumption_resolution,[status(thm)],[f43,f1592]) ).
fof(f1706,plain,
op(e0,e3) != e0,
inference(forward_demodulation,[status(thm)],[f1591,f1585]) ).
fof(f1771,plain,
( op(e1,e3) = e3
| op(e1,e3) = e1 ),
inference(forward_subsumption_resolution,[status(thm)],[f1676,f1588]) ).
fof(f1772,plain,
( op(e1,e3) = e1
| op(e0,e3) = op(e1,e3) ),
inference(paramodulation,[status(thm)],[f1771,f1632]) ).
fof(f1781,plain,
op(e1,e3) = e1,
inference(forward_subsumption_resolution,[status(thm)],[f1772,f183]) ).
fof(f1783,plain,
op(e0,e3) = op(e1,e1),
inference(backward_demodulation,[status(thm)],[f1781,f1632]) ).
fof(f1795,plain,
op(e0,e3) = e0,
inference(forward_demodulation,[status(thm)],[f1569,f1783]) ).
fof(f1796,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1795,f1706]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG023+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n020.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 12:54:33 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.10/0.43 % Refutation found
% 0.10/0.43 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.10/0.43 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.10/0.45 % Elapsed time: 0.076887 seconds
% 0.10/0.45 % CPU time: 0.420259 seconds
% 0.10/0.45 % Total memory used: 20.281 MB
% 0.10/0.45 % Net memory used: 19.711 MB
%------------------------------------------------------------------------------