%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CSR063+1 : TPTP v8.2.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %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 : 300s
% DateTime : Mon Jun 24 05:00:54 EDT 2024
% Result : Theorem 1.18s 1.23s
% Output : CNFRefutation 1.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : CSR063+1 : TPTP v8.2.0. Released v3.4.0.
% 0.10/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.11/0.32 % Computer : n022.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Wed Jun 19 22:06:39 EDT 2024
% 0.11/0.32 % CPUTime :
% 0.16/0.56 start to proof:theBenchmark
% 1.10/1.20 %-------------------------------------------
% 1.10/1.20 % File :CSE---1.7
% 1.10/1.20 % Problem :theBenchmark
% 1.10/1.20 % Transform :cnf
% 1.10/1.20 % Format :tptp:raw
% 1.10/1.20 % Command :java -jar mcs_scs.jar %d %s
% 1.10/1.20
% 1.10/1.20 % Result :Theorem 0.580000s
% 1.10/1.20 % Output :CNFRefutation 0.580000s
% 1.10/1.20 %-------------------------------------------
% 1.10/1.20 %------------------------------------------------------------------------------
% 1.10/1.20 % File : CSR063+1 : TPTP v8.2.0. Released v3.4.0.
% 1.10/1.20 % Domain : Common Sense Reasoning
% 1.10/1.20 % Problem : Autogenerated Cyc Problem CSR063+1
% 1.10/1.20 % Version : Especial.
% 1.10/1.20 % English :
% 1.10/1.20
% 1.10/1.20 % Refs : [RS+] Reagan Smith et al., The Cyc TPTP Challenge Problem
% 1.10/1.20 % Source : [RS+]
% 1.10/1.20 % Names :
% 1.10/1.20
% 1.10/1.20 % Status : Theorem
% 1.10/1.20 % Rating : 0.12 v8.2.0, 0.13 v8.1.0, 0.14 v7.5.0, 0.10 v7.4.0, 0.12 v7.3.0, 0.14 v7.2.0, 0.17 v7.1.0, 0.25 v7.0.0, 0.00 v6.1.0, 0.04 v6.0.0, 0.25 v5.5.0, 0.08 v5.4.0, 0.13 v5.3.0, 0.22 v5.2.0, 0.07 v5.0.0, 0.15 v4.1.0, 0.11 v4.0.0, 0.10 v3.7.0, 0.00 v3.4.0
% 1.10/1.20 % Syntax : Number of formulae : 116 ( 23 unt; 0 def)
% 1.10/1.20 % Number of atoms : 235 ( 0 equ)
% 1.10/1.20 % Maximal formula atoms : 3 ( 2 avg)
% 1.10/1.20 % Number of connectives : 124 ( 5 ~; 0 |; 30 &)
% 1.10/1.20 % ( 0 <=>; 89 =>; 0 <=; 0 <~>)
% 1.10/1.20 % Maximal formula depth : 7 ( 4 avg)
% 1.10/1.20 % Maximal term depth : 3 ( 1 avg)
% 1.10/1.20 % Number of predicates : 30 ( 30 usr; 0 prp; 1-3 aty)
% 1.10/1.20 % Number of functors : 23 ( 23 usr; 21 con; 0-1 aty)
% 1.10/1.20 % Number of variables : 183 ( 183 !; 0 ?)
% 1.10/1.20 % SPC : FOF_THM_RFO_NEQ
% 1.10/1.20
% 1.10/1.20 % Comments : Autogenerated from the OpenCyc KB. Documentation can be found at
% 1.10/1.20 % http://opencyc.org/doc/#TPTP_Challenge_Problem_Set
% 1.10/1.20 % : Cyc(R) Knowledge Base Copyright(C) 1995-2007 Cycorp, Inc., Austin,
% 1.10/1.20 % TX, USA. All rights reserved.
% 1.10/1.20 % : OpenCyc Knowledge Base Copyright(C) 2001-2007 Cycorp, Inc.,
% 1.10/1.20 % Austin, TX, USA. All rights reserved.
% 1.10/1.20 %------------------------------------------------------------------------------
% 1.10/1.20 %$problem_series(cyc_scaling_1,[CSR025+1,CSR026+1,CSR027+1,CSR028+1,CSR029+1,CSR030+1,CSR031+1,CSR032+1,CSR033+1,CSR034+1,CSR035+1,CSR036+1,CSR037+1,CSR038+1,CSR039+1,CSR040+1,CSR041+1,CSR042+1,CSR043+1,CSR044+1,CSR045+1,CSR046+1,CSR047+1,CSR048+1,CSR049+1,CSR050+1,CSR051+1,CSR052+1,CSR053+1,CSR054+1,CSR055+1,CSR056+1,CSR057+1,CSR058+1,CSR059+1,CSR060+1,CSR061+1,CSR062+1,CSR063+1,CSR064+1,CSR065+1,CSR066+1,CSR067+1,CSR068+1,CSR069+1,CSR070+1,CSR071+1,CSR072+1,CSR073+1,CSR074+1])
% 1.10/1.20 %$static(cyc_scaling_1,include('Axioms/CSR002+0.ax'))
% 1.10/1.20 %----Empty file include('Axioms/CSR002+0.ax').
% 1.10/1.20 %------------------------------------------------------------------------------
% 1.10/1.20 % Cyc Assertion #294201:
% 1.10/1.20 fof(just1,axiom,
% 1.10/1.20 genls(c_setorcollection,c_mathematicalthing) ).
% 1.10/1.20
% 1.10/1.20 fof(just2,axiom,
% 1.10/1.20 ! [OBJ] :
% 1.10/1.20 ( setorcollection(OBJ)
% 1.10/1.20 => mathematicalthing(OBJ) ) ).
% 1.10/1.20
% 1.10/1.20 % Cyc Assertion #385707:
% 1.10/1.20 fof(just3,axiom,
% 1.10/1.20 computerdataartifact(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) ).
% 1.10/1.20
% 1.10/1.20 % Cyc Assertion #642174:
% 1.10/1.20 fof(just4,axiom,
% 1.10/1.20 genls(c_mathematicalorcomputationalthing,c_intangible) ).
% 1.10/1.20
% 1.10/1.20 fof(just5,axiom,
% 1.10/1.20 ! [OBJ] :
% 1.10/1.20 ( mathematicalorcomputationalthing(OBJ)
% 1.10/1.20 => intangible(OBJ) ) ).
% 1.10/1.20
% 1.10/1.20 % Cyc Assertion #670314:
% 1.10/1.20 fof(just6,axiom,
% 1.10/1.20 disjointwith(c_intangible,c_partiallytangible) ).
% 1.10/1.20
% 1.10/1.20 fof(just7,axiom,
% 1.10/1.20 ! [OBJ] :
% 1.10/1.20 ~ ( intangible(OBJ)
% 1.10/1.20 & partiallytangible(OBJ) ) ).
% 1.10/1.20
% 1.10/1.20 % Cyc Assertion #833751:
% 1.10/1.20 fof(just8,axiom,
% 1.10/1.20 genls(c_computerdataartifact,c_artifact) ).
% 1.10/1.20
% 1.10/1.20 fof(just9,axiom,
% 1.10/1.20 ! [OBJ] :
% 1.10/1.20 ( computerdataartifact(OBJ)
% 1.10/1.21 => artifact(OBJ) ) ).
% 1.10/1.21
% 1.10/1.21 % Cyc Assertion #913648:
% 1.10/1.21 fof(just10,axiom,
% 1.10/1.21 genls(c_mathematicalthing,c_mathematicalorcomputationalthing) ).
% 1.10/1.21
% 1.10/1.21 fof(just11,axiom,
% 1.10/1.21 ! [OBJ] :
% 1.10/1.21 ( mathematicalthing(OBJ)
% 1.10/1.21 => mathematicalorcomputationalthing(OBJ) ) ).
% 1.10/1.21
% 1.10/1.21 % Cyc Assertion #985685:
% 1.10/1.21 fof(just12,axiom,
% 1.10/1.21 genlmt(c_universalvocabularymt,c_basekb) ).
% 1.10/1.21
% 1.10/1.21 % Cyc Assertion #1591255:
% 1.10/1.21 fof(just13,axiom,
% 1.10/1.21 genls(c_artifact,c_inanimateobject_nonnatural) ).
% 1.10/1.21
% 1.10/1.21 fof(just14,axiom,
% 1.10/1.21 ! [OBJ] :
% 1.10/1.21 ( artifact(OBJ)
% 1.10/1.21 => inanimateobject_nonnatural(OBJ) ) ).
% 1.10/1.21
% 1.10/1.21 % Cyc Assertion #1643131:
% 1.10/1.21 fof(just15,axiom,
% 1.10/1.21 genls(c_inanimateobject_nonnatural,c_inanimateobject) ).
% 1.10/1.21
% 1.10/1.21 fof(just16,axiom,
% 1.10/1.21 ! [OBJ] :
% 1.10/1.21 ( inanimateobject_nonnatural(OBJ)
% 1.10/1.21 => inanimateobject(OBJ) ) ).
% 1.10/1.21
% 1.10/1.21 % Cyc Assertion #1694819:
% 1.10/1.21 fof(just17,axiom,
% 1.10/1.21 genls(c_inanimateobject,c_partiallytangible) ).
% 1.10/1.21
% 1.10/1.21 fof(just18,axiom,
% 1.10/1.21 ! [OBJ] :
% 1.10/1.21 ( inanimateobject(OBJ)
% 1.10/1.21 => partiallytangible(OBJ) ) ).
% 1.10/1.21
% 1.10/1.21 % Cyc Assertion #398814:
% 1.10/1.21 fof(just19,axiom,
% 1.10/1.21 ! [OBJ,COL1,COL2] :
% 1.10/1.21 ~ ( isa(OBJ,COL1)
% 1.10/1.21 & isa(OBJ,COL2)
% 1.10/1.21 & disjointwith(COL1,COL2) ) ).
% 1.10/1.21
% 1.10/1.21 % Cyc Assertion #831913:
% 1.10/1.21 fof(just20,axiom,
% 1.10/1.21 ! [SPECPRED,PRED,GENLPRED] :
% 1.10/1.21 ( ( genlinverse(SPECPRED,PRED)
% 1.10/1.21 & genlinverse(PRED,GENLPRED) )
% 1.10/1.21 => genlpreds(SPECPRED,GENLPRED) ) ).
% 1.10/1.21
% 1.10/1.21 % Cyc Assertion #649807:
% 1.10/1.21 fof(just21,axiom,
% 1.10/1.21 genlpreds(c_disjointwith,c_no) ).
% 1.10/1.21
% 1.10/1.21 fof(just22,axiom,
% 1.10/1.21 ! [ARG1,ARG2] :
% 1.10/1.21 ( disjointwith(ARG1,ARG2)
% 1.10/1.21 => no(ARG1,ARG2) ) ).
% 1.10/1.21
% 1.10/1.21 % Cyc Assertion #849068:
% 1.10/1.21 fof(just23,axiom,
% 1.10/1.21 transitivebinarypredicate(c_genlpreds) ).
% 1.10/1.21
% 1.10/1.21 % Cyc Assertion #1263090:
% 1.10/1.21 fof(just24,axiom,
% 1.10/1.21 genlpreds(c_no,c_few) ).
% 1.10/1.21
% 1.10/1.21 fof(just25,axiom,
% 1.10/1.21 ! [ARG1,ARG2] :
% 1.10/1.21 ( no(ARG1,ARG2)
% 1.10/1.21 => few(ARG1,ARG2) ) ).
% 1.10/1.21
% 1.10/1.21 % Cyc Assertion #398814:
% 1.10/1.21 fof(just26,axiom,
% 1.10/1.21 ! [OBJ,COL1,COL2] :
% 1.10/1.21 ~ ( isa(OBJ,COL1)
% 1.10/1.21 & isa(OBJ,COL2)
% 1.10/1.21 & disjointwith(COL1,COL2) ) ).
% 1.10/1.21
% 1.10/1.21 % Cyc Assertion #831913:
% 1.10/1.21 fof(just27,axiom,
% 1.10/1.21 ! [SPECPRED,PRED,GENLPRED] :
% 1.10/1.21 ( ( genlinverse(SPECPRED,PRED)
% 1.10/1.21 & genlinverse(PRED,GENLPRED) )
% 1.10/1.21 => genlpreds(SPECPRED,GENLPRED) ) ).
% 1.10/1.21
% 1.10/1.21 % Cyc Assertion #1255218:
% 1.10/1.21 fof(just28,axiom,
% 1.10/1.21 arg2isa(c_few,c_setorcollection) ).
% 1.10/1.21
% 1.10/1.21 fof(just29,axiom,
% 1.10/1.21 ! [ARG1,ARG2] :
% 1.10/1.21 ( few(ARG1,ARG2)
% 1.10/1.21 => setorcollection(ARG2) ) ).
% 1.10/1.21
% 1.10/1.21 % Cyc Assertion #398814:
% 1.10/1.21 fof(just30,axiom,
% 1.10/1.21 ! [OBJ,COL1,COL2] :
% 1.10/1.21 ~ ( isa(OBJ,COL1)
% 1.10/1.21 & isa(OBJ,COL2)
% 1.10/1.21 & disjointwith(COL1,COL2) ) ).
% 1.10/1.21
% 1.10/1.21 % Cyc Assertion #831913:
% 1.10/1.21 fof(just31,axiom,
% 1.10/1.21 ! [SPECPRED,PRED,GENLPRED] :
% 1.10/1.21 ( ( genlinverse(SPECPRED,PRED)
% 1.10/1.21 & genlinverse(PRED,GENLPRED) )
% 1.10/1.21 => genlpreds(SPECPRED,GENLPRED) ) ).
% 1.10/1.21
% 1.10/1.21 % Cyc Constant #59425:
% 1.10/1.21 fof(just32,axiom,
% 1.10/1.21 ! [ARG1,INS] :
% 1.10/1.21 ( arg2isa(ARG1,INS)
% 1.10/1.21 => collection(INS) ) ).
% 1.10/1.21
% 1.10/1.21 fof(just33,axiom,
% 1.10/1.21 ! [INS,ARG2] :
% 1.10/1.21 ( arg2isa(INS,ARG2)
% 1.10/1.21 => relation(INS) ) ).
% 1.10/1.21
% 1.10/1.21 fof(just34,axiom,
% 1.10/1.21 ! [ARG1,OLD,NEW] :
% 1.10/1.21 ( ( arg2isa(ARG1,OLD)
% 1.10/1.21 & genls(OLD,NEW) )
% 1.10/1.21 => arg2isa(ARG1,NEW) ) ).
% 1.10/1.21
% 1.10/1.21 fof(just35,axiom,
% 1.10/1.21 ! [ARG1,OLD,NEW] :
% 1.10/1.21 ( ( arg2isa(ARG1,OLD)
% 1.10/1.21 & genls(OLD,NEW) )
% 1.10/1.21 => arg2isa(ARG1,NEW) ) ).
% 1.10/1.21
% 1.10/1.21 % Cyc Constant #72033:
% 1.10/1.21 fof(just36,axiom,
% 1.10/1.21 ! [ARG1,INS] :
% 1.10/1.21 ( few(ARG1,INS)
% 1.10/1.21 => setorcollection(INS) ) ).
% 1.10/1.21
% 1.10/1.21 fof(just37,axiom,
% 1.10/1.21 ! [ARG1,INS] :
% 1.10/1.21 ( few(ARG1,INS)
% 1.10/1.21 => setorcollection(INS) ) ).
% 1.10/1.21
% 1.10/1.21 fof(just38,axiom,
% 1.10/1.21 ! [INS,ARG2] :
% 1.10/1.21 ( few(INS,ARG2)
% 1.10/1.21 => setorcollection(INS) ) ).
% 1.10/1.21
% 1.10/1.21 fof(just39,axiom,
% 1.10/1.21 ! [INS,ARG2] :
% 1.10/1.21 ( few(INS,ARG2)
% 1.10/1.21 => setorcollection(INS) ) ).
% 1.10/1.21
% 1.10/1.21 fof(just40,axiom,
% 1.10/1.21 ! [ARG1,OLD,NEW] :
% 1.10/1.21 ( ( few(ARG1,OLD)
% 1.10/1.21 & subsetof(NEW,OLD) )
% 1.10/1.21 => few(ARG1,NEW) ) ).
% 1.10/1.21
% 1.10/1.21 % Cyc Constant #127156:
% 1.10/1.21 fof(just41,axiom,
% 1.10/1.21 ! [X] :
% 1.10/1.21 ( isa(X,c_transitivebinarypredicate)
% 1.10/1.21 => transitivebinarypredicate(X) ) ).
% 1.10/1.21
% 1.10/1.21 fof(just42,axiom,
% 1.10/1.21 ! [X] :
% 1.10/1.21 ( transitivebinarypredicate(X)
% 1.10/1.21 => isa(X,c_transitivebinarypredicate) ) ).
% 1.10/1.21
% 1.10/1.21 % Cyc Constant #117270:
% 1.10/1.21 fof(just43,axiom,
% 1.10/1.21 ! [ARG1,INS] :
% 1.10/1.21 ( no(ARG1,INS)
% 1.10/1.21 => setorcollection(INS) ) ).
% 1.10/1.21
% 1.10/1.21 fof(just44,axiom,
% 1.10/1.21 ! [INS,ARG2] :
% 1.10/1.21 ( no(INS,ARG2)
% 1.10/1.21 => setorcollection(INS) ) ).
% 1.10/1.21
% 1.10/1.21 fof(just45,axiom,
% 1.10/1.21 ! [X,Y] :
% 1.10/1.21 ( no(X,Y)
% 1.10/1.21 => no(Y,X) ) ).
% 1.10/1.21
% 1.10/1.21 fof(just46,axiom,
% 1.10/1.21 ! [ARG1,OLD,NEW] :
% 1.10/1.21 ( ( no(ARG1,OLD)
% 1.10/1.21 & subsetof(NEW,OLD) )
% 1.10/1.21 => no(ARG1,NEW) ) ).
% 1.10/1.21
% 1.10/1.21 fof(just47,axiom,
% 1.10/1.21 ! [OLD,ARG2,NEW] :
% 1.10/1.21 ( ( no(OLD,ARG2)
% 1.10/1.21 & subsetof(NEW,OLD) )
% 1.10/1.21 => no(NEW,ARG2) ) ).
% 1.10/1.21
% 1.10/1.21 fof(just48,axiom,
% 1.10/1.21 ! [OLD,ARG2,NEW] :
% 1.10/1.21 ( ( no(OLD,ARG2)
% 1.10/1.21 & genls(NEW,OLD) )
% 1.10/1.21 => no(NEW,ARG2) ) ).
% 1.10/1.21
% 1.10/1.21 fof(just49,axiom,
% 1.10/1.21 ! [ARG1,OLD,NEW] :
% 1.10/1.21 ( ( no(ARG1,OLD)
% 1.10/1.21 & genls(NEW,OLD) )
% 1.10/1.21 => no(ARG1,NEW) ) ).
% 1.10/1.21
% 1.10/1.21 fof(just50,axiom,
% 1.10/1.21 ! [OLD,ARG2,NEW] :
% 1.10/1.21 ( ( no(OLD,ARG2)
% 1.10/1.21 & subsetof(NEW,OLD) )
% 1.10/1.21 => no(NEW,ARG2) ) ).
% 1.10/1.21
% 1.10/1.21 fof(just51,axiom,
% 1.10/1.21 ! [ARG1,OLD,NEW] :
% 1.10/1.21 ( ( no(ARG1,OLD)
% 1.10/1.21 & subsetof(NEW,OLD) )
% 1.10/1.21 => no(ARG1,NEW) ) ).
% 1.10/1.21
% 1.10/1.21 % Cyc Constant #40273:
% 1.10/1.21 fof(just52,axiom,
% 1.10/1.21 ! [ARG1,INS] :
% 1.10/1.21 ( genlpreds(ARG1,INS)
% 1.10/1.21 => predicate(INS) ) ).
% 1.10/1.21
% 1.10/1.21 fof(just53,axiom,
% 1.10/1.21 ! [ARG1,INS] :
% 1.10/1.21 ( genlpreds(ARG1,INS)
% 1.10/1.21 => predicate(INS) ) ).
% 1.10/1.21
% 1.10/1.21 fof(just54,axiom,
% 1.10/1.21 ! [INS,ARG2] :
% 1.10/1.21 ( genlpreds(INS,ARG2)
% 1.10/1.21 => predicate(INS) ) ).
% 1.10/1.21
% 1.10/1.21 fof(just55,axiom,
% 1.10/1.21 ! [INS,ARG2] :
% 1.10/1.21 ( genlpreds(INS,ARG2)
% 1.10/1.21 => predicate(INS) ) ).
% 1.10/1.21
% 1.10/1.21 fof(just56,axiom,
% 1.10/1.21 ! [X,Y,Z] :
% 1.10/1.21 ( ( genlpreds(X,Y)
% 1.10/1.21 & genlpreds(Y,Z) )
% 1.10/1.21 => genlpreds(X,Z) ) ).
% 1.10/1.21
% 1.10/1.21 fof(just57,axiom,
% 1.10/1.21 ! [X] :
% 1.10/1.21 ( predicate(X)
% 1.10/1.21 => genlpreds(X,X) ) ).
% 1.10/1.21
% 1.10/1.21 fof(just58,axiom,
% 1.10/1.21 ! [X] :
% 1.10/1.21 ( predicate(X)
% 1.10/1.21 => genlpreds(X,X) ) ).
% 1.10/1.21
% 1.10/1.21 % Cyc Constant #45259:
% 1.10/1.21 fof(just59,axiom,
% 1.10/1.21 ! [ARG1,INS] :
% 1.10/1.21 ( genlinverse(ARG1,INS)
% 1.10/1.21 => binarypredicate(INS) ) ).
% 1.10/1.21
% 1.10/1.21 fof(just60,axiom,
% 1.10/1.21 ! [INS,ARG2] :
% 1.10/1.21 ( genlinverse(INS,ARG2)
% 1.10/1.21 => binarypredicate(INS) ) ).
% 1.10/1.21
% 1.10/1.21 fof(just61,axiom,
% 1.10/1.21 ! [OLD,ARG2,NEW] :
% 1.10/1.21 ( ( genlinverse(OLD,ARG2)
% 1.10/1.21 & genlpreds(NEW,OLD) )
% 1.10/1.21 => genlinverse(NEW,ARG2) ) ).
% 1.10/1.21
% 1.10/1.21 fof(just62,axiom,
% 1.10/1.22 ! [ARG1,OLD,NEW] :
% 1.10/1.22 ( ( genlinverse(ARG1,OLD)
% 1.10/1.22 & genlpreds(OLD,NEW) )
% 1.10/1.22 => genlinverse(ARG1,NEW) ) ).
% 1.10/1.22
% 1.10/1.22 % Cyc Constant #101883:
% 1.10/1.22 fof(just63,axiom,
% 1.10/1.22 ! [X] :
% 1.10/1.22 ( isa(X,c_inanimateobject)
% 1.10/1.22 => inanimateobject(X) ) ).
% 1.10/1.22
% 1.10/1.22 fof(just64,axiom,
% 1.10/1.22 ! [X] :
% 1.10/1.22 ( inanimateobject(X)
% 1.10/1.22 => isa(X,c_inanimateobject) ) ).
% 1.10/1.22
% 1.10/1.22 % Cyc Constant #117378:
% 1.10/1.22 fof(just65,axiom,
% 1.10/1.22 ! [X] :
% 1.10/1.22 ( isa(X,c_inanimateobject_nonnatural)
% 1.10/1.22 => inanimateobject_nonnatural(X) ) ).
% 1.10/1.22
% 1.10/1.22 fof(just66,axiom,
% 1.10/1.22 ! [X] :
% 1.10/1.22 ( inanimateobject_nonnatural(X)
% 1.10/1.22 => isa(X,c_inanimateobject_nonnatural) ) ).
% 1.10/1.22
% 1.10/1.22 % Cyc Constant #19550:
% 1.10/1.22 fof(just67,axiom,
% 1.10/1.22 ! [SPECMT,GENLMT] :
% 1.10/1.22 ( ( mtvisible(SPECMT)
% 1.10/1.22 & genlmt(SPECMT,GENLMT) )
% 1.10/1.22 => mtvisible(GENLMT) ) ).
% 1.10/1.22
% 1.10/1.22 fof(just68,axiom,
% 1.10/1.22 ! [ARG1,INS] :
% 1.10/1.22 ( genlmt(ARG1,INS)
% 1.10/1.22 => microtheory(INS) ) ).
% 1.10/1.22
% 1.10/1.22 fof(just69,axiom,
% 1.10/1.22 ! [ARG1,INS] :
% 1.10/1.22 ( genlmt(ARG1,INS)
% 1.10/1.22 => microtheory(INS) ) ).
% 1.10/1.22
% 1.10/1.22 fof(just70,axiom,
% 1.10/1.22 ! [INS,ARG2] :
% 1.10/1.22 ( genlmt(INS,ARG2)
% 1.10/1.22 => microtheory(INS) ) ).
% 1.10/1.22
% 1.10/1.22 fof(just71,axiom,
% 1.10/1.22 ! [INS,ARG2] :
% 1.10/1.22 ( genlmt(INS,ARG2)
% 1.10/1.22 => microtheory(INS) ) ).
% 1.10/1.22
% 1.10/1.22 fof(just72,axiom,
% 1.10/1.22 ! [X,Y,Z] :
% 1.10/1.22 ( ( genlmt(X,Y)
% 1.10/1.22 & genlmt(Y,Z) )
% 1.10/1.22 => genlmt(X,Z) ) ).
% 1.10/1.22
% 1.10/1.22 fof(just73,axiom,
% 1.10/1.22 ! [X] :
% 1.10/1.22 ( microtheory(X)
% 1.10/1.22 => genlmt(X,X) ) ).
% 1.10/1.22
% 1.10/1.22 fof(just74,axiom,
% 1.10/1.22 ! [X] :
% 1.10/1.22 ( microtheory(X)
% 1.10/1.22 => genlmt(X,X) ) ).
% 1.10/1.22
% 1.10/1.22 % Cyc Constant #104935:
% 1.10/1.22 fof(just75,axiom,
% 1.10/1.22 ! [X] :
% 1.10/1.22 ( isa(X,c_artifact)
% 1.10/1.22 => artifact(X) ) ).
% 1.10/1.22
% 1.10/1.22 fof(just76,axiom,
% 1.10/1.22 ! [X] :
% 1.10/1.22 ( artifact(X)
% 1.10/1.22 => isa(X,c_artifact) ) ).
% 1.10/1.22
% 1.10/1.22 % Cyc Constant #36435:
% 1.10/1.22 fof(just77,axiom,
% 1.10/1.22 ! [X] :
% 1.10/1.22 ( isa(X,c_partiallytangible)
% 1.10/1.22 => partiallytangible(X) ) ).
% 1.10/1.22
% 1.10/1.22 fof(just78,axiom,
% 1.10/1.22 ! [X] :
% 1.10/1.22 ( partiallytangible(X)
% 1.10/1.22 => isa(X,c_partiallytangible) ) ).
% 1.10/1.22
% 1.10/1.22 % Cyc Constant #78648:
% 1.10/1.22 fof(just79,axiom,
% 1.10/1.22 ! [ARG1,INS] :
% 1.10/1.22 ( disjointwith(ARG1,INS)
% 1.10/1.22 => collection(INS) ) ).
% 1.10/1.22
% 1.10/1.22 fof(just80,axiom,
% 1.10/1.22 ! [INS,ARG2] :
% 1.10/1.22 ( disjointwith(INS,ARG2)
% 1.10/1.22 => collection(INS) ) ).
% 1.10/1.22
% 1.10/1.22 fof(just81,axiom,
% 1.10/1.22 ! [X,Y] :
% 1.10/1.22 ( disjointwith(X,Y)
% 1.10/1.22 => disjointwith(Y,X) ) ).
% 1.10/1.22
% 1.10/1.22 fof(just82,axiom,
% 1.10/1.22 ! [ARG1,OLD,NEW] :
% 1.10/1.22 ( ( disjointwith(ARG1,OLD)
% 1.10/1.22 & genls(NEW,OLD) )
% 1.10/1.22 => disjointwith(ARG1,NEW) ) ).
% 1.10/1.22
% 1.10/1.22 fof(just83,axiom,
% 1.10/1.22 ! [OLD,ARG2,NEW] :
% 1.10/1.22 ( ( disjointwith(OLD,ARG2)
% 1.10/1.22 & genls(NEW,OLD) )
% 1.10/1.22 => disjointwith(NEW,ARG2) ) ).
% 1.10/1.22
% 1.10/1.22 % Cyc Constant #108599:
% 1.10/1.22 fof(just84,axiom,
% 1.10/1.22 ! [X] :
% 1.10/1.22 ( isa(X,c_intangible)
% 1.10/1.22 => intangible(X) ) ).
% 1.10/1.22
% 1.10/1.22 fof(just85,axiom,
% 1.10/1.22 ! [X] :
% 1.10/1.22 ( intangible(X)
% 1.10/1.22 => isa(X,c_intangible) ) ).
% 1.10/1.22
% 1.10/1.22 % Cyc Constant #101351:
% 1.10/1.22 fof(just86,axiom,
% 1.10/1.22 ! [X] :
% 1.18/1.22 ( isa(X,c_mathematicalorcomputationalthing)
% 1.18/1.22 => mathematicalorcomputationalthing(X) ) ).
% 1.18/1.22
% 1.18/1.22 fof(just87,axiom,
% 1.18/1.22 ! [X] :
% 1.18/1.22 ( mathematicalorcomputationalthing(X)
% 1.18/1.22 => isa(X,c_mathematicalorcomputationalthing) ) ).
% 1.18/1.22
% 1.18/1.22 % Cyc Constant #2465:
% 1.18/1.22 fof(just88,axiom,
% 1.18/1.22 ! [X] :
% 1.18/1.22 ( isa(X,c_computerdataartifact)
% 1.18/1.22 => computerdataartifact(X) ) ).
% 1.18/1.22
% 1.18/1.22 fof(just89,axiom,
% 1.18/1.22 ! [X] :
% 1.18/1.22 ( computerdataartifact(X)
% 1.18/1.22 => isa(X,c_computerdataartifact) ) ).
% 1.18/1.22
% 1.18/1.22 % Cyc Constant #129091:
% 1.18/1.22 fof(just90,axiom,
% 1.18/1.22 ! [ARG1] : natfunction(f_urlfn(ARG1),c_urlfn) ).
% 1.18/1.22
% 1.18/1.22 fof(just91,axiom,
% 1.18/1.22 ! [ARG1] : natargument(f_urlfn(ARG1),n_1,ARG1) ).
% 1.18/1.22
% 1.18/1.22 fof(just92,axiom,
% 1.18/1.22 ! [ARG1] : uniformresourcelocator(f_urlfn(ARG1)) ).
% 1.18/1.22
% 1.18/1.22 % Cyc Constant #78971:
% 1.18/1.22 fof(just93,axiom,
% 1.18/1.22 ! [ARG1] : natfunction(f_urlreferentfn(ARG1),c_urlreferentfn) ).
% 1.18/1.22
% 1.18/1.22 fof(just94,axiom,
% 1.18/1.22 ! [ARG1] : natargument(f_urlreferentfn(ARG1),n_1,ARG1) ).
% 1.18/1.22
% 1.18/1.22 fof(just95,axiom,
% 1.18/1.22 ! [ARG1] : computerdataartifact(f_urlreferentfn(ARG1)) ).
% 1.18/1.22
% 1.18/1.22 % Cyc Constant #72115:
% 1.18/1.22 fof(just96,axiom,
% 1.18/1.22 ! [ARG1,INS] :
% 1.18/1.22 ( isa(ARG1,INS)
% 1.18/1.22 => collection(INS) ) ).
% 1.18/1.22
% 1.18/1.22 fof(just97,axiom,
% 1.18/1.22 ! [ARG1,INS] :
% 1.18/1.22 ( isa(ARG1,INS)
% 1.18/1.22 => collection(INS) ) ).
% 1.18/1.22
% 1.18/1.22 fof(just98,axiom,
% 1.18/1.22 ! [INS,ARG2] :
% 1.18/1.22 ( isa(INS,ARG2)
% 1.18/1.22 => thing(INS) ) ).
% 1.18/1.22
% 1.18/1.22 fof(just99,axiom,
% 1.18/1.22 ! [INS,ARG2] :
% 1.18/1.22 ( isa(INS,ARG2)
% 1.18/1.22 => thing(INS) ) ).
% 1.18/1.22
% 1.18/1.22 fof(just100,axiom,
% 1.18/1.22 ! [ARG1,OLD,NEW] :
% 1.18/1.22 ( ( isa(ARG1,OLD)
% 1.18/1.22 & genls(OLD,NEW) )
% 1.18/1.22 => isa(ARG1,NEW) ) ).
% 1.18/1.22
% 1.18/1.22 % Cyc Constant #27757:
% 1.18/1.22 fof(just101,axiom,
% 1.18/1.22 mtvisible(c_basekb) ).
% 1.18/1.22
% 1.18/1.22 % Cyc Constant #89394:
% 1.18/1.22 fof(just102,axiom,
% 1.18/1.22 ! [X] :
% 1.18/1.22 ( isa(X,c_mathematicalthing)
% 1.18/1.22 => mathematicalthing(X) ) ).
% 1.18/1.22
% 1.18/1.22 fof(just103,axiom,
% 1.18/1.22 ! [X] :
% 1.18/1.22 ( mathematicalthing(X)
% 1.18/1.22 => isa(X,c_mathematicalthing) ) ).
% 1.18/1.22
% 1.18/1.22 % Cyc Constant #29216:
% 1.18/1.22 fof(just104,axiom,
% 1.18/1.22 ! [X] :
% 1.18/1.22 ( isa(X,c_setorcollection)
% 1.18/1.22 => setorcollection(X) ) ).
% 1.18/1.22
% 1.18/1.22 fof(just105,axiom,
% 1.18/1.22 ! [X] :
% 1.18/1.22 ( setorcollection(X)
% 1.18/1.22 => isa(X,c_setorcollection) ) ).
% 1.18/1.22
% 1.18/1.22 % Cyc Constant #0:
% 1.18/1.22 fof(just106,axiom,
% 1.18/1.22 ! [ARG1,INS] :
% 1.18/1.22 ( genls(ARG1,INS)
% 1.18/1.22 => collection(INS) ) ).
% 1.18/1.22
% 1.18/1.22 fof(just107,axiom,
% 1.18/1.22 ! [ARG1,INS] :
% 1.18/1.22 ( genls(ARG1,INS)
% 1.18/1.22 => collection(INS) ) ).
% 1.18/1.22
% 1.18/1.22 fof(just108,axiom,
% 1.18/1.22 ! [INS,ARG2] :
% 1.18/1.22 ( genls(INS,ARG2)
% 1.18/1.22 => collection(INS) ) ).
% 1.18/1.22
% 1.18/1.22 fof(just109,axiom,
% 1.18/1.22 ! [INS,ARG2] :
% 1.18/1.22 ( genls(INS,ARG2)
% 1.18/1.22 => collection(INS) ) ).
% 1.18/1.22
% 1.18/1.22 fof(just110,axiom,
% 1.18/1.22 ! [X,Y,Z] :
% 1.18/1.22 ( ( genls(X,Y)
% 1.18/1.22 & genls(Y,Z) )
% 1.18/1.22 => genls(X,Z) ) ).
% 1.18/1.22
% 1.18/1.22 fof(just111,axiom,
% 1.18/1.22 ! [X] :
% 1.18/1.22 ( collection(X)
% 1.18/1.22 => genls(X,X) ) ).
% 1.18/1.22
% 1.18/1.22 fof(just112,axiom,
% 1.18/1.22 ! [X] :
% 1.18/1.22 ( collection(X)
% 1.18/1.22 => genls(X,X) ) ).
% 1.18/1.22
% 1.18/1.23 fof(just113,axiom,
% 1.18/1.23 ! [OLD,ARG2,NEW] :
% 1.18/1.23 ( ( genls(OLD,ARG2)
% 1.18/1.23 & genls(NEW,OLD) )
% 1.18/1.23 => genls(NEW,ARG2) ) ).
% 1.18/1.23
% 1.18/1.23 fof(just114,axiom,
% 1.18/1.23 ! [ARG1,OLD,NEW] :
% 1.18/1.23 ( ( genls(ARG1,OLD)
% 1.18/1.23 & genls(OLD,NEW) )
% 1.18/1.23 => genls(ARG1,NEW) ) ).
% 1.18/1.23
% 1.18/1.23 % Cyc Constant #95028:
% 1.18/1.23 fof(just115,axiom,
% 1.18/1.23 mtvisible(c_universalvocabularymt) ).
% 1.18/1.23
% 1.18/1.23 fof(query63,conjecture,
% 1.18/1.23 ~ disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949) ).
% 1.18/1.23
% 1.18/1.23 %------------------------------------------------------------------------------
% 1.18/1.23 %-------------------------------------------
% 1.18/1.23 % Proof found
% 1.18/1.23 % SZS status Theorem for theBenchmark
% 1.18/1.23 % SZS output start Proof
% 1.18/1.23 %ClaNum:116(EqnAxiom:0)
% 1.18/1.23 %VarNum:243(SingletonVarNum:131)
% 1.18/1.23 %MaxLitNum:3
% 1.18/1.23 %MaxfuncDepth:2
% 1.18/1.23 %SharedTerms:40
% 1.18/1.23 %goalClause: 21
% 1.18/1.23 %singleGoalClaCount:1
% 1.18/1.23 [1]P1(a1)
% 1.18/1.23 [2]P2(a7)
% 1.18/1.23 [3]P2(a2)
% 1.18/1.23 [6]P8(a8,a9)
% 1.18/1.23 [7]P8(a9,a10)
% 1.18/1.23 [8]P8(a10,a11)
% 1.18/1.23 [9]P8(a4,a3)
% 1.18/1.23 [10]P8(a3,a12)
% 1.18/1.23 [11]P8(a12,a13)
% 1.18/1.23 [12]P8(a13,a14)
% 1.18/1.23 [13]P9(a11,a14)
% 1.18/1.23 [14]P10(a7,a2)
% 1.18/1.23 [15]P13(a5,a15)
% 1.18/1.23 [16]P13(a15,a6)
% 1.18/1.23 [17]P4(a6,a8)
% 1.18/1.23 [21]P9(f18(f19(a22)),a16)
% 1.18/1.23 [4]P3(f18(x41))
% 1.18/1.23 [5]P30(f19(x51))
% 1.18/1.23 [19]P21(f19(x191),a20)
% 1.18/1.23 [20]P21(f18(x201),a21)
% 1.18/1.23 [22]P22(f19(x221),a23,x221)
% 1.18/1.23 [23]P22(f18(x231),a23,x231)
% 1.18/1.23 [24]~P23(x241)+P14(x241)
% 1.18/1.23 [25]~P14(x251)+P15(x251)
% 1.18/1.23 [26]~P15(x261)+P16(x261)
% 1.18/1.23 [27]~P17(x271)+P24(x271)
% 1.18/1.23 [28]~P3(x281)+P5(x281)
% 1.18/1.23 [29]~P5(x291)+P18(x291)
% 1.18/1.23 [30]~P18(x301)+P17(x301)
% 1.18/1.23 [31]~P24(x311)+~P16(x311)
% 1.18/1.23 [32]~P23(x321)+P19(x321,a8)
% 1.18/1.23 [33]~P14(x331)+P19(x331,a9)
% 1.18/1.23 [34]~P15(x341)+P19(x341,a10)
% 1.18/1.23 [35]~P16(x351)+P19(x351,a11)
% 1.18/1.23 [36]~P24(x361)+P19(x361,a14)
% 1.18/1.23 [37]~P3(x371)+P19(x371,a4)
% 1.18/1.23 [38]~P5(x381)+P19(x381,a3)
% 1.18/1.23 [39]~P18(x391)+P19(x391,a12)
% 1.18/1.23 [40]~P17(x401)+P19(x401,a13)
% 1.18/1.23 [41]~P1(x411)+P19(x411,a17)
% 1.18/1.23 [43]~P6(x431)+P8(x431,x431)
% 1.18/1.23 [45]~P20(x451)+P10(x451,x451)
% 1.18/1.23 [47]~P26(x471)+P13(x471,x471)
% 1.18/1.23 [48]P23(x481)+~P19(x481,a8)
% 1.18/1.23 [49]P14(x491)+~P19(x491,a9)
% 1.18/1.23 [50]P3(x501)+~P19(x501,a4)
% 1.18/1.23 [51]P15(x511)+~P19(x511,a10)
% 1.18/1.23 [52]P16(x521)+~P19(x521,a11)
% 1.18/1.23 [53]P24(x531)+~P19(x531,a14)
% 1.18/1.23 [54]P5(x541)+~P19(x541,a3)
% 1.18/1.23 [55]P18(x551)+~P19(x551,a12)
% 1.18/1.23 [56]P17(x561)+~P19(x561,a13)
% 1.18/1.23 [57]P1(x571)+~P19(x571,a17)
% 1.18/1.23 [58]P23(x581)+~P25(x582,x581)
% 1.18/1.23 [61]P23(x611)+~P11(x612,x611)
% 1.18/1.23 [62]P23(x621)+~P25(x621,x622)
% 1.18/1.23 [64]P23(x641)+~P11(x641,x642)
% 1.18/1.23 [66]P6(x661)+~P8(x662,x661)
% 1.18/1.23 [67]P6(x671)+~P9(x672,x671)
% 1.18/1.23 [69]P6(x691)+~P19(x692,x691)
% 1.18/1.23 [70]P6(x701)+~P4(x702,x701)
% 1.18/1.23 [72]P6(x721)+~P8(x721,x722)
% 1.18/1.23 [73]P6(x731)+~P9(x731,x732)
% 1.18/1.23 [74]P27(x741)+~P4(x741,x742)
% 1.18/1.23 [76]P26(x761)+~P13(x762,x761)
% 1.18/1.23 [78]P26(x781)+~P13(x781,x782)
% 1.18/1.23 [79]P7(x791)+~P12(x792,x791)
% 1.18/1.23 [80]P7(x801)+~P12(x801,x802)
% 1.18/1.23 [82]P20(x821)+~P10(x822,x821)
% 1.18/1.23 [84]P20(x841)+~P10(x841,x842)
% 1.18/1.23 [86]P28(x861)+~P19(x861,x862)
% 1.18/1.23 [88]~P9(x882,x881)+P9(x881,x882)
% 1.18/1.23 [89]~P25(x892,x891)+P25(x891,x892)
% 1.18/1.23 [90]~P9(x901,x902)+P25(x901,x902)
% 1.18/1.23 [91]~P25(x911,x912)+P11(x911,x912)
% 1.18/1.23 [87]~P10(x872,x871)+P2(x871)+~P2(x872)
% 1.18/1.23 [94]~P8(x941,x943)+P8(x941,x942)+~P8(x943,x942)
% 1.18/1.23 [95]~P9(x953,x952)+P9(x951,x952)+~P8(x951,x953)
% 1.18/1.23 [96]~P9(x961,x963)+P9(x961,x962)+~P8(x962,x963)
% 1.18/1.23 [97]~P10(x971,x973)+P10(x971,x972)+~P10(x973,x972)
% 1.18/1.23 [98]~P19(x981,x983)+P19(x981,x982)+~P8(x983,x982)
% 1.18/1.23 [99]~P13(x991,x993)+P12(x991,x992)+~P12(x993,x992)
% 1.18/1.23 [100]~P13(x1003,x1002)+P12(x1001,x1002)+~P12(x1001,x1003)
% 1.18/1.23 [103]~P12(x1031,x1033)+P13(x1031,x1032)+~P12(x1033,x1032)
% 1.18/1.23 [104]~P13(x1041,x1043)+P13(x1041,x1042)+~P13(x1043,x1042)
% 1.18/1.23 [105]~P25(x1053,x1052)+P25(x1051,x1052)+~P8(x1051,x1053)
% 1.18/1.23 [107]~P29(x1071,x1073)+P25(x1071,x1072)+~P25(x1073,x1072)
% 1.18/1.23 [108]~P25(x1081,x1083)+P25(x1081,x1082)+~P8(x1082,x1083)
% 1.18/1.23 [110]~P29(x1102,x1103)+P25(x1101,x1102)+~P25(x1101,x1103)
% 1.18/1.23 [111]~P29(x1112,x1113)+P11(x1111,x1112)+~P11(x1111,x1113)
% 1.18/1.23 [113]~P4(x1131,x1133)+P4(x1131,x1132)+~P8(x1133,x1132)
% 1.18/1.23 [116]~P19(x1163,x1161)+~P9(x1161,x1162)+~P19(x1163,x1162)
% 1.18/1.23 %EqnAxiom
% 1.18/1.23
% 1.18/1.23 %-------------------------------------------
% 1.18/1.23 cnf(509,plain,
% 1.18/1.23 (~P15(x5091)+~P24(x5091)),
% 1.18/1.23 inference(scs_inference,[],[26,31])).
% 1.18/1.23 cnf(759,plain,
% 1.18/1.23 (P24(x7591)+~P18(x7591)),
% 1.18/1.23 inference(scs_inference,[],[30,27])).
% 1.18/1.23 cnf(762,plain,
% 1.18/1.23 (P24(x7621)+~P5(x7621)),
% 1.18/1.23 inference(scs_inference,[],[759,29])).
% 1.18/1.23 cnf(763,plain,
% 1.18/1.23 (P24(f18(x7631))),
% 1.18/1.23 inference(scs_inference,[],[4,762,28])).
% 1.18/1.23 cnf(778,plain,
% 1.18/1.23 ($false),
% 1.18/1.23 inference(scs_inference,[],[21,763,509,25,24,62,64,61,58,90]),
% 1.18/1.23 ['proof']).
% 1.18/1.23 % SZS output end Proof
% 1.18/1.23 % Total time :0.580000s
%------------------------------------------------------------------------------