%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SCT105+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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:07:19 PM UTC 2026
% Result : Theorem 0.17s 5.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT105+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/5.40 % Computer : n017.cluster.edu
% 0.12/5.40 % Model : x86_64 x86_64
% 0.12/5.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.40 % Memory : 8046.5625MB
% 0.12/5.40 % OS : Linux 6.8.0-71-generic
% 0.12/5.40 % CPULimit : 300
% 0.12/5.40 % WCLimit : 300
% 0.12/5.40 % DateTime : Mon Sep 21 04:27:17 UTC 2026
% 0.12/5.41 % CPUTime :
% 0.12/5.49 % Drodi V4.1.1
% 0.17/5.53 % Refutation found
% 0.17/5.53 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/5.53 % SZS output start CNFRefutation for theBenchmark
% 0.17/5.53 fof(f523,conjecture,(
% 0.17/5.53 ( ( c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,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))& (! [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) ) ) ))<=> ( c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,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))& (! [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) ) ) )) ) ),
% 0.17/5.53 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.17/5.53 fof(f524,negated_conjecture,(
% 0.17/5.53 ~(( ( c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,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))& (! [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) ) ) ))<=> ( c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,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))& (! [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) ) ) )) ) )),
% 0.17/5.53 inference(negated_conjecture,[status(cth)],[f523])).
% 0.17/5.53 fof(f2076,plain,(
% 0.17/5.53 (((c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,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)))&(![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)))))<~>((c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,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)))&(![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))))))),
% 0.17/5.53 inference(pre_NNF_transformation,[status(thm)],[f524])).
% 0.17/5.53 fof(f2077,definition,(
% 0.17/5.53 sP6_prd<=>((c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,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)))&(![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)))))),
% 0.17/5.53 introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 0.17/5.53 fof(f2078,plain,(
% 0.17/5.53 sP6_prd<~>((c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,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)))&(![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)))))),
% 0.17/5.53 inference(formula_renaming,[status(thm)],[f2076,f2077])).
% 0.17/5.53 fof(f2079,plain,(
% 0.17/5.53 (sP6_prd|((c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,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)))&(![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))))))&(~sP6_prd|((~c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,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)))|(?[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))))))),
% 0.17/5.53 inference(NNF_transformation,[status(thm)],[f2078])).
% 0.17/5.53 fof(f2080,plain,(
% 0.17/5.53 (sP6_prd|((c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,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)))&(![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))))))&(~sP6_prd|((~c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,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))|(~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,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,sK88_skl,sK87_skl),v_L)))))),
% 0.17/5.53 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])).
% 0.17/5.53 fof(f2081,plain,(
% 0.17/5.53 sP6_prd|c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L)),
% 0.17/5.53 inference(cnf_transformation,[status(thm)],[f2080])).
% 0.17/5.53 fof(f2082,plain,(
% 0.17/5.53 ![X0]: (sP6_prd|~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))),
% 0.17/5.53 inference(cnf_transformation,[status(thm)],[f2080])).
% 0.17/5.53 fof(f2083,plain,(
% 0.17/5.53 ![X0,X1]: (sP6_prd|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))),
% 0.17/5.53 inference(cnf_transformation,[status(thm)],[f2080])).
% 0.17/5.53 fof(f2084,plain,(
% 0.17/5.53 ~sP6_prd|~c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,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)|~sK87_skl=sK88_skl),
% 0.17/5.53 inference(cnf_transformation,[status(thm)],[f2080])).
% 0.17/5.53 fof(f2085,plain,(
% 0.17/5.53 ~sP6_prd|~c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,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_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)),
% 0.17/5.53 inference(cnf_transformation,[status(thm)],[f2080])).
% 0.17/5.53 fof(f2086,plain,(
% 0.17/5.53 ~sP6_prd|~c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,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_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)),
% 0.17/5.53 inference(cnf_transformation,[status(thm)],[f2080])).
% 0.17/5.53 fof(f2124,plain,(
% 0.17/5.53 (~sP6_prd|((c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,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)))&(![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))))))&(sP6_prd|((~c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,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)))|(?[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))))))),
% 0.17/5.53 inference(NNF_transformation,[status(thm)],[f2077])).
% 0.17/5.53 fof(f2125,plain,(
% 0.17/5.53 (~sP6_prd|((c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,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)))&(![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))))))&(sP6_prd|((~c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,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))|(~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,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,sK92_skl,sK93_skl),v_L)))))),
% 0.17/5.53 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])).
% 0.17/5.53 fof(f2126,plain,(
% 0.17/5.53 ~sP6_prd|c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L)),
% 0.17/5.53 inference(cnf_transformation,[status(thm)],[f2125])).
% 0.17/5.53 fof(f2127,plain,(
% 0.17/5.53 ![X0]: (~sP6_prd|~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))),
% 0.17/5.53 inference(cnf_transformation,[status(thm)],[f2125])).
% 0.17/5.53 fof(f2128,plain,(
% 0.17/5.53 ![X0,X1]: (~sP6_prd|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))),
% 0.17/5.53 inference(cnf_transformation,[status(thm)],[f2125])).
% 0.17/5.53 fof(f2129,plain,(
% 0.17/5.53 sP6_prd|~c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,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)|~sK92_skl=sK93_skl),
% 0.17/5.53 inference(cnf_transformation,[status(thm)],[f2125])).
% 0.17/5.53 fof(f2130,plain,(
% 0.17/5.53 sP6_prd|~c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,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_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)),
% 0.17/5.53 inference(cnf_transformation,[status(thm)],[f2125])).
% 0.17/5.53 fof(f2131,plain,(
% 0.17/5.53 sP6_prd|~c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,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_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)),
% 0.17/5.53 inference(cnf_transformation,[status(thm)],[f2125])).
% 0.17/5.53 fof(f2212,plain,(
% 0.17/5.53 c_Relation_Otrans(tc_Arrow__Order__Mirabelle_Oalt,v_L)),
% 0.17/5.53 inference(forward_subsumption_resolution,[status(thm)],[f2126,f2081])).
% 0.17/5.53 fof(f2213,plain,(
% 0.17/5.53 ~sP6_prd|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)|~sK87_skl=sK88_skl),
% 0.17/5.53 inference(forward_subsumption_resolution,[status(thm)],[f2084,f2212])).
% 0.17/5.53 fof(f2214,plain,(
% 0.17/5.53 ~sP6_prd|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_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)),
% 0.17/5.53 inference(forward_subsumption_resolution,[status(thm)],[f2085,f2212])).
% 0.17/5.53 fof(f2221,plain,(
% 0.17/5.53 ~sP6_prd|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_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)),
% 0.17/5.53 inference(forward_subsumption_resolution,[status(thm)],[f2086,f2212])).
% 0.17/5.53 fof(f2224,plain,(
% 0.17/5.53 ~sP6_prd|~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)),
% 0.17/5.53 inference(backward_subsumption_resolution,[status(thm)],[f2221,f2227])).
% 0.17/5.53 fof(f2225,plain,(
% 0.17/5.53 ~sP6_prd|~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)),
% 0.17/5.53 inference(backward_subsumption_resolution,[status(thm)],[f2214,f2227])).
% 0.17/5.53 fof(f2226,plain,(
% 0.17/5.53 ~sP6_prd|~sK87_skl=sK88_skl),
% 0.17/5.53 inference(backward_subsumption_resolution,[status(thm)],[f2213,f2227])).
% 0.17/5.53 fof(f2227,plain,(
% 0.17/5.53 ![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))),
% 0.17/5.53 inference(forward_subsumption_resolution,[status(thm)],[f2127,f2082])).
% 0.17/5.53 fof(f2244,plain,(
% 0.17/5.53 ![X0,X1]: (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))),
% 0.17/5.53 inference(forward_subsumption_resolution,[status(thm)],[f2128,f2083])).
% 0.17/5.53 fof(f2272,plain,(
% 0.17/5.53 sP6_prd|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)|~sK92_skl=sK93_skl),
% 0.17/5.53 inference(forward_subsumption_resolution,[status(thm)],[f2129,f2212])).
% 0.17/5.53 fof(f2278,plain,(
% 0.17/5.53 sP6_prd|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_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)),
% 0.17/5.53 inference(forward_subsumption_resolution,[status(thm)],[f2130,f2212])).
% 0.17/5.53 fof(f2283,plain,(
% 0.17/5.53 sP6_prd|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_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)),
% 0.17/5.53 inference(forward_subsumption_resolution,[status(thm)],[f2131,f2212])).
% 0.17/5.53 fof(f2288,plain,(
% 0.17/5.53 ~sP6_prd|sK88_skl=sK87_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,sK87_skl,sK88_skl),v_L)),
% 0.17/5.54 inference(resolution,[status(thm)],[f2224,f2244])).
% 0.17/5.54 fof(f2290,plain,(
% 0.17/5.54 ~sP6_prd|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)),
% 0.17/5.54 inference(forward_subsumption_resolution,[status(thm)],[f2288,f2226])).
% 0.17/5.54 fof(f2315,plain,(
% 0.17/5.54 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_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)),
% 0.17/5.54 inference(backward_subsumption_resolution,[status(thm)],[f2283,f2318])).
% 0.17/5.54 fof(f2316,plain,(
% 0.17/5.54 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_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)),
% 0.17/5.54 inference(backward_subsumption_resolution,[status(thm)],[f2278,f2318])).
% 0.17/5.54 fof(f2317,plain,(
% 0.17/5.54 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)|~sK92_skl=sK93_skl),
% 0.17/5.54 inference(backward_subsumption_resolution,[status(thm)],[f2272,f2318])).
% 0.17/5.54 fof(f2318,plain,(
% 0.17/5.54 ~sP6_prd),
% 0.17/5.54 inference(forward_subsumption_resolution,[status(thm)],[f2290,f2225])).
% 0.17/5.54 fof(f2319,plain,(
% 0.17/5.54 ~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)),
% 0.17/5.54 inference(forward_subsumption_resolution,[status(thm)],[f2315,f2227])).
% 0.17/5.54 fof(f2320,plain,(
% 0.17/5.54 ~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)),
% 0.17/5.54 inference(forward_subsumption_resolution,[status(thm)],[f2316,f2227])).
% 0.17/5.54 fof(f2321,plain,(
% 0.17/5.54 ~sK92_skl=sK93_skl),
% 0.17/5.54 inference(forward_subsumption_resolution,[status(thm)],[f2317,f2227])).
% 0.17/5.54 fof(f2324,plain,(
% 0.17/5.54 sK93_skl=sK92_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,sK92_skl,sK93_skl),v_L)),
% 0.17/5.54 inference(resolution,[status(thm)],[f2320,f2244])).
% 0.17/5.54 fof(f2326,plain,(
% 0.17/5.54 sK93_skl=sK92_skl),
% 0.17/5.54 inference(forward_subsumption_resolution,[status(thm)],[f2324,f2319])).
% 0.17/5.54 fof(f2328,plain,(
% 0.17/5.54 $false),
% 0.17/5.54 inference(forward_subsumption_resolution,[status(thm)],[f2326,f2321])).
% 0.17/5.54 % SZS output end CNFRefutation for theBenchmark.p
% 0.17/5.56 % Elapsed time: 0.147445 seconds
% 0.17/5.56 % CPU time: 0.375630 seconds
% 0.17/5.56 % Total memory used: 98.626 MB
% 0.17/5.56 % Net memory used: 98.152 MB
%------------------------------------------------------------------------------