%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : CSR063+1 : TPTP v8.1.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n022.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Fri Jul 15 21:57:21 EDT 2022
% Result : Theorem 0.13s 0.40s
% Output : CNFRefutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 12
% Syntax : Number of formulae : 74 ( 23 unt; 0 def)
% Number of atoms : 125 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 103 ( 52 ~; 41 |; 1 &)
% ( 0 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 12 ( 11 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-1 aty)
% Number of variables : 66 ( 9 sgn 41 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(just2,axiom,
! [OBJ] :
( setorcollection(OBJ)
=> mathematicalthing(OBJ) ) ).
fof(just5,axiom,
! [OBJ] :
( mathematicalorcomputationalthing(OBJ)
=> intangible(OBJ) ) ).
fof(just7,axiom,
! [OBJ] :
~ ( intangible(OBJ)
& partiallytangible(OBJ) ) ).
fof(just9,axiom,
! [OBJ] :
( computerdataartifact(OBJ)
=> artifact(OBJ) ) ).
fof(just11,axiom,
! [OBJ] :
( mathematicalthing(OBJ)
=> mathematicalorcomputationalthing(OBJ) ) ).
fof(just14,axiom,
! [OBJ] :
( artifact(OBJ)
=> inanimateobject_nonnatural(OBJ) ) ).
fof(just16,axiom,
! [OBJ] :
( inanimateobject_nonnatural(OBJ)
=> inanimateobject(OBJ) ) ).
fof(just18,axiom,
! [OBJ] :
( inanimateobject(OBJ)
=> partiallytangible(OBJ) ) ).
fof(just22,axiom,
! [ARG1,ARG2] :
( disjointwith(ARG1,ARG2)
=> no(ARG1,ARG2) ) ).
fof(just44,axiom,
! [INS,ARG2] :
( no(INS,ARG2)
=> setorcollection(INS) ) ).
fof(just95,axiom,
! [ARG1] : computerdataartifact(f_urlreferentfn(ARG1)) ).
fof(query63,conjecture,
~ disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949) ).
fof(subgoal_0,plain,
~ disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(strip,[],[query63]) ).
fof(negate_0_0,plain,
~ ~ disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(negate,[],[subgoal_0]) ).
fof(normalize_0_0,plain,
! [OBJ] :
( ~ mathematicalorcomputationalthing(OBJ)
| intangible(OBJ) ),
inference(canonicalize,[],[just5]) ).
fof(normalize_0_1,plain,
! [OBJ] :
( ~ mathematicalorcomputationalthing(OBJ)
| intangible(OBJ) ),
inference(specialize,[],[normalize_0_0]) ).
fof(normalize_0_2,plain,
! [OBJ] :
( ~ mathematicalthing(OBJ)
| mathematicalorcomputationalthing(OBJ) ),
inference(canonicalize,[],[just11]) ).
fof(normalize_0_3,plain,
! [OBJ] :
( ~ mathematicalthing(OBJ)
| mathematicalorcomputationalthing(OBJ) ),
inference(specialize,[],[normalize_0_2]) ).
fof(normalize_0_4,plain,
! [OBJ] :
( ~ setorcollection(OBJ)
| mathematicalthing(OBJ) ),
inference(canonicalize,[],[just2]) ).
fof(normalize_0_5,plain,
! [OBJ] :
( ~ setorcollection(OBJ)
| mathematicalthing(OBJ) ),
inference(specialize,[],[normalize_0_4]) ).
fof(normalize_0_6,plain,
! [INS] :
( setorcollection(INS)
| ! [ARG2] : ~ no(INS,ARG2) ),
inference(canonicalize,[],[just44]) ).
fof(normalize_0_7,plain,
! [INS] :
( setorcollection(INS)
| ! [ARG2] : ~ no(INS,ARG2) ),
inference(specialize,[],[normalize_0_6]) ).
fof(normalize_0_8,plain,
! [ARG2,INS] :
( ~ no(INS,ARG2)
| setorcollection(INS) ),
inference(clausify,[],[normalize_0_7]) ).
fof(normalize_0_9,plain,
disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(canonicalize,[],[negate_0_0]) ).
fof(normalize_0_10,plain,
! [ARG1,ARG2] :
( ~ disjointwith(ARG1,ARG2)
| no(ARG1,ARG2) ),
inference(canonicalize,[],[just22]) ).
fof(normalize_0_11,plain,
! [ARG1,ARG2] :
( ~ disjointwith(ARG1,ARG2)
| no(ARG1,ARG2) ),
inference(specialize,[],[normalize_0_10]) ).
fof(normalize_0_12,plain,
! [OBJ] :
( ~ intangible(OBJ)
| ~ partiallytangible(OBJ) ),
inference(canonicalize,[],[just7]) ).
fof(normalize_0_13,plain,
! [OBJ] :
( ~ intangible(OBJ)
| ~ partiallytangible(OBJ) ),
inference(specialize,[],[normalize_0_12]) ).
fof(normalize_0_14,plain,
! [OBJ] :
( ~ inanimateobject(OBJ)
| partiallytangible(OBJ) ),
inference(canonicalize,[],[just18]) ).
fof(normalize_0_15,plain,
! [OBJ] :
( ~ inanimateobject(OBJ)
| partiallytangible(OBJ) ),
inference(specialize,[],[normalize_0_14]) ).
fof(normalize_0_16,plain,
! [ARG1] : computerdataartifact(f_urlreferentfn(ARG1)),
inference(canonicalize,[],[just95]) ).
fof(normalize_0_17,plain,
! [ARG1] : computerdataartifact(f_urlreferentfn(ARG1)),
inference(specialize,[],[normalize_0_16]) ).
fof(normalize_0_18,plain,
! [OBJ] :
( ~ computerdataartifact(OBJ)
| artifact(OBJ) ),
inference(canonicalize,[],[just9]) ).
fof(normalize_0_19,plain,
! [OBJ] :
( ~ computerdataartifact(OBJ)
| artifact(OBJ) ),
inference(specialize,[],[normalize_0_18]) ).
fof(normalize_0_20,plain,
! [OBJ] :
( ~ artifact(OBJ)
| inanimateobject_nonnatural(OBJ) ),
inference(canonicalize,[],[just14]) ).
fof(normalize_0_21,plain,
! [OBJ] :
( ~ artifact(OBJ)
| inanimateobject_nonnatural(OBJ) ),
inference(specialize,[],[normalize_0_20]) ).
fof(normalize_0_22,plain,
! [OBJ] :
( ~ inanimateobject_nonnatural(OBJ)
| inanimateobject(OBJ) ),
inference(canonicalize,[],[just16]) ).
fof(normalize_0_23,plain,
! [OBJ] :
( ~ inanimateobject_nonnatural(OBJ)
| inanimateobject(OBJ) ),
inference(specialize,[],[normalize_0_22]) ).
cnf(refute_0_0,plain,
( ~ mathematicalorcomputationalthing(OBJ)
| intangible(OBJ) ),
inference(canonicalize,[],[normalize_0_1]) ).
cnf(refute_0_1,plain,
( ~ mathematicalorcomputationalthing(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))
| intangible(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) ),
inference(subst,[],[refute_0_0:[bind(OBJ,$fot(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))))]]) ).
cnf(refute_0_2,plain,
( ~ mathematicalthing(OBJ)
| mathematicalorcomputationalthing(OBJ) ),
inference(canonicalize,[],[normalize_0_3]) ).
cnf(refute_0_3,plain,
( ~ mathematicalthing(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))
| mathematicalorcomputationalthing(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) ),
inference(subst,[],[refute_0_2:[bind(OBJ,$fot(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))))]]) ).
cnf(refute_0_4,plain,
( ~ setorcollection(OBJ)
| mathematicalthing(OBJ) ),
inference(canonicalize,[],[normalize_0_5]) ).
cnf(refute_0_5,plain,
( ~ setorcollection(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))
| mathematicalthing(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) ),
inference(subst,[],[refute_0_4:[bind(OBJ,$fot(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))))]]) ).
cnf(refute_0_6,plain,
( ~ no(INS,ARG2)
| setorcollection(INS) ),
inference(canonicalize,[],[normalize_0_8]) ).
cnf(refute_0_7,plain,
( ~ no(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949)
| setorcollection(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) ),
inference(subst,[],[refute_0_6:[bind(ARG2,$fot(c_tptpcol_16_118949)),bind(INS,$fot(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))))]]) ).
cnf(refute_0_8,plain,
disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(canonicalize,[],[normalize_0_9]) ).
cnf(refute_0_9,plain,
( ~ disjointwith(ARG1,ARG2)
| no(ARG1,ARG2) ),
inference(canonicalize,[],[normalize_0_11]) ).
cnf(refute_0_10,plain,
( ~ disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949)
| no(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949) ),
inference(subst,[],[refute_0_9:[bind(ARG1,$fot(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))),bind(ARG2,$fot(c_tptpcol_16_118949))]]) ).
cnf(refute_0_11,plain,
no(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(resolve,[$cnf( disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949) )],[refute_0_8,refute_0_10]) ).
cnf(refute_0_12,plain,
setorcollection(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))),
inference(resolve,[$cnf( no(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949) )],[refute_0_11,refute_0_7]) ).
cnf(refute_0_13,plain,
mathematicalthing(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))),
inference(resolve,[$cnf( setorcollection(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) )],[refute_0_12,refute_0_5]) ).
cnf(refute_0_14,plain,
mathematicalorcomputationalthing(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))),
inference(resolve,[$cnf( mathematicalthing(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) )],[refute_0_13,refute_0_3]) ).
cnf(refute_0_15,plain,
intangible(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))),
inference(resolve,[$cnf( mathematicalorcomputationalthing(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) )],[refute_0_14,refute_0_1]) ).
cnf(refute_0_16,plain,
( ~ intangible(OBJ)
| ~ partiallytangible(OBJ) ),
inference(canonicalize,[],[normalize_0_13]) ).
cnf(refute_0_17,plain,
( ~ intangible(f_urlreferentfn(X_17))
| ~ partiallytangible(f_urlreferentfn(X_17)) ),
inference(subst,[],[refute_0_16:[bind(OBJ,$fot(f_urlreferentfn(X_17)))]]) ).
cnf(refute_0_18,plain,
( ~ inanimateobject(OBJ)
| partiallytangible(OBJ) ),
inference(canonicalize,[],[normalize_0_15]) ).
cnf(refute_0_19,plain,
( ~ inanimateobject(f_urlreferentfn(X_16))
| partiallytangible(f_urlreferentfn(X_16)) ),
inference(subst,[],[refute_0_18:[bind(OBJ,$fot(f_urlreferentfn(X_16)))]]) ).
cnf(refute_0_20,plain,
computerdataartifact(f_urlreferentfn(ARG1)),
inference(canonicalize,[],[normalize_0_17]) ).
cnf(refute_0_21,plain,
( ~ computerdataartifact(OBJ)
| artifact(OBJ) ),
inference(canonicalize,[],[normalize_0_19]) ).
cnf(refute_0_22,plain,
( ~ computerdataartifact(f_urlreferentfn(ARG1))
| artifact(f_urlreferentfn(ARG1)) ),
inference(subst,[],[refute_0_21:[bind(OBJ,$fot(f_urlreferentfn(ARG1)))]]) ).
cnf(refute_0_23,plain,
artifact(f_urlreferentfn(ARG1)),
inference(resolve,[$cnf( computerdataartifact(f_urlreferentfn(ARG1)) )],[refute_0_20,refute_0_22]) ).
cnf(refute_0_24,plain,
( ~ artifact(OBJ)
| inanimateobject_nonnatural(OBJ) ),
inference(canonicalize,[],[normalize_0_21]) ).
cnf(refute_0_25,plain,
( ~ artifact(f_urlreferentfn(ARG1))
| inanimateobject_nonnatural(f_urlreferentfn(ARG1)) ),
inference(subst,[],[refute_0_24:[bind(OBJ,$fot(f_urlreferentfn(ARG1)))]]) ).
cnf(refute_0_26,plain,
inanimateobject_nonnatural(f_urlreferentfn(ARG1)),
inference(resolve,[$cnf( artifact(f_urlreferentfn(ARG1)) )],[refute_0_23,refute_0_25]) ).
cnf(refute_0_27,plain,
( ~ inanimateobject_nonnatural(OBJ)
| inanimateobject(OBJ) ),
inference(canonicalize,[],[normalize_0_23]) ).
cnf(refute_0_28,plain,
( ~ inanimateobject_nonnatural(f_urlreferentfn(ARG1))
| inanimateobject(f_urlreferentfn(ARG1)) ),
inference(subst,[],[refute_0_27:[bind(OBJ,$fot(f_urlreferentfn(ARG1)))]]) ).
cnf(refute_0_29,plain,
inanimateobject(f_urlreferentfn(ARG1)),
inference(resolve,[$cnf( inanimateobject_nonnatural(f_urlreferentfn(ARG1)) )],[refute_0_26,refute_0_28]) ).
cnf(refute_0_30,plain,
inanimateobject(f_urlreferentfn(X_16)),
inference(subst,[],[refute_0_29:[bind(ARG1,$fot(X_16))]]) ).
cnf(refute_0_31,plain,
partiallytangible(f_urlreferentfn(X_16)),
inference(resolve,[$cnf( inanimateobject(f_urlreferentfn(X_16)) )],[refute_0_30,refute_0_19]) ).
cnf(refute_0_32,plain,
partiallytangible(f_urlreferentfn(X_17)),
inference(subst,[],[refute_0_31:[bind(X_16,$fot(X_17))]]) ).
cnf(refute_0_33,plain,
~ intangible(f_urlreferentfn(X_17)),
inference(resolve,[$cnf( partiallytangible(f_urlreferentfn(X_17)) )],[refute_0_32,refute_0_17]) ).
cnf(refute_0_34,plain,
~ intangible(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))),
inference(subst,[],[refute_0_33:[bind(X_17,$fot(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))]]) ).
cnf(refute_0_35,plain,
$false,
inference(resolve,[$cnf( intangible(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) )],[refute_0_15,refute_0_34]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : CSR063+1 : TPTP v8.1.0. Released v3.4.0.
% 0.07/0.13 % Command : metis --show proof --show saturation %s
% 0.13/0.35 % Computer : n022.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Sat Jun 11 01:43:39 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.13/0.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.13/0.40 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.40
% 0.13/0.40 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 0.20/0.40
%------------------------------------------------------------------------------