%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SCT105+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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:06:56 PM UTC 2026
% Result : Theorem 0.14s 0.44s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 2
% Syntax : Number of formulae : 45 ( 8 unt; 1 def)
% Number of atoms : 180 ( 29 equ)
% Maximal formula atoms : 12 ( 4 avg)
% Number of connectives : 215 ( 80 ~; 90 |; 36 &)
% ( 3 <=>; 4 =>; 0 <=; 2 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 2 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-4 aty)
% Number of variables : 51 ( 45 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f523,conjecture,
( ( ! [B_x,B_y] :
( B_x != B_y
=> ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_y),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_y,B_x),v_L) ) )
& ! [B_x] : ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_x),v_L)
& c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L) )
<=> ( ! [B_x,B_y] :
( B_x != B_y
=> ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_y,B_x),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_y),v_L) ) )
& ! [B_x] : ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_x),v_L)
& c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f524,negated_conjecture,
~ ( ( ! [B_x,B_y] :
( B_x != B_y
=> ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_y),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_y,B_x),v_L) ) )
& ! [B_x] : ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_x),v_L)
& c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L) )
<=> ( ! [B_x,B_y] :
( B_x != B_y
=> ( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_y,B_x),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_y),v_L) ) )
& ! [B_x] : ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_x),v_L)
& c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L) ) ),
inference(negated_conjecture,[status(cth)],[f523]) ).
fof(f2076,plain,
( ( ! [B_x,B_y] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_y),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_y,B_x),v_L)
| B_x = B_y )
& ! [B_x] : ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_x),v_L)
& c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L) )
<~> ( ! [B_x,B_y] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_y,B_x),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_y),v_L)
| B_x = B_y )
& ! [B_x] : ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_x),v_L)
& c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L) ) ),
inference(pre_NNF_transformation,[status(thm)],[f524]) ).
fof(f2077,definition,
( sP6_prd
<=> ( ! [B_x,B_y] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_y),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_y,B_x),v_L)
| B_x = B_y )
& ! [B_x] : ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_x),v_L)
& c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L) ) ),
introduced(definition,[new_symbols(definition,[sP6_prd])],[]) ).
fof(f2078,plain,
( sP6_prd
<~> ( ! [B_x,B_y] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_y,B_x),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_y),v_L)
| B_x = B_y )
& ! [B_x] : ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_x),v_L)
& c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L) ) ),
inference(formula_renaming,[status(thm)],[f2076,f2077]) ).
fof(f2079,plain,
( ( ? [B_x,B_y] :
( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_y,B_x),v_L)
& ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_y),v_L)
& B_x != B_y )
| ? [B_x] : c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_x),v_L)
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L)
| ~ sP6_prd )
& ( ( ! [B_x,B_y] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_y,B_x),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_y),v_L)
| B_x = B_y )
& ! [B_x] : ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_x),v_L)
& c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L) )
| sP6_prd ) ),
inference(NNF_transformation,[status(thm)],[f2078]) ).
fof(f2080,plain,
( ( ( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK88_skl,sK87_skl),v_L)
& ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK87_skl,sK88_skl),v_L)
& sK87_skl != sK88_skl )
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK86_skl,sK86_skl),v_L)
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L)
| ~ sP6_prd )
& ( ( ! [B_x,B_y] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_y,B_x),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_y),v_L)
| B_x = B_y )
& ! [B_x] : ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_x),v_L)
& c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L) )
| sP6_prd ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK86_skl,sK87_skl,sK88_skl]),skolemize(B_x,sK86_skl),skolemize(B_x,sK87_skl),skolemize(B_y,sK88_skl)],[f2079]) ).
fof(f2081,plain,
( c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L)
| sP6_prd ),
inference(cnf_transformation,[status(thm)],[f2080]) ).
fof(f2082,plain,
! [X0] :
( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X0),v_L)
| sP6_prd ),
inference(cnf_transformation,[status(thm)],[f2080]) ).
fof(f2083,plain,
! [X0,X1] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X0),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),v_L)
| X0 = X1
| sP6_prd ),
inference(cnf_transformation,[status(thm)],[f2080]) ).
fof(f2084,plain,
( sK87_skl != sK88_skl
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK86_skl,sK86_skl),v_L)
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L)
| ~ sP6_prd ),
inference(cnf_transformation,[status(thm)],[f2080]) ).
fof(f2085,plain,
( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK87_skl,sK88_skl),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK86_skl,sK86_skl),v_L)
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L)
| ~ sP6_prd ),
inference(cnf_transformation,[status(thm)],[f2080]) ).
fof(f2086,plain,
( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK88_skl,sK87_skl),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK86_skl,sK86_skl),v_L)
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L)
| ~ sP6_prd ),
inference(cnf_transformation,[status(thm)],[f2080]) ).
fof(f2124,plain,
( ( ? [B_x,B_y] :
( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_y),v_L)
& ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_y,B_x),v_L)
& B_x != B_y )
| ? [B_x] : c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_x),v_L)
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L)
| sP6_prd )
& ( ( ! [B_x,B_y] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_y),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_y,B_x),v_L)
| B_x = B_y )
& ! [B_x] : ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_x),v_L)
& c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L) )
| ~ sP6_prd ) ),
inference(NNF_transformation,[status(thm)],[f2077]) ).
fof(f2125,plain,
( ( ( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK92_skl,sK93_skl),v_L)
& ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK93_skl,sK92_skl),v_L)
& sK92_skl != sK93_skl )
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK91_skl,sK91_skl),v_L)
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L)
| sP6_prd )
& ( ( ! [B_x,B_y] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_y),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_y,B_x),v_L)
| B_x = B_y )
& ! [B_x] : ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,B_x,B_x),v_L)
& c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L) )
| ~ sP6_prd ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK91_skl,sK92_skl,sK93_skl]),skolemize(B_x,sK91_skl),skolemize(B_x,sK92_skl),skolemize(B_y,sK93_skl)],[f2124]) ).
fof(f2126,plain,
( c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L)
| ~ sP6_prd ),
inference(cnf_transformation,[status(thm)],[f2125]) ).
fof(f2127,plain,
! [X0] :
( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X0),v_L)
| ~ sP6_prd ),
inference(cnf_transformation,[status(thm)],[f2125]) ).
fof(f2128,plain,
! [X0,X1] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X0),v_L)
| X0 = X1
| ~ sP6_prd ),
inference(cnf_transformation,[status(thm)],[f2125]) ).
fof(f2129,plain,
( sK92_skl != sK93_skl
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK91_skl,sK91_skl),v_L)
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L)
| sP6_prd ),
inference(cnf_transformation,[status(thm)],[f2125]) ).
fof(f2130,plain,
( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK93_skl,sK92_skl),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK91_skl,sK91_skl),v_L)
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L)
| sP6_prd ),
inference(cnf_transformation,[status(thm)],[f2125]) ).
fof(f2131,plain,
( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK92_skl,sK93_skl),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK91_skl,sK91_skl),v_L)
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L)
| sP6_prd ),
inference(cnf_transformation,[status(thm)],[f2125]) ).
fof(f2193,plain,
c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L),
inference(forward_subsumption_resolution,[status(thm)],[f2126,f2081]) ).
fof(f2208,plain,
! [X0] : ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X0),v_L),
inference(forward_subsumption_resolution,[status(thm)],[f2127,f2082]) ).
fof(f2212,plain,
( sK87_skl != sK88_skl
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK86_skl,sK86_skl),v_L)
| ~ sP6_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f2084,f2193]) ).
fof(f2213,plain,
( sK87_skl != sK88_skl
| ~ sP6_prd ),
inference(resolution,[status(thm)],[f2212,f2208]) ).
fof(f2215,plain,
( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK87_skl,sK88_skl),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK86_skl,sK86_skl),v_L)
| ~ sP6_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f2085,f2193]) ).
fof(f2219,plain,
( sK92_skl != sK93_skl
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK91_skl,sK91_skl),v_L)
| sP6_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f2129,f2193]) ).
fof(f2220,plain,
( sK92_skl != sK93_skl
| sP6_prd ),
inference(resolution,[status(thm)],[f2219,f2208]) ).
fof(f2227,plain,
! [X0,X1] :
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X0,X1),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,X1,X0),v_L)
| X0 = X1 ),
inference(forward_subsumption_resolution,[status(thm)],[f2128,f2083]) ).
fof(f2234,plain,
( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK88_skl,sK87_skl),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK86_skl,sK86_skl),v_L)
| ~ sP6_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f2086,f2193]) ).
fof(f2235,plain,
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK87_skl,sK88_skl),v_L)
| sK87_skl = sK88_skl
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK86_skl,sK86_skl),v_L)
| ~ sP6_prd ),
inference(resolution,[status(thm)],[f2234,f2227]) ).
fof(f2237,plain,
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK87_skl,sK88_skl),v_L)
| sK87_skl = sK88_skl
| ~ sP6_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f2235,f2208]) ).
fof(f2239,plain,
( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK93_skl,sK92_skl),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK91_skl,sK91_skl),v_L)
| sP6_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f2130,f2193]) ).
fof(f2246,plain,
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK86_skl,sK86_skl),v_L)
| ~ sP6_prd ),
inference(backward_subsumption_resolution,[status(thm)],[f2215,f2247]) ).
fof(f2247,plain,
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK87_skl,sK88_skl),v_L)
| ~ sP6_prd ),
inference(forward_subsumption_resolution,[status(thm)],[f2237,f2213]) ).
fof(f2250,plain,
~ sP6_prd,
inference(forward_subsumption_resolution,[status(thm)],[f2246,f2208]) ).
fof(f2252,plain,
( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK93_skl,sK92_skl),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK91_skl,sK91_skl),v_L) ),
inference(backward_subsumption_resolution,[status(thm)],[f2239,f2250]) ).
fof(f2253,plain,
sK92_skl != sK93_skl,
inference(backward_subsumption_resolution,[status(thm)],[f2220,f2250]) ).
fof(f2254,plain,
~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK93_skl,sK92_skl),v_L),
inference(forward_subsumption_resolution,[status(thm)],[f2252,f2208]) ).
fof(f2255,plain,
( ~ c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK92_skl,sK93_skl),v_L)
| c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK91_skl,sK91_skl),v_L)
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L) ),
inference(forward_subsumption_resolution,[status(thm)],[f2131,f2250]) ).
fof(f2261,plain,
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK92_skl,sK93_skl),v_L)
| sK92_skl = sK93_skl ),
inference(resolution,[status(thm)],[f2254,f2227]) ).
fof(f2263,plain,
c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK92_skl,sK93_skl),v_L),
inference(forward_subsumption_resolution,[status(thm)],[f2261,f2253]) ).
fof(f2265,plain,
( c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK91_skl,sK91_skl),v_L)
| ~ c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L) ),
inference(backward_subsumption_resolution,[status(thm)],[f2255,f2263]) ).
fof(f2268,plain,
c_member(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Product__Type_OPair(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt,sK91_skl,sK91_skl),v_L),
inference(forward_subsumption_resolution,[status(thm)],[f2265,f2193]) ).
fof(f2270,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f2268,f2208]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SCT105+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n003.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 04:33:31 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.14/0.41 % Drodi V4.1.1
% 0.14/0.44 % Refutation found
% 0.14/0.44 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.44 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.50 % Elapsed time: 0.129452 seconds
% 0.14/0.50 % CPU time: 0.329082 seconds
% 0.14/0.50 % Total memory used: 149.371 MB
% 0.14/0.50 % Net memory used: 148.706 MB
%------------------------------------------------------------------------------