%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CSR060+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 : n028.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:51 EDT 2024
% Result : Theorem 0.55s 0.78s
% Output : CNFRefutation 0.55s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : CSR060+1 : TPTP v8.2.0. Released v3.4.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n028.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed Jun 19 21:50:38 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.52/0.56 start to proof:theBenchmark
% 0.55/0.76 %-------------------------------------------
% 0.55/0.76 % File :CSE---1.7
% 0.55/0.76 % Problem :theBenchmark
% 0.55/0.76 % Transform :cnf
% 0.55/0.76 % Format :tptp:raw
% 0.55/0.76 % Command :java -jar mcs_scs.jar %d %s
% 0.55/0.76
% 0.55/0.76 % Result :Theorem 0.150000s
% 0.55/0.76 % Output :CNFRefutation 0.150000s
% 0.55/0.76 %-------------------------------------------
% 0.55/0.76 %------------------------------------------------------------------------------
% 0.55/0.76 % File : CSR060+1 : TPTP v8.2.0. Released v3.4.0.
% 0.55/0.76 % Domain : Common Sense Reasoning
% 0.55/0.76 % Problem : Autogenerated Cyc Problem CSR060+1
% 0.55/0.76 % Version : Especial.
% 0.55/0.76 % English :
% 0.55/0.76
% 0.55/0.76 % Refs : [RS+] Reagan Smith et al., The Cyc TPTP Challenge Problem
% 0.55/0.76 % Source : [RS+]
% 0.55/0.76 % Names :
% 0.55/0.76
% 0.55/0.76 % Status : Theorem
% 0.55/0.76 % Rating : 0.00 v6.1.0, 0.04 v6.0.0, 0.25 v5.5.0, 0.17 v5.3.0, 0.26 v5.2.0, 0.14 v5.0.0, 0.20 v4.1.0, 0.17 v4.0.1, 0.16 v4.0.0, 0.15 v3.7.0, 0.00 v3.4.0
% 0.55/0.76 % Syntax : Number of formulae : 95 ( 37 unt; 0 def)
% 0.55/0.76 % Number of atoms : 170 ( 0 equ)
% 0.55/0.76 % Maximal formula atoms : 3 ( 1 avg)
% 0.55/0.76 % Number of connectives : 77 ( 2 ~; 0 |; 18 &)
% 0.55/0.76 % ( 0 <=>; 57 =>; 0 <=; 0 <~>)
% 0.55/0.76 % Maximal formula depth : 7 ( 4 avg)
% 0.55/0.76 % Maximal term depth : 4 ( 1 avg)
% 0.55/0.76 % Number of predicates : 32 ( 32 usr; 0 prp; 1-3 aty)
% 0.55/0.77 % Number of functors : 33 ( 33 usr; 28 con; 0-4 aty)
% 0.55/0.77 % Number of variables : 172 ( 171 !; 1 ?)
% 0.55/0.77 % SPC : FOF_THM_RFO_NEQ
% 0.55/0.77
% 0.55/0.77 % Comments : Autogenerated from the OpenCyc KB. Documentation can be found at
% 0.55/0.77 % http://opencyc.org/doc/#TPTP_Challenge_Problem_Set
% 0.55/0.77 % : Cyc(R) Knowledge Base Copyright(C) 1995-2007 Cycorp, Inc., Austin,
% 0.55/0.77 % TX, USA. All rights reserved.
% 0.55/0.77 % : OpenCyc Knowledge Base Copyright(C) 2001-2007 Cycorp, Inc.,
% 0.55/0.77 % Austin, TX, USA. All rights reserved.
% 0.55/0.77 %------------------------------------------------------------------------------
% 0.55/0.77 %$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])
% 0.55/0.77 %$static(cyc_scaling_1,include('Axioms/CSR002+0.ax'))
% 0.55/0.77 %----Empty file include('Axioms/CSR002+0.ax').
% 0.55/0.77 %------------------------------------------------------------------------------
% 0.55/0.77 % Cyc Assertion #518539:
% 0.55/0.77 fof(just1,axiom,
% 0.55/0.77 genlmt(c_ldscdemonstrationspindleheadmt,c_currentworlddatacollectormt_nonhomocentric) ).
% 0.55/0.77
% 0.55/0.77 % Cyc Assertion #592971:
% 0.55/0.77 fof(just2,axiom,
% 0.55/0.77 genlmt(c_cycorpproductsmt,c_basekb) ).
% 0.55/0.77
% 0.55/0.77 % Cyc Assertion #600900:
% 0.55/0.77 fof(just3,axiom,
% 0.55/0.77 genlmt(c_cycnounlearnermt,c_cycorpproductsmt) ).
% 0.55/0.77
% 0.55/0.77 % Cyc Assertion #665043:
% 0.55/0.77 fof(just4,axiom,
% 0.55/0.77 genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885),c_machinelearningspindleheadmt) ).
% 0.55/0.77
% 0.55/0.77 % Cyc Assertion #964779:
% 0.55/0.77 fof(just5,axiom,
% 0.55/0.77 genlmt(c_machinelearningspindleheadmt,c_miptdatabase19681997_termsmt) ).
% 0.55/0.77
% 0.55/0.77 % Cyc Assertion #976441:
% 0.55/0.77 fof(just6,axiom,
% 0.55/0.77 ! [TERM,INDEPCOL,PRED,DEPCOL] :
% 0.55/0.77 ( ( isa(TERM,INDEPCOL)
% 0.55/0.77 & relationexistsall(PRED,DEPCOL,INDEPCOL) )
% 0.55/0.77 => isa(f_relationexistsallfn(TERM,PRED,DEPCOL,INDEPCOL),DEPCOL) ) ).
% 0.55/0.77
% 0.55/0.77 fof(just7,axiom,
% 0.55/0.77 resultisaarg(c_relationexistsallfn,n_3) ).
% 0.55/0.77
% 0.55/0.77 % Cyc Assertion #1028120:
% 0.55/0.77 fof(just8,axiom,
% 0.55/0.77 genlmt(c_miptdatabase19681997_termsmt,c_ldscgeneralcollectormt) ).
% 0.55/0.77
% 0.55/0.77 % Cyc Assertion #1103756:
% 0.55/0.77 fof(just9,axiom,
% 0.55/0.77 genlmt(c_ldscgeneralcollectormt,c_ldscdemonstrationspindleheadmt) ).
% 0.55/0.77
% 0.55/0.77 % Cyc Assertion #1322220:
% 0.55/0.77 fof(just10,axiom,
% 0.55/0.77 transitivebinarypredicate(c_genlmt) ).
% 0.55/0.77
% 0.55/0.77 % Cyc Assertion #1614635:
% 0.55/0.77 fof(just11,axiom,
% 0.55/0.77 genlmt(c_machinelearningspindleheadmt,c_cycnounlearnermt) ).
% 0.55/0.77
% 0.55/0.77 % Cyc Assertion #1650755:
% 0.55/0.77 fof(just12,axiom,
% 0.55/0.77 genlmt(c_basekb,c_universalvocabularymt) ).
% 0.55/0.77
% 0.55/0.77 % Cyc Assertion #2188322:
% 0.55/0.77 fof(just13,axiom,
% 0.55/0.77 ! [TERM] :
% 0.55/0.77 ( ( mtvisible(c_currentworlddatacollectormt_nonhomocentric)
% 0.55/0.77 & isa(TERM,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)) )
% 0.55/0.77 => tptp_9_51(f_relationexistsallfn(TERM,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),TERM) ) ).
% 0.55/0.77
% 0.55/0.77 fof(just14,axiom,
% 0.55/0.77 ( mtvisible(c_currentworlddatacollectormt_nonhomocentric)
% 0.55/0.77 => relationexistsall(c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)) ) ).
% 0.55/0.77
% 0.55/0.77 % Cyc Assertion #2283540:
% 0.55/0.77 fof(just15,axiom,
% 0.55/0.77 isa(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)) ).
% 0.55/0.77
% 0.55/0.77 fof(just16,axiom,
% 0.55/0.77 subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802) ).
% 0.55/0.77
% 0.55/0.77 % Cyc Assertion #398814:
% 0.55/0.77 fof(just17,axiom,
% 0.55/0.77 ! [OBJ,COL1,COL2] :
% 0.55/0.77 ~ ( isa(OBJ,COL1)
% 0.55/0.77 & isa(OBJ,COL2)
% 0.55/0.77 & disjointwith(COL1,COL2) ) ).
% 0.55/0.77
% 0.55/0.77 % Cyc Assertion #831913:
% 0.55/0.77 fof(just18,axiom,
% 0.55/0.77 ! [SPECPRED,PRED,GENLPRED] :
% 0.55/0.77 ( ( genlinverse(SPECPRED,PRED)
% 0.55/0.77 & genlinverse(PRED,GENLPRED) )
% 0.55/0.77 => genlpreds(SPECPRED,GENLPRED) ) ).
% 0.55/0.77
% 0.55/0.77 % Cyc Constant #40273:
% 0.55/0.77 fof(just19,axiom,
% 0.55/0.77 ! [ARG1,INS] :
% 0.55/0.77 ( genlpreds(ARG1,INS)
% 0.55/0.77 => predicate(INS) ) ).
% 0.55/0.77
% 0.55/0.77 fof(just20,axiom,
% 0.55/0.77 ! [ARG1,INS] :
% 0.55/0.77 ( genlpreds(ARG1,INS)
% 0.55/0.77 => predicate(INS) ) ).
% 0.55/0.77
% 0.55/0.77 fof(just21,axiom,
% 0.55/0.77 ! [INS,ARG2] :
% 0.55/0.77 ( genlpreds(INS,ARG2)
% 0.55/0.77 => predicate(INS) ) ).
% 0.55/0.77
% 0.55/0.77 fof(just22,axiom,
% 0.55/0.77 ! [INS,ARG2] :
% 0.55/0.77 ( genlpreds(INS,ARG2)
% 0.55/0.77 => predicate(INS) ) ).
% 0.55/0.77
% 0.55/0.77 fof(just23,axiom,
% 0.55/0.77 ! [X,Y,Z] :
% 0.55/0.77 ( ( genlpreds(X,Y)
% 0.55/0.77 & genlpreds(Y,Z) )
% 0.55/0.77 => genlpreds(X,Z) ) ).
% 0.55/0.77
% 0.55/0.77 fof(just24,axiom,
% 0.55/0.77 ! [X] :
% 0.55/0.77 ( predicate(X)
% 0.55/0.77 => genlpreds(X,X) ) ).
% 0.55/0.77
% 0.55/0.77 fof(just25,axiom,
% 0.55/0.77 ! [X] :
% 0.55/0.77 ( predicate(X)
% 0.55/0.77 => genlpreds(X,X) ) ).
% 0.55/0.77
% 0.55/0.77 % Cyc Constant #45259:
% 0.55/0.77 fof(just26,axiom,
% 0.55/0.77 ! [ARG1,INS] :
% 0.55/0.77 ( genlinverse(ARG1,INS)
% 0.55/0.77 => binarypredicate(INS) ) ).
% 0.55/0.77
% 0.55/0.77 fof(just27,axiom,
% 0.55/0.77 ! [INS,ARG2] :
% 0.55/0.77 ( genlinverse(INS,ARG2)
% 0.55/0.77 => binarypredicate(INS) ) ).
% 0.55/0.77
% 0.55/0.77 fof(just28,axiom,
% 0.55/0.77 ! [OLD,ARG2,NEW] :
% 0.55/0.77 ( ( genlinverse(OLD,ARG2)
% 0.55/0.77 & genlpreds(NEW,OLD) )
% 0.55/0.77 => genlinverse(NEW,ARG2) ) ).
% 0.55/0.77
% 0.55/0.77 fof(just29,axiom,
% 0.55/0.77 ! [ARG1,OLD,NEW] :
% 0.55/0.77 ( ( genlinverse(ARG1,OLD)
% 0.55/0.77 & genlpreds(OLD,NEW) )
% 0.55/0.77 => genlinverse(ARG1,NEW) ) ).
% 0.55/0.77
% 0.55/0.77 % Cyc Constant #78648:
% 0.55/0.77 fof(just30,axiom,
% 0.55/0.77 ! [ARG1,INS] :
% 0.55/0.77 ( disjointwith(ARG1,INS)
% 0.55/0.77 => collection(INS) ) ).
% 0.55/0.77
% 0.55/0.77 fof(just31,axiom,
% 0.55/0.77 ! [INS,ARG2] :
% 0.55/0.77 ( disjointwith(INS,ARG2)
% 0.55/0.77 => collection(INS) ) ).
% 0.55/0.77
% 0.55/0.77 fof(just32,axiom,
% 0.55/0.77 ! [X,Y] :
% 0.55/0.77 ( disjointwith(X,Y)
% 0.55/0.77 => disjointwith(Y,X) ) ).
% 0.55/0.77
% 0.55/0.77 fof(just33,axiom,
% 0.55/0.77 ! [ARG1,OLD,NEW] :
% 0.55/0.77 ( ( disjointwith(ARG1,OLD)
% 0.55/0.77 & genls(NEW,OLD) )
% 0.55/0.77 => disjointwith(ARG1,NEW) ) ).
% 0.55/0.77
% 0.55/0.77 fof(just34,axiom,
% 0.55/0.77 ! [OLD,ARG2,NEW] :
% 0.55/0.77 ( ( disjointwith(OLD,ARG2)
% 0.55/0.77 & genls(NEW,OLD) )
% 0.55/0.77 => disjointwith(NEW,ARG2) ) ).
% 0.55/0.77
% 0.55/0.77 % Cyc Constant #66840:
% 0.55/0.77 fof(just35,axiom,
% 0.55/0.77 ! [ARG1,INS] :
% 0.55/0.77 ( objectfoundinlocation(ARG1,INS)
% 0.55/0.77 => spatialthing_nonsituational(INS) ) ).
% 0.55/0.77
% 0.55/0.77 fof(just36,axiom,
% 0.55/0.77 ! [ARG1,INS] :
% 0.55/0.77 ( objectfoundinlocation(ARG1,INS)
% 0.55/0.77 => spatialthing_localized(INS) ) ).
% 0.55/0.77
% 0.55/0.77 fof(just37,axiom,
% 0.55/0.77 ! [INS,ARG2] :
% 0.55/0.77 ( objectfoundinlocation(INS,ARG2)
% 0.55/0.77 => spatialthing_nonsituational(INS) ) ).
% 0.55/0.77
% 0.55/0.77 fof(just38,axiom,
% 0.55/0.77 ! [INS,ARG2] :
% 0.55/0.77 ( objectfoundinlocation(INS,ARG2)
% 0.55/0.77 => spatialthing_localized(INS) ) ).
% 0.55/0.77
% 0.55/0.77 fof(just39,axiom,
% 0.55/0.77 ! [X,Y,Z] :
% 0.55/0.77 ( ( objectfoundinlocation(X,Y)
% 0.55/0.77 & objectfoundinlocation(Y,Z) )
% 0.55/0.77 => objectfoundinlocation(X,Z) ) ).
% 0.55/0.77
% 0.55/0.77 fof(just40,axiom,
% 0.55/0.77 ! [X] : ~ objectfoundinlocation(X,X) ).
% 0.55/0.77
% 0.55/0.77 fof(just41,axiom,
% 0.55/0.77 ! [ARG1,OLD,NEW] :
% 0.55/0.77 ( ( objectfoundinlocation(ARG1,OLD)
% 0.55/0.77 & geopoliticalsubdivision(NEW,OLD) )
% 0.55/0.77 => objectfoundinlocation(ARG1,NEW) ) ).
% 0.55/0.77
% 0.55/0.77 fof(just42,axiom,
% 0.55/0.77 ! [ARG1,OLD,NEW] :
% 0.55/0.77 ( ( objectfoundinlocation(ARG1,OLD)
% 0.55/0.77 & geographicallysubsumes(NEW,OLD) )
% 0.55/0.77 => objectfoundinlocation(ARG1,NEW) ) ).
% 0.55/0.77
% 0.55/0.77 fof(just43,axiom,
% 0.55/0.77 ! [ARG1,OLD,NEW] :
% 0.55/0.77 ( ( objectfoundinlocation(ARG1,OLD)
% 0.55/0.77 & subregions(NEW,OLD) )
% 0.55/0.77 => objectfoundinlocation(ARG1,NEW) ) ).
% 0.55/0.77
% 0.55/0.78 % Cyc Constant #54624:
% 0.55/0.78 fof(just44,axiom,
% 0.55/0.78 ! [X] :
% 0.55/0.78 ( isa(X,c_ship)
% 0.55/0.78 => ship(X) ) ).
% 0.55/0.78
% 0.55/0.78 fof(just45,axiom,
% 0.55/0.78 ! [X] :
% 0.55/0.78 ( ship(X)
% 0.55/0.78 => isa(X,c_ship) ) ).
% 0.55/0.78
% 0.55/0.78 % Cyc Constant #93912:
% 0.55/0.78 fof(just46,axiom,
% 0.55/0.78 ! [ARG1,ARG2,ARG3] : natfunction(f_subcollectionofwithrelationtofn(ARG1,ARG2,ARG3),c_subcollectionofwithrelationtofn) ).
% 0.55/0.78
% 0.55/0.78 fof(just47,axiom,
% 0.55/0.78 ! [ARG1,ARG2,ARG3] : natargument(f_subcollectionofwithrelationtofn(ARG1,ARG2,ARG3),n_1,ARG1) ).
% 0.55/0.78
% 0.55/0.78 fof(just48,axiom,
% 0.55/0.78 ! [ARG1,ARG2,ARG3] : natargument(f_subcollectionofwithrelationtofn(ARG1,ARG2,ARG3),n_2,ARG2) ).
% 0.55/0.78
% 0.55/0.78 fof(just49,axiom,
% 0.55/0.78 ! [ARG1,ARG2,ARG3] : natargument(f_subcollectionofwithrelationtofn(ARG1,ARG2,ARG3),n_3,ARG3) ).
% 0.55/0.78
% 0.55/0.78 fof(just50,axiom,
% 0.55/0.78 ! [ARG1,ARG2,ARG3] : collection(f_subcollectionofwithrelationtofn(ARG1,ARG2,ARG3)) ).
% 0.55/0.78
% 0.55/0.78 % Cyc NART #11809:
% 0.55/0.78 fof(just51,axiom,
% 0.55/0.78 ! [X] :
% 0.55/0.78 ( isa(X,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))
% 0.55/0.78 => subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(X) ) ).
% 0.55/0.78
% 0.55/0.78 fof(just52,axiom,
% 0.55/0.78 ! [X] :
% 0.55/0.78 ( subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(X)
% 0.55/0.78 => isa(X,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)) ) ).
% 0.55/0.78
% 0.55/0.78 % Cyc Constant #156786:
% 0.55/0.78 fof(just53,axiom,
% 0.55/0.78 ! [X] :
% 0.55/0.78 ( isa(X,c_tptpcol_16_27189)
% 0.55/0.78 => tptpcol_16_27189(X) ) ).
% 0.55/0.78
% 0.55/0.78 fof(just54,axiom,
% 0.55/0.78 ! [X] :
% 0.55/0.78 ( tptpcol_16_27189(X)
% 0.55/0.78 => isa(X,c_tptpcol_16_27189) ) ).
% 0.55/0.78
% 0.55/0.78 % Cyc Constant #262034:
% 0.55/0.78 fof(just55,axiom,
% 0.55/0.78 ! [ARG1,INS] :
% 0.55/0.78 ( tptp_9_51(ARG1,INS)
% 0.55/0.78 => subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(INS) ) ).
% 0.55/0.78
% 0.55/0.78 fof(just56,axiom,
% 0.55/0.78 ! [INS,ARG2] :
% 0.55/0.78 ( tptp_9_51(INS,ARG2)
% 0.55/0.78 => tptpcol_7_26628(INS) ) ).
% 0.55/0.78
% 0.55/0.78 % Cyc Constant #77435:
% 0.55/0.78 fof(just57,axiom,
% 0.55/0.78 ! [ARG1,ARG2,INS] :
% 0.55/0.78 ( relationexistsall(ARG1,ARG2,INS)
% 0.55/0.78 => collection(INS) ) ).
% 0.55/0.78
% 0.55/0.78 fof(just58,axiom,
% 0.55/0.78 ! [ARG1,INS,ARG3] :
% 0.55/0.78 ( relationexistsall(ARG1,INS,ARG3)
% 0.55/0.78 => collection(INS) ) ).
% 0.55/0.78
% 0.55/0.78 fof(just59,axiom,
% 0.55/0.78 ! [INS,ARG2,ARG3] :
% 0.55/0.78 ( relationexistsall(INS,ARG2,ARG3)
% 0.55/0.78 => binarypredicate(INS) ) ).
% 0.55/0.78
% 0.55/0.78 % Cyc Constant #127156:
% 0.55/0.78 fof(just60,axiom,
% 0.55/0.78 ! [X] :
% 0.55/0.78 ( isa(X,c_transitivebinarypredicate)
% 0.55/0.78 => transitivebinarypredicate(X) ) ).
% 0.55/0.78
% 0.55/0.78 fof(just61,axiom,
% 0.55/0.78 ! [X] :
% 0.55/0.78 ( transitivebinarypredicate(X)
% 0.55/0.78 => isa(X,c_transitivebinarypredicate) ) ).
% 0.55/0.78
% 0.55/0.78 % Cyc Constant #72115:
% 0.55/0.78 fof(just62,axiom,
% 0.55/0.78 ! [ARG1,INS] :
% 0.55/0.78 ( isa(ARG1,INS)
% 0.55/0.78 => collection(INS) ) ).
% 0.55/0.78
% 0.55/0.78 fof(just63,axiom,
% 0.55/0.78 ! [ARG1,INS] :
% 0.55/0.78 ( isa(ARG1,INS)
% 0.55/0.78 => collection(INS) ) ).
% 0.55/0.78
% 0.55/0.78 fof(just64,axiom,
% 0.55/0.78 ! [INS,ARG2] :
% 0.55/0.78 ( isa(INS,ARG2)
% 0.55/0.78 => thing(INS) ) ).
% 0.55/0.78
% 0.55/0.78 fof(just65,axiom,
% 0.55/0.78 ! [INS,ARG2] :
% 0.55/0.78 ( isa(INS,ARG2)
% 0.55/0.78 => thing(INS) ) ).
% 0.55/0.78
% 0.55/0.78 fof(just66,axiom,
% 0.55/0.78 ! [ARG1,OLD,NEW] :
% 0.55/0.78 ( ( isa(ARG1,OLD)
% 0.55/0.78 & genls(OLD,NEW) )
% 0.55/0.78 => isa(ARG1,NEW) ) ).
% 0.55/0.78
% 0.55/0.78 % Cyc Constant #109289:
% 0.55/0.78 fof(just67,axiom,
% 0.55/0.78 ! [ARG1,ARG2,ARG3,ARG4] : natfunction(f_relationexistsallfn(ARG1,ARG2,ARG3,ARG4),c_relationexistsallfn) ).
% 0.55/0.78
% 0.55/0.78 fof(just68,axiom,
% 0.55/0.78 ! [ARG1,ARG2,ARG3,ARG4] : natargument(f_relationexistsallfn(ARG1,ARG2,ARG3,ARG4),n_1,ARG1) ).
% 0.55/0.78
% 0.55/0.78 fof(just69,axiom,
% 0.55/0.78 ! [ARG1,ARG2,ARG3,ARG4] : natargument(f_relationexistsallfn(ARG1,ARG2,ARG3,ARG4),n_2,ARG2) ).
% 0.55/0.78
% 0.55/0.78 fof(just70,axiom,
% 0.55/0.78 ! [ARG1,ARG2,ARG3,ARG4] : natargument(f_relationexistsallfn(ARG1,ARG2,ARG3,ARG4),n_3,ARG3) ).
% 0.55/0.78
% 0.55/0.78 fof(just71,axiom,
% 0.55/0.78 ! [ARG1,ARG2,ARG3,ARG4] : natargument(f_relationexistsallfn(ARG1,ARG2,ARG3,ARG4),n_4,ARG4) ).
% 0.55/0.78
% 0.55/0.78 fof(just72,axiom,
% 0.55/0.78 ! [ARG1,ARG2,ARG3,ARG4] : thing(f_relationexistsallfn(ARG1,ARG2,ARG3,ARG4)) ).
% 0.55/0.78
% 0.55/0.78 % Cyc Constant #97397:
% 0.55/0.78 fof(just73,axiom,
% 0.55/0.78 ! [ARG1,INS] :
% 0.55/0.78 ( resultisaarg(ARG1,INS)
% 0.55/0.78 => positiveinteger(INS) ) ).
% 0.55/0.78
% 0.55/0.78 fof(just74,axiom,
% 0.55/0.78 ! [INS,ARG2] :
% 0.55/0.78 ( resultisaarg(INS,ARG2)
% 0.55/0.78 => function_denotational(INS) ) ).
% 0.55/0.78
% 0.55/0.78 % Cyc Constant #129091:
% 0.55/0.78 fof(just75,axiom,
% 0.55/0.78 ! [ARG1] : natfunction(f_urlfn(ARG1),c_urlfn) ).
% 0.55/0.78
% 0.55/0.78 fof(just76,axiom,
% 0.55/0.78 ! [ARG1] : natargument(f_urlfn(ARG1),n_1,ARG1) ).
% 0.55/0.78
% 0.55/0.78 fof(just77,axiom,
% 0.55/0.78 ! [ARG1] : uniformresourcelocator(f_urlfn(ARG1)) ).
% 0.55/0.78
% 0.55/0.78 % Cyc Constant #78971:
% 0.55/0.78 fof(just78,axiom,
% 0.55/0.78 ! [ARG1] : natfunction(f_urlreferentfn(ARG1),c_urlreferentfn) ).
% 0.55/0.78
% 0.55/0.78 fof(just79,axiom,
% 0.55/0.78 ! [ARG1] : natargument(f_urlreferentfn(ARG1),n_1,ARG1) ).
% 0.55/0.78
% 0.55/0.78 fof(just80,axiom,
% 0.55/0.78 ! [ARG1] : computerdataartifact(f_urlreferentfn(ARG1)) ).
% 0.55/0.78
% 0.55/0.78 % Cyc Constant #71728:
% 0.55/0.78 fof(just81,axiom,
% 0.55/0.78 ! [ARG1,ARG2] : natfunction(f_contentmtofcdafromeventfn(ARG1,ARG2),c_contentmtofcdafromeventfn) ).
% 0.55/0.78
% 0.55/0.78 fof(just82,axiom,
% 0.55/0.78 ! [ARG1,ARG2] : natargument(f_contentmtofcdafromeventfn(ARG1,ARG2),n_1,ARG1) ).
% 0.55/0.78
% 0.55/0.78 fof(just83,axiom,
% 0.55/0.78 ! [ARG1,ARG2] : natargument(f_contentmtofcdafromeventfn(ARG1,ARG2),n_2,ARG2) ).
% 0.55/0.78
% 0.55/0.78 fof(just84,axiom,
% 0.55/0.78 ! [ARG1,ARG2] : microtheory(f_contentmtofcdafromeventfn(ARG1,ARG2)) ).
% 0.55/0.78
% 0.55/0.78 % Cyc Constant #27757:
% 0.55/0.78 fof(just85,axiom,
% 0.55/0.78 mtvisible(c_basekb) ).
% 0.55/0.78
% 0.55/0.78 % Cyc Constant #19550:
% 0.55/0.78 fof(just86,axiom,
% 0.55/0.78 ! [SPECMT,GENLMT] :
% 0.55/0.78 ( ( mtvisible(SPECMT)
% 0.55/0.78 & genlmt(SPECMT,GENLMT) )
% 0.55/0.78 => mtvisible(GENLMT) ) ).
% 0.55/0.78
% 0.55/0.78 fof(just87,axiom,
% 0.55/0.78 ! [ARG1,INS] :
% 0.55/0.78 ( genlmt(ARG1,INS)
% 0.55/0.78 => microtheory(INS) ) ).
% 0.55/0.78
% 0.55/0.78 fof(just88,axiom,
% 0.55/0.78 ! [ARG1,INS] :
% 0.55/0.78 ( genlmt(ARG1,INS)
% 0.55/0.78 => microtheory(INS) ) ).
% 0.55/0.78
% 0.55/0.78 fof(just89,axiom,
% 0.55/0.78 ! [INS,ARG2] :
% 0.55/0.78 ( genlmt(INS,ARG2)
% 0.55/0.78 => microtheory(INS) ) ).
% 0.55/0.78
% 0.55/0.78 fof(just90,axiom,
% 0.55/0.78 ! [INS,ARG2] :
% 0.55/0.78 ( genlmt(INS,ARG2)
% 0.55/0.78 => microtheory(INS) ) ).
% 0.55/0.78
% 0.55/0.78 fof(just91,axiom,
% 0.55/0.78 ! [X,Y,Z] :
% 0.55/0.78 ( ( genlmt(X,Y)
% 0.55/0.78 & genlmt(Y,Z) )
% 0.55/0.78 => genlmt(X,Z) ) ).
% 0.55/0.78
% 0.55/0.78 fof(just92,axiom,
% 0.55/0.78 ! [X] :
% 0.55/0.78 ( microtheory(X)
% 0.55/0.78 => genlmt(X,X) ) ).
% 0.55/0.78
% 0.55/0.78 fof(just93,axiom,
% 0.55/0.78 ! [X] :
% 0.55/0.78 ( microtheory(X)
% 0.55/0.78 => genlmt(X,X) ) ).
% 0.55/0.78
% 0.55/0.78 % Cyc Constant #95028:
% 0.55/0.78 fof(just94,axiom,
% 0.55/0.78 mtvisible(c_universalvocabularymt) ).
% 0.55/0.78
% 0.55/0.78 fof(query60,conjecture,
% 0.55/0.78 ? [X] :
% 0.55/0.78 ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885))
% 0.55/0.78 => ( tptp_9_51(X,c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802)
% 0.55/0.78 & tptpcol_16_27189(X) ) ) ).
% 0.55/0.78
% 0.55/0.78 %------------------------------------------------------------------------------
% 0.55/0.78 %-------------------------------------------
% 0.55/0.78 % Proof found
% 0.55/0.78 % SZS status Theorem for theBenchmark
% 0.55/0.78 % SZS output start Proof
% 0.55/0.78 %ClaNum:96(EqnAxiom:0)
% 0.55/0.78 %VarNum:255(SingletonVarNum:158)
% 0.55/0.78 %MaxLitNum:3
% 0.55/0.78 %MaxfuncDepth:3
% 0.55/0.78 %SharedTerms:50
% 0.55/0.78 %goalClause: 20 73
% 0.55/0.78 %singleGoalClaCount:1
% 0.55/0.78 [1]P1(a1)
% 0.55/0.78 [2]P2(a2)
% 0.55/0.78 [3]P2(a8)
% 0.55/0.78 [4]P16(a9)
% 0.55/0.78 [7]P6(a10,a3)
% 0.55/0.78 [8]P6(a6,a2)
% 0.55/0.78 [9]P6(a2,a8)
% 0.55/0.78 [10]P6(a7,a6)
% 0.55/0.78 [11]P6(a11,a7)
% 0.55/0.78 [12]P6(a11,a13)
% 0.55/0.78 [13]P6(a13,a12)
% 0.55/0.78 [14]P6(a12,a10)
% 0.55/0.78 [15]P17(a14,a29)
% 0.55/0.78 [26]P11(a9,f26(a16,a15,a5))
% 0.55/0.78 [20]P2(f25(f28(f22(a32)),a20))
% 0.55/0.78 [23]P6(f25(f28(f22(a32)),a20),a11)
% 0.55/0.78 [38]~P20(x381,x381)
% 0.55/0.78 [5]P32(f22(x51))
% 0.55/0.78 [6]P3(f28(x61))
% 0.55/0.78 [16]P18(f22(x161),a23)
% 0.55/0.78 [17]P18(f28(x171),a24)
% 0.55/0.78 [21]P19(f22(x211),a30,x211)
% 0.55/0.78 [22]P19(f28(x221),a30,x221)
% 0.55/0.78 [18]P10(f25(x181,x182))
% 0.55/0.78 [19]P18(f25(x191,x192),a4)
% 0.55/0.78 [24]P19(f25(x241,x242),a30,x241)
% 0.55/0.78 [25]P19(f25(x251,x252),a31,x252)
% 0.55/0.78 [27]P4(f26(x271,x272,x273))
% 0.55/0.78 [28]P18(f26(x281,x282,x283),a17)
% 0.55/0.78 [29]P19(f26(x291,x292,x293),a29,x293)
% 0.55/0.78 [30]P19(f26(x301,x302,x303),a30,x301)
% 0.55/0.78 [31]P19(f26(x311,x312,x313),a31,x312)
% 0.55/0.78 [32]P27(f27(x321,x322,x323,x324))
% 0.55/0.78 [33]P18(f27(x331,x332,x333,x334),a14)
% 0.55/0.78 [34]P19(f27(x341,x342,x343,x344),a29,x343)
% 0.55/0.78 [35]P19(f27(x351,x352,x353,x354),a30,x351)
% 0.55/0.78 [36]P19(f27(x361,x362,x363,x364),a31,x362)
% 0.55/0.78 [37]P19(f27(x371,x372,x373,x374),a33,x374)
% 0.55/0.78 [93]~P2(a3)+P23(a19,a18,f26(a16,a15,a5))
% 0.55/0.78 [39]~P24(x391)+P11(x391,a16)
% 0.55/0.78 [40]~P29(x401)+P11(x401,a18)
% 0.55/0.78 [41]~P1(x411)+P11(x411,a21)
% 0.55/0.78 [43]~P10(x431)+P6(x431,x431)
% 0.55/0.78 [45]~P21(x451)+P12(x451,x451)
% 0.55/0.78 [46]P1(x461)+~P11(x461,a21)
% 0.55/0.78 [47]P24(x471)+~P11(x471,a16)
% 0.55/0.78 [48]P29(x481)+~P11(x481,a18)
% 0.55/0.78 [73]~P29(x731)+~P30(x731,a9)
% 0.55/0.78 [92]~P16(x921)+P11(x921,f26(a16,a15,a5))
% 0.55/0.78 [94]P16(x941)+~P11(x941,f26(a16,a15,a5))
% 0.55/0.78 [49]P16(x491)+~P30(x492,x491)
% 0.55/0.78 [51]P21(x511)+~P12(x512,x511)
% 0.55/0.78 [53]P21(x531)+~P12(x531,x532)
% 0.55/0.78 [54]P5(x541)+~P7(x542,x541)
% 0.55/0.78 [55]P5(x551)+~P7(x551,x552)
% 0.55/0.78 [57]P4(x571)+~P11(x572,x571)
% 0.55/0.78 [58]P4(x581)+~P8(x582,x581)
% 0.55/0.78 [59]P4(x591)+~P8(x591,x592)
% 0.55/0.78 [60]P25(x601)+~P20(x602,x601)
% 0.55/0.78 [61]P25(x611)+~P20(x611,x612)
% 0.55/0.78 [62]P26(x621)+~P20(x622,x621)
% 0.55/0.78 [63]P26(x631)+~P20(x631,x632)
% 0.55/0.78 [64]P31(x641)+~P30(x641,x642)
% 0.55/0.78 [66]P27(x661)+~P11(x661,x662)
% 0.55/0.78 [67]P22(x671)+~P17(x672,x671)
% 0.55/0.78 [68]P9(x681)+~P17(x681,x682)
% 0.55/0.78 [70]P10(x701)+~P6(x702,x701)
% 0.55/0.78 [72]P10(x721)+~P6(x721,x722)
% 0.55/0.78 [75]~P8(x752,x751)+P8(x751,x752)
% 0.55/0.78 [89]P5(x891)+~P23(x891,x892,x893)
% 0.55/0.78 [90]P4(x901)+~P23(x902,x903,x901)
% 0.55/0.78 [91]P4(x911)+~P23(x912,x911,x913)
% 0.55/0.78 [96]~P11(x961,f26(a16,a15,a5))+~P2(a3)+P30(f27(x961,a19,a18,f26(a16,a15,a5)),x961)
% 0.55/0.78 [74]~P6(x742,x741)+P2(x741)+~P2(x742)
% 0.55/0.78 [76]~P6(x761,x763)+P6(x761,x762)+~P6(x763,x762)
% 0.55/0.78 [77]~P13(x773,x772)+P11(x771,x772)+~P11(x771,x773)
% 0.55/0.78 [78]~P13(x781,x783)+P8(x781,x782)+~P8(x783,x782)
% 0.55/0.78 [79]~P13(x792,x793)+P8(x791,x792)+~P8(x791,x793)
% 0.55/0.78 [80]~P12(x801,x803)+P7(x801,x802)+~P7(x803,x802)
% 0.55/0.78 [81]~P12(x813,x812)+P7(x811,x812)+~P7(x811,x813)
% 0.55/0.78 [82]~P7(x821,x823)+P12(x821,x822)+~P7(x823,x822)
% 0.55/0.78 [83]~P12(x831,x833)+P12(x831,x832)+~P12(x833,x832)
% 0.55/0.78 [84]~P20(x841,x843)+P20(x841,x842)+~P20(x843,x842)
% 0.55/0.78 [85]~P14(x852,x853)+P20(x851,x852)+~P20(x851,x853)
% 0.55/0.78 [86]~P15(x862,x863)+P20(x861,x862)+~P20(x861,x863)
% 0.55/0.78 [87]~P28(x872,x873)+P20(x871,x872)+~P20(x871,x873)
% 0.55/0.78 [88]~P8(x883,x882)+~P11(x881,x882)+~P11(x881,x883)
% 0.55/0.78 [95]~P11(x951,x954)+~P23(x952,x953,x954)+P11(f27(x951,x952,x953,x954),x953)
% 0.55/0.78 %EqnAxiom
% 0.55/0.78
% 0.55/0.78 %-------------------------------------------
% 0.55/0.78 cnf(97,plain,
% 0.55/0.78 (P6(a12,a3)),
% 0.55/0.78 inference(scs_inference,[],[7,14,76])).
% 0.55/0.78 cnf(103,plain,
% 0.55/0.78 (P6(a13,a3)),
% 0.55/0.78 inference(scs_inference,[],[97,13,76])).
% 0.55/0.78 cnf(107,plain,
% 0.55/0.78 (P6(a11,a3)),
% 0.55/0.78 inference(scs_inference,[],[103,12,76])).
% 0.55/0.78 cnf(111,plain,
% 0.55/0.78 (P6(f25(f28(f22(a32)),a20),a3)),
% 0.55/0.78 inference(scs_inference,[],[107,23,76])).
% 0.55/0.78 cnf(155,plain,
% 0.55/0.78 (~P30(x1551,x1552)+P11(x1552,f26(a16,a15,a5))),
% 0.55/0.78 inference(scs_inference,[],[49,92])).
% 0.55/0.78 cnf(164,plain,
% 0.55/0.78 (P23(a19,a18,f26(a16,a15,a5))),
% 0.55/0.78 inference(scs_inference,[],[20,111,93,74])).
% 0.55/0.78 cnf(165,plain,
% 0.55/0.78 (~P30(x1651,x1652)+P11(f27(x1652,a19,a18,f26(a16,a15,a5)),a18)),
% 0.55/0.78 inference(scs_inference,[],[164,155,95])).
% 0.55/0.78 cnf(184,plain,
% 0.55/0.79 (P11(f27(a9,a19,a18,f26(a16,a15,a5)),a18)+~P2(a3)),
% 0.55/0.79 inference(scs_inference,[],[26,165,96])).
% 0.55/0.79 cnf(185,plain,
% 0.55/0.79 (P29(f27(a9,a19,a18,f26(a16,a15,a5)))+~P2(a3)),
% 0.55/0.79 inference(scs_inference,[],[184,48])).
% 0.55/0.79 cnf(186,plain,
% 0.55/0.79 (~P30(f27(a9,a19,a18,f26(a16,a15,a5)),a9)+~P2(a3)),
% 0.55/0.79 inference(scs_inference,[],[185,73])).
% 0.55/0.79 cnf(187,plain,
% 0.55/0.79 (~P2(a3)),
% 0.55/0.79 inference(scs_inference,[],[26,186,96])).
% 0.55/0.79 cnf(188,plain,
% 0.55/0.79 ($false),
% 0.55/0.79 inference(scs_inference,[],[20,187,111,74]),
% 0.55/0.79 ['proof']).
% 0.55/0.79 % SZS output end Proof
% 0.55/0.79 % Total time :0.150000s
%------------------------------------------------------------------------------