%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CSR052+1 : TPTP v8.2.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/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:38 EDT 2024
% Result : Theorem 0.54s 0.66s
% Output : CNFRefutation 0.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : CSR052+1 : TPTP v8.2.0. Released v3.4.0.
% 0.08/0.12 % Command : java -jar /export/starexec/sandbox/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:57:39 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.47/0.58 start to proof:theBenchmark
% 0.54/0.64 %-------------------------------------------
% 0.54/0.64 % File :CSE---1.7
% 0.54/0.64 % Problem :theBenchmark
% 0.54/0.64 % Transform :cnf
% 0.54/0.64 % Format :tptp:raw
% 0.54/0.64 % Command :java -jar mcs_scs.jar %d %s
% 0.54/0.64
% 0.54/0.64 % Result :Theorem 0.010000s
% 0.54/0.64 % Output :CNFRefutation 0.010000s
% 0.54/0.64 %-------------------------------------------
% 0.54/0.65 %------------------------------------------------------------------------------
% 0.54/0.65 % File : CSR052+1 : TPTP v8.2.0. Released v3.4.0.
% 0.54/0.65 % Domain : Common Sense Reasoning
% 0.54/0.65 % Problem : Autogenerated Cyc Problem CSR052+1
% 0.54/0.65 % Version : Especial.
% 0.54/0.65 % English :
% 0.54/0.65
% 0.54/0.65 % Refs : [RS+] Reagan Smith et al., The Cyc TPTP Challenge Problem
% 0.54/0.65 % Source : [RS+]
% 0.54/0.65 % Names :
% 0.54/0.65
% 0.54/0.65 % Status : Theorem
% 0.54/0.65 % Rating : 0.06 v8.2.0, 0.07 v7.5.0, 0.05 v7.4.0, 0.06 v7.3.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.10 v4.1.0, 0.06 v4.0.1, 0.00 v3.4.0
% 0.54/0.65 % Syntax : Number of formulae : 96 ( 27 unt; 0 def)
% 0.54/0.65 % Number of atoms : 178 ( 0 equ)
% 0.54/0.65 % Maximal formula atoms : 3 ( 1 avg)
% 0.54/0.65 % Number of connectives : 83 ( 1 ~; 0 |; 14 &)
% 0.54/0.65 % ( 0 <=>; 68 =>; 0 <=; 0 <~>)
% 0.54/0.65 % Maximal formula depth : 7 ( 3 avg)
% 0.54/0.65 % Maximal term depth : 4 ( 1 avg)
% 0.54/0.65 % Number of predicates : 26 ( 26 usr; 0 prp; 1-3 aty)
% 0.54/0.65 % Number of functors : 27 ( 27 usr; 24 con; 0-2 aty)
% 0.54/0.65 % Number of variables : 128 ( 128 !; 0 ?)
% 0.54/0.65 % SPC : FOF_THM_RFO_NEQ
% 0.54/0.65
% 0.54/0.65 % Comments : Autogenerated from the OpenCyc KB. Documentation can be found at
% 0.54/0.65 % http://opencyc.org/doc/#TPTP_Challenge_Problem_Set
% 0.54/0.65 % : Cyc(R) Knowledge Base Copyright(C) 1995-2007 Cycorp, Inc., Austin,
% 0.54/0.65 % TX, USA. All rights reserved.
% 0.54/0.65 % : OpenCyc Knowledge Base Copyright(C) 2001-2007 Cycorp, Inc.,
% 0.54/0.65 % Austin, TX, USA. All rights reserved.
% 0.54/0.65 %------------------------------------------------------------------------------
% 0.54/0.65 %$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.54/0.65 %$static(cyc_scaling_1,include('Axioms/CSR002+0.ax'))
% 0.54/0.65 %----Empty file include('Axioms/CSR002+0.ax').
% 0.54/0.65 %------------------------------------------------------------------------------
% 0.54/0.65 % Cyc Assertion #455528:
% 0.54/0.65 fof(just1,axiom,
% 0.54/0.65 transitivebinarypredicate(c_genls) ).
% 0.54/0.65
% 0.54/0.65 % Cyc Assertion #592971:
% 0.54/0.65 fof(just2,axiom,
% 0.54/0.65 genlmt(c_cycorpproductsmt,c_basekb) ).
% 0.54/0.65
% 0.54/0.65 % Cyc Assertion #600900:
% 0.54/0.65 fof(just3,axiom,
% 0.54/0.65 genlmt(c_cycnounlearnermt,c_cycorpproductsmt) ).
% 0.54/0.65
% 0.54/0.65 % Cyc Assertion #829544:
% 0.54/0.65 fof(just4,axiom,
% 0.54/0.65 genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_ukencartamsncomencyclopedia_761573010_4united_states_of_americahtml)),c_translation_33),c_machinelearningspindleheadmt) ).
% 0.54/0.65
% 0.54/0.65 % Cyc Assertion #1322220:
% 0.54/0.65 fof(just5,axiom,
% 0.54/0.65 transitivebinarypredicate(c_genlmt) ).
% 0.54/0.65
% 0.54/0.65 % Cyc Assertion #1614635:
% 0.54/0.65 fof(just6,axiom,
% 0.54/0.65 genlmt(c_machinelearningspindleheadmt,c_cycnounlearnermt) ).
% 0.54/0.65
% 0.54/0.65 % Cyc Assertion #1650755:
% 0.54/0.65 fof(just7,axiom,
% 0.54/0.65 genlmt(c_basekb,c_universalvocabularymt) ).
% 0.54/0.65
% 0.54/0.65 % Cyc Assertion #1922596:
% 0.54/0.65 fof(just8,axiom,
% 0.54/0.65 genls(c_tptpcol_8_39940,c_tptpcol_7_39939) ).
% 0.54/0.65
% 0.54/0.65 fof(just9,axiom,
% 0.54/0.65 ! [OBJ] :
% 0.54/0.65 ( tptpcol_8_39940(OBJ)
% 0.54/0.65 => tptpcol_7_39939(OBJ) ) ).
% 0.54/0.65
% 0.54/0.65 % Cyc Assertion #1923235:
% 0.54/0.65 fof(just10,axiom,
% 0.54/0.65 genls(c_tptpcol_9_40196,c_tptpcol_8_39940) ).
% 0.54/0.65
% 0.54/0.65 fof(just11,axiom,
% 0.54/0.65 ! [OBJ] :
% 0.54/0.65 ( tptpcol_9_40196(OBJ)
% 0.54/0.65 => tptpcol_8_39940(OBJ) ) ).
% 0.54/0.65
% 0.54/0.65 % Cyc Assertion #1923554:
% 0.54/0.65 fof(just12,axiom,
% 0.54/0.65 genls(c_tptpcol_10_40324,c_tptpcol_9_40196) ).
% 0.54/0.65
% 0.54/0.65 fof(just13,axiom,
% 0.54/0.65 ! [OBJ] :
% 0.54/0.65 ( tptpcol_10_40324(OBJ)
% 0.54/0.65 => tptpcol_9_40196(OBJ) ) ).
% 0.54/0.65
% 0.54/0.65 % Cyc Assertion #1923713:
% 0.54/0.65 fof(just14,axiom,
% 0.54/0.65 genls(c_tptpcol_11_40388,c_tptpcol_10_40324) ).
% 0.54/0.65
% 0.54/0.65 fof(just15,axiom,
% 0.54/0.65 ! [OBJ] :
% 0.54/0.65 ( tptpcol_11_40388(OBJ)
% 0.54/0.65 => tptpcol_10_40324(OBJ) ) ).
% 0.54/0.65
% 0.54/0.65 % Cyc Assertion #1923792:
% 0.54/0.65 fof(just16,axiom,
% 0.54/0.65 genls(c_tptpcol_12_40420,c_tptpcol_11_40388) ).
% 0.54/0.65
% 0.54/0.65 fof(just17,axiom,
% 0.54/0.65 ! [OBJ] :
% 0.54/0.65 ( tptpcol_12_40420(OBJ)
% 0.54/0.65 => tptpcol_11_40388(OBJ) ) ).
% 0.54/0.65
% 0.54/0.65 % Cyc Assertion #1923794:
% 0.54/0.65 fof(just18,axiom,
% 0.54/0.65 genls(c_tptpcol_13_40421,c_tptpcol_12_40420) ).
% 0.54/0.65
% 0.54/0.65 fof(just19,axiom,
% 0.54/0.65 ! [OBJ] :
% 0.54/0.65 ( tptpcol_13_40421(OBJ)
% 0.54/0.65 => tptpcol_12_40420(OBJ) ) ).
% 0.54/0.65
% 0.54/0.65 % Cyc Assertion #1923813:
% 0.54/0.65 fof(just20,axiom,
% 0.54/0.65 genls(c_tptpcol_14_40429,c_tptpcol_13_40421) ).
% 0.54/0.65
% 0.54/0.65 fof(just21,axiom,
% 0.54/0.65 ! [OBJ] :
% 0.54/0.65 ( tptpcol_14_40429(OBJ)
% 0.54/0.65 => tptpcol_13_40421(OBJ) ) ).
% 0.54/0.65
% 0.54/0.65 % Cyc Assertion #1923815:
% 0.54/0.65 fof(just22,axiom,
% 0.54/0.65 genls(c_tptpcol_15_40430,c_tptpcol_14_40429) ).
% 0.54/0.65
% 0.54/0.65 fof(just23,axiom,
% 0.54/0.65 ! [OBJ] :
% 0.54/0.65 ( tptpcol_15_40430(OBJ)
% 0.54/0.65 => tptpcol_14_40429(OBJ) ) ).
% 0.54/0.65
% 0.54/0.65 % Cyc Assertion #398814:
% 0.54/0.65 fof(just24,axiom,
% 0.54/0.65 ! [OBJ,COL1,COL2] :
% 0.54/0.65 ~ ( isa(OBJ,COL1)
% 0.54/0.65 & isa(OBJ,COL2)
% 0.54/0.65 & disjointwith(COL1,COL2) ) ).
% 0.54/0.65
% 0.54/0.65 % Cyc Assertion #831913:
% 0.54/0.65 fof(just25,axiom,
% 0.54/0.65 ! [SPECPRED,PRED,GENLPRED] :
% 0.54/0.65 ( ( genlinverse(SPECPRED,PRED)
% 0.54/0.65 & genlinverse(PRED,GENLPRED) )
% 0.54/0.65 => genlpreds(SPECPRED,GENLPRED) ) ).
% 0.54/0.65
% 0.54/0.65 % Cyc Constant #40273:
% 0.54/0.65 fof(just26,axiom,
% 0.54/0.65 ! [ARG1,INS] :
% 0.54/0.65 ( genlpreds(ARG1,INS)
% 0.54/0.65 => predicate(INS) ) ).
% 0.54/0.65
% 0.54/0.65 fof(just27,axiom,
% 0.54/0.65 ! [ARG1,INS] :
% 0.54/0.65 ( genlpreds(ARG1,INS)
% 0.54/0.65 => predicate(INS) ) ).
% 0.54/0.65
% 0.54/0.65 fof(just28,axiom,
% 0.54/0.65 ! [INS,ARG2] :
% 0.54/0.65 ( genlpreds(INS,ARG2)
% 0.54/0.65 => predicate(INS) ) ).
% 0.54/0.65
% 0.54/0.65 fof(just29,axiom,
% 0.54/0.65 ! [INS,ARG2] :
% 0.54/0.65 ( genlpreds(INS,ARG2)
% 0.54/0.65 => predicate(INS) ) ).
% 0.54/0.65
% 0.54/0.65 fof(just30,axiom,
% 0.54/0.65 ! [X,Y,Z] :
% 0.54/0.65 ( ( genlpreds(X,Y)
% 0.54/0.65 & genlpreds(Y,Z) )
% 0.54/0.65 => genlpreds(X,Z) ) ).
% 0.54/0.65
% 0.54/0.65 fof(just31,axiom,
% 0.54/0.65 ! [X] :
% 0.54/0.65 ( predicate(X)
% 0.54/0.65 => genlpreds(X,X) ) ).
% 0.54/0.65
% 0.54/0.65 fof(just32,axiom,
% 0.54/0.65 ! [X] :
% 0.54/0.65 ( predicate(X)
% 0.54/0.65 => genlpreds(X,X) ) ).
% 0.54/0.65
% 0.54/0.65 % Cyc Constant #45259:
% 0.54/0.65 fof(just33,axiom,
% 0.54/0.65 ! [ARG1,INS] :
% 0.54/0.65 ( genlinverse(ARG1,INS)
% 0.54/0.65 => binarypredicate(INS) ) ).
% 0.54/0.65
% 0.54/0.65 fof(just34,axiom,
% 0.54/0.65 ! [INS,ARG2] :
% 0.54/0.65 ( genlinverse(INS,ARG2)
% 0.54/0.65 => binarypredicate(INS) ) ).
% 0.54/0.65
% 0.54/0.65 fof(just35,axiom,
% 0.54/0.65 ! [OLD,ARG2,NEW] :
% 0.54/0.65 ( ( genlinverse(OLD,ARG2)
% 0.54/0.65 & genlpreds(NEW,OLD) )
% 0.54/0.65 => genlinverse(NEW,ARG2) ) ).
% 0.54/0.65
% 0.54/0.65 fof(just36,axiom,
% 0.54/0.65 ! [ARG1,OLD,NEW] :
% 0.54/0.65 ( ( genlinverse(ARG1,OLD)
% 0.54/0.65 & genlpreds(OLD,NEW) )
% 0.54/0.65 => genlinverse(ARG1,NEW) ) ).
% 0.54/0.65
% 0.54/0.65 % Cyc Constant #78648:
% 0.54/0.65 fof(just37,axiom,
% 0.54/0.65 ! [ARG1,INS] :
% 0.54/0.65 ( disjointwith(ARG1,INS)
% 0.54/0.65 => collection(INS) ) ).
% 0.54/0.65
% 0.54/0.65 fof(just38,axiom,
% 0.54/0.65 ! [INS,ARG2] :
% 0.54/0.65 ( disjointwith(INS,ARG2)
% 0.54/0.65 => collection(INS) ) ).
% 0.54/0.65
% 0.54/0.65 fof(just39,axiom,
% 0.54/0.65 ! [X,Y] :
% 0.54/0.65 ( disjointwith(X,Y)
% 0.54/0.65 => disjointwith(Y,X) ) ).
% 0.54/0.65
% 0.54/0.65 fof(just40,axiom,
% 0.54/0.65 ! [ARG1,OLD,NEW] :
% 0.54/0.65 ( ( disjointwith(ARG1,OLD)
% 0.54/0.65 & genls(NEW,OLD) )
% 0.54/0.65 => disjointwith(ARG1,NEW) ) ).
% 0.54/0.65
% 0.54/0.65 fof(just41,axiom,
% 0.54/0.65 ! [OLD,ARG2,NEW] :
% 0.54/0.65 ( ( disjointwith(OLD,ARG2)
% 0.54/0.65 & genls(NEW,OLD) )
% 0.54/0.65 => disjointwith(NEW,ARG2) ) ).
% 0.54/0.65
% 0.54/0.65 % Cyc Constant #170027:
% 0.54/0.65 fof(just42,axiom,
% 0.54/0.65 ! [X] :
% 0.54/0.65 ( isa(X,c_tptpcol_15_40430)
% 0.54/0.65 => tptpcol_15_40430(X) ) ).
% 0.54/0.65
% 0.54/0.65 fof(just43,axiom,
% 0.54/0.65 ! [X] :
% 0.54/0.65 ( tptpcol_15_40430(X)
% 0.54/0.65 => isa(X,c_tptpcol_15_40430) ) ).
% 0.54/0.65
% 0.54/0.65 % Cyc Constant #170026:
% 0.54/0.65 fof(just44,axiom,
% 0.54/0.65 ! [X] :
% 0.54/0.65 ( isa(X,c_tptpcol_14_40429)
% 0.54/0.65 => tptpcol_14_40429(X) ) ).
% 0.54/0.65
% 0.54/0.65 fof(just45,axiom,
% 0.54/0.65 ! [X] :
% 0.54/0.65 ( tptpcol_14_40429(X)
% 0.54/0.65 => isa(X,c_tptpcol_14_40429) ) ).
% 0.54/0.65
% 0.54/0.65 % Cyc Constant #170018:
% 0.54/0.65 fof(just46,axiom,
% 0.54/0.65 ! [X] :
% 0.54/0.65 ( isa(X,c_tptpcol_13_40421)
% 0.54/0.65 => tptpcol_13_40421(X) ) ).
% 0.54/0.65
% 0.54/0.65 fof(just47,axiom,
% 0.54/0.65 ! [X] :
% 0.54/0.65 ( tptpcol_13_40421(X)
% 0.54/0.65 => isa(X,c_tptpcol_13_40421) ) ).
% 0.54/0.65
% 0.54/0.65 % Cyc Constant #170017:
% 0.54/0.65 fof(just48,axiom,
% 0.54/0.65 ! [X] :
% 0.54/0.65 ( isa(X,c_tptpcol_12_40420)
% 0.54/0.65 => tptpcol_12_40420(X) ) ).
% 0.54/0.65
% 0.54/0.65 fof(just49,axiom,
% 0.54/0.65 ! [X] :
% 0.54/0.65 ( tptpcol_12_40420(X)
% 0.54/0.65 => isa(X,c_tptpcol_12_40420) ) ).
% 0.54/0.65
% 0.54/0.65 % Cyc Constant #169985:
% 0.54/0.65 fof(just50,axiom,
% 0.54/0.66 ! [X] :
% 0.54/0.66 ( isa(X,c_tptpcol_11_40388)
% 0.54/0.66 => tptpcol_11_40388(X) ) ).
% 0.54/0.66
% 0.54/0.66 fof(just51,axiom,
% 0.54/0.66 ! [X] :
% 0.54/0.66 ( tptpcol_11_40388(X)
% 0.54/0.66 => isa(X,c_tptpcol_11_40388) ) ).
% 0.54/0.66
% 0.54/0.66 % Cyc Constant #169921:
% 0.54/0.66 fof(just52,axiom,
% 0.54/0.66 ! [X] :
% 0.54/0.66 ( isa(X,c_tptpcol_10_40324)
% 0.54/0.66 => tptpcol_10_40324(X) ) ).
% 0.54/0.66
% 0.54/0.66 fof(just53,axiom,
% 0.54/0.66 ! [X] :
% 0.54/0.66 ( tptpcol_10_40324(X)
% 0.54/0.66 => isa(X,c_tptpcol_10_40324) ) ).
% 0.54/0.66
% 0.54/0.66 % Cyc Constant #169793:
% 0.54/0.66 fof(just54,axiom,
% 0.54/0.66 ! [X] :
% 0.54/0.66 ( isa(X,c_tptpcol_9_40196)
% 0.54/0.66 => tptpcol_9_40196(X) ) ).
% 0.54/0.66
% 0.54/0.66 fof(just55,axiom,
% 0.54/0.66 ! [X] :
% 0.54/0.66 ( tptpcol_9_40196(X)
% 0.54/0.66 => isa(X,c_tptpcol_9_40196) ) ).
% 0.54/0.66
% 0.54/0.66 % Cyc Constant #169536:
% 0.54/0.66 fof(just56,axiom,
% 0.54/0.66 ! [X] :
% 0.54/0.66 ( isa(X,c_tptpcol_7_39939)
% 0.54/0.66 => tptpcol_7_39939(X) ) ).
% 0.54/0.66
% 0.54/0.66 fof(just57,axiom,
% 0.54/0.66 ! [X] :
% 0.54/0.66 ( tptpcol_7_39939(X)
% 0.54/0.66 => isa(X,c_tptpcol_7_39939) ) ).
% 0.54/0.66
% 0.54/0.66 % Cyc Constant #169537:
% 0.54/0.66 fof(just58,axiom,
% 0.54/0.66 ! [X] :
% 0.54/0.66 ( isa(X,c_tptpcol_8_39940)
% 0.54/0.66 => tptpcol_8_39940(X) ) ).
% 0.54/0.66
% 0.54/0.66 fof(just59,axiom,
% 0.54/0.66 ! [X] :
% 0.54/0.66 ( tptpcol_8_39940(X)
% 0.54/0.66 => isa(X,c_tptpcol_8_39940) ) ).
% 0.54/0.66
% 0.54/0.66 % Cyc Constant #129091:
% 0.54/0.66 fof(just60,axiom,
% 0.54/0.66 ! [ARG1] : natfunction(f_urlfn(ARG1),c_urlfn) ).
% 0.54/0.66
% 0.54/0.66 fof(just61,axiom,
% 0.54/0.66 ! [ARG1] : natargument(f_urlfn(ARG1),n_1,ARG1) ).
% 0.54/0.66
% 0.54/0.66 fof(just62,axiom,
% 0.54/0.66 ! [ARG1] : uniformresourcelocator(f_urlfn(ARG1)) ).
% 0.54/0.66
% 0.54/0.66 % Cyc Constant #78971:
% 0.54/0.66 fof(just63,axiom,
% 0.54/0.66 ! [ARG1] : natfunction(f_urlreferentfn(ARG1),c_urlreferentfn) ).
% 0.54/0.66
% 0.54/0.66 fof(just64,axiom,
% 0.54/0.66 ! [ARG1] : natargument(f_urlreferentfn(ARG1),n_1,ARG1) ).
% 0.54/0.66
% 0.54/0.66 fof(just65,axiom,
% 0.54/0.66 ! [ARG1] : computerdataartifact(f_urlreferentfn(ARG1)) ).
% 0.54/0.66
% 0.54/0.66 % Cyc Constant #71728:
% 0.54/0.66 fof(just66,axiom,
% 0.54/0.66 ! [ARG1,ARG2] : natfunction(f_contentmtofcdafromeventfn(ARG1,ARG2),c_contentmtofcdafromeventfn) ).
% 0.54/0.66
% 0.54/0.66 fof(just67,axiom,
% 0.54/0.66 ! [ARG1,ARG2] : natargument(f_contentmtofcdafromeventfn(ARG1,ARG2),n_1,ARG1) ).
% 0.54/0.66
% 0.54/0.66 fof(just68,axiom,
% 0.54/0.66 ! [ARG1,ARG2] : natargument(f_contentmtofcdafromeventfn(ARG1,ARG2),n_2,ARG2) ).
% 0.54/0.66
% 0.54/0.66 fof(just69,axiom,
% 0.54/0.66 ! [ARG1,ARG2] : microtheory(f_contentmtofcdafromeventfn(ARG1,ARG2)) ).
% 0.54/0.66
% 0.54/0.66 % Cyc Constant #19550:
% 0.54/0.66 fof(just70,axiom,
% 0.54/0.66 ! [SPECMT,GENLMT] :
% 0.54/0.66 ( ( mtvisible(SPECMT)
% 0.54/0.66 & genlmt(SPECMT,GENLMT) )
% 0.54/0.66 => mtvisible(GENLMT) ) ).
% 0.54/0.66
% 0.54/0.66 fof(just71,axiom,
% 0.54/0.66 ! [ARG1,INS] :
% 0.54/0.66 ( genlmt(ARG1,INS)
% 0.54/0.66 => microtheory(INS) ) ).
% 0.54/0.66
% 0.54/0.66 fof(just72,axiom,
% 0.54/0.66 ! [ARG1,INS] :
% 0.54/0.66 ( genlmt(ARG1,INS)
% 0.54/0.66 => microtheory(INS) ) ).
% 0.54/0.66
% 0.54/0.66 fof(just73,axiom,
% 0.54/0.66 ! [INS,ARG2] :
% 0.54/0.66 ( genlmt(INS,ARG2)
% 0.54/0.66 => microtheory(INS) ) ).
% 0.54/0.66
% 0.54/0.66 fof(just74,axiom,
% 0.54/0.66 ! [INS,ARG2] :
% 0.54/0.66 ( genlmt(INS,ARG2)
% 0.54/0.66 => microtheory(INS) ) ).
% 0.54/0.66
% 0.54/0.66 fof(just75,axiom,
% 0.54/0.66 ! [X,Y,Z] :
% 0.54/0.66 ( ( genlmt(X,Y)
% 0.54/0.66 & genlmt(Y,Z) )
% 0.54/0.66 => genlmt(X,Z) ) ).
% 0.54/0.66
% 0.54/0.66 fof(just76,axiom,
% 0.54/0.66 ! [X] :
% 0.54/0.66 ( microtheory(X)
% 0.54/0.66 => genlmt(X,X) ) ).
% 0.54/0.66
% 0.54/0.66 fof(just77,axiom,
% 0.54/0.66 ! [X] :
% 0.54/0.66 ( microtheory(X)
% 0.54/0.66 => genlmt(X,X) ) ).
% 0.54/0.66
% 0.54/0.66 % Cyc Constant #27757:
% 0.54/0.66 fof(just78,axiom,
% 0.54/0.66 mtvisible(c_basekb) ).
% 0.54/0.66
% 0.54/0.66 % Cyc Constant #127156:
% 0.54/0.66 fof(just79,axiom,
% 0.54/0.66 ! [X] :
% 0.54/0.66 ( isa(X,c_transitivebinarypredicate)
% 0.54/0.66 => transitivebinarypredicate(X) ) ).
% 0.54/0.66
% 0.54/0.66 fof(just80,axiom,
% 0.54/0.66 ! [X] :
% 0.54/0.66 ( transitivebinarypredicate(X)
% 0.54/0.66 => isa(X,c_transitivebinarypredicate) ) ).
% 0.54/0.66
% 0.54/0.66 % Cyc Constant #0:
% 0.54/0.66 fof(just81,axiom,
% 0.54/0.66 ! [ARG1,INS] :
% 0.54/0.66 ( genls(ARG1,INS)
% 0.54/0.66 => collection(INS) ) ).
% 0.54/0.66
% 0.54/0.66 fof(just82,axiom,
% 0.54/0.66 ! [ARG1,INS] :
% 0.54/0.66 ( genls(ARG1,INS)
% 0.54/0.66 => collection(INS) ) ).
% 0.54/0.66
% 0.54/0.66 fof(just83,axiom,
% 0.54/0.66 ! [INS,ARG2] :
% 0.54/0.66 ( genls(INS,ARG2)
% 0.54/0.66 => collection(INS) ) ).
% 0.54/0.66
% 0.54/0.66 fof(just84,axiom,
% 0.54/0.66 ! [INS,ARG2] :
% 0.54/0.66 ( genls(INS,ARG2)
% 0.54/0.66 => collection(INS) ) ).
% 0.54/0.66
% 0.54/0.66 fof(just85,axiom,
% 0.54/0.66 ! [X,Y,Z] :
% 0.54/0.66 ( ( genls(X,Y)
% 0.54/0.66 & genls(Y,Z) )
% 0.54/0.66 => genls(X,Z) ) ).
% 0.54/0.66
% 0.54/0.66 fof(just86,axiom,
% 0.54/0.66 ! [X] :
% 0.54/0.66 ( collection(X)
% 0.54/0.66 => genls(X,X) ) ).
% 0.54/0.66
% 0.54/0.66 fof(just87,axiom,
% 0.54/0.66 ! [X] :
% 0.54/0.66 ( collection(X)
% 0.54/0.66 => genls(X,X) ) ).
% 0.54/0.66
% 0.54/0.66 fof(just88,axiom,
% 0.54/0.66 ! [OLD,ARG2,NEW] :
% 0.54/0.66 ( ( genls(OLD,ARG2)
% 0.54/0.66 & genls(NEW,OLD) )
% 0.54/0.66 => genls(NEW,ARG2) ) ).
% 0.54/0.66
% 0.54/0.66 fof(just89,axiom,
% 0.54/0.66 ! [ARG1,OLD,NEW] :
% 0.54/0.66 ( ( genls(ARG1,OLD)
% 0.54/0.66 & genls(OLD,NEW) )
% 0.54/0.66 => genls(ARG1,NEW) ) ).
% 0.54/0.66
% 0.54/0.66 % Cyc Constant #72115:
% 0.54/0.66 fof(just90,axiom,
% 0.54/0.66 ! [ARG1,INS] :
% 0.54/0.66 ( isa(ARG1,INS)
% 0.54/0.66 => collection(INS) ) ).
% 0.54/0.66
% 0.54/0.66 fof(just91,axiom,
% 0.54/0.66 ! [ARG1,INS] :
% 0.54/0.66 ( isa(ARG1,INS)
% 0.54/0.66 => collection(INS) ) ).
% 0.54/0.66
% 0.54/0.66 fof(just92,axiom,
% 0.54/0.66 ! [INS,ARG2] :
% 0.54/0.66 ( isa(INS,ARG2)
% 0.54/0.66 => thing(INS) ) ).
% 0.54/0.66
% 0.54/0.66 fof(just93,axiom,
% 0.54/0.66 ! [INS,ARG2] :
% 0.54/0.66 ( isa(INS,ARG2)
% 0.54/0.66 => thing(INS) ) ).
% 0.54/0.66
% 0.54/0.66 fof(just94,axiom,
% 0.54/0.66 ! [ARG1,OLD,NEW] :
% 0.54/0.66 ( ( isa(ARG1,OLD)
% 0.54/0.66 & genls(OLD,NEW) )
% 0.54/0.66 => isa(ARG1,NEW) ) ).
% 0.54/0.66
% 0.54/0.66 % Cyc Constant #95028:
% 0.54/0.66 fof(just95,axiom,
% 0.54/0.66 mtvisible(c_universalvocabularymt) ).
% 0.54/0.66
% 0.54/0.66 fof(query52,conjecture,
% 0.54/0.66 ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_ukencartamsncomencyclopedia_761573010_4united_states_of_americahtml)),c_translation_33))
% 0.54/0.66 => genls(c_tptpcol_15_40430,c_tptpcol_7_39939) ) ).
% 0.54/0.66
% 0.54/0.66 %------------------------------------------------------------------------------
% 0.54/0.66 %-------------------------------------------
% 0.54/0.66 % Proof found
% 0.54/0.66 % SZS status Theorem for theBenchmark
% 0.54/0.66 % SZS output start Proof
% 0.54/0.66 %ClaNum:97(EqnAxiom:0)
% 0.54/0.66 %VarNum:187(SingletonVarNum:103)
% 0.54/0.66 %MaxLitNum:3
% 0.54/0.66 %MaxfuncDepth:3
% 0.54/0.66 %SharedTerms:46
% 0.54/0.66 %goalClause: 23 29
% 0.54/0.66 %singleGoalClaCount:2
% 0.54/0.66 [1]P1(a1)
% 0.54/0.66 [2]P1(a2)
% 0.54/0.66 [3]P2(a3)
% 0.54/0.66 [4]P2(a7)
% 0.54/0.66 [7]P6(a4,a3)
% 0.54/0.66 [8]P6(a3,a7)
% 0.54/0.66 [9]P6(a5,a4)
% 0.54/0.66 [10]P6(a8,a5)
% 0.54/0.66 [11]P9(a9,a10)
% 0.54/0.66 [12]P9(a17,a9)
% 0.54/0.66 [13]P9(a11,a17)
% 0.54/0.66 [14]P9(a12,a11)
% 0.54/0.66 [15]P9(a13,a12)
% 0.54/0.66 [16]P9(a14,a13)
% 0.54/0.66 [17]P9(a15,a14)
% 0.54/0.66 [18]P9(a16,a15)
% 0.54/0.66 [29]~P9(a16,a10)
% 0.54/0.66 [23]P2(f23(f24(f20(a25)),a18))
% 0.54/0.66 [26]P6(f23(f24(f20(a25)),a18),a8)
% 0.54/0.66 [5]P26(f20(x51))
% 0.54/0.66 [6]P3(f24(x61))
% 0.54/0.66 [19]P13(f20(x191),a21)
% 0.54/0.66 [20]P13(f24(x201),a22)
% 0.54/0.66 [24]P14(f20(x241),a26,x241)
% 0.54/0.66 [25]P14(f24(x251),a26,x251)
% 0.54/0.66 [21]P11(f23(x211,x212))
% 0.54/0.66 [22]P13(f23(x221,x222),a6)
% 0.54/0.66 [27]P14(f23(x271,x272),a26,x271)
% 0.54/0.66 [28]P14(f23(x281,x282),a27,x282)
% 0.54/0.66 [30]~P25(x301)+P15(x301)
% 0.54/0.66 [31]~P15(x311)+P16(x311)
% 0.54/0.66 [32]~P17(x321)+P25(x321)
% 0.54/0.66 [33]~P20(x331)+P17(x331)
% 0.54/0.66 [34]~P21(x341)+P20(x341)
% 0.54/0.66 [35]~P22(x351)+P21(x351)
% 0.54/0.66 [36]~P23(x361)+P22(x361)
% 0.54/0.66 [37]~P24(x371)+P23(x371)
% 0.54/0.66 [38]~P15(x381)+P12(x381,a9)
% 0.54/0.66 [39]~P16(x391)+P12(x391,a10)
% 0.54/0.66 [40]~P25(x401)+P12(x401,a17)
% 0.54/0.66 [41]~P17(x411)+P12(x411,a11)
% 0.54/0.66 [42]~P20(x421)+P12(x421,a12)
% 0.54/0.66 [43]~P21(x431)+P12(x431,a13)
% 0.54/0.66 [44]~P22(x441)+P12(x441,a14)
% 0.54/0.66 [45]~P23(x451)+P12(x451,a15)
% 0.54/0.66 [46]~P24(x461)+P12(x461,a16)
% 0.54/0.66 [47]~P1(x471)+P12(x471,a19)
% 0.54/0.66 [49]~P11(x491)+P6(x491,x491)
% 0.54/0.66 [51]~P4(x511)+P9(x511,x511)
% 0.54/0.66 [53]~P18(x531)+P10(x531,x531)
% 0.54/0.66 [54]P1(x541)+~P12(x541,a19)
% 0.54/0.66 [55]P15(x551)+~P12(x551,a9)
% 0.54/0.66 [56]P16(x561)+~P12(x561,a10)
% 0.54/0.66 [57]P25(x571)+~P12(x571,a17)
% 0.54/0.66 [58]P17(x581)+~P12(x581,a11)
% 0.54/0.66 [59]P20(x591)+~P12(x591,a12)
% 0.54/0.66 [60]P21(x601)+~P12(x601,a13)
% 0.54/0.66 [61]P22(x611)+~P12(x611,a14)
% 0.54/0.66 [62]P23(x621)+~P12(x621,a15)
% 0.54/0.66 [63]P24(x631)+~P12(x631,a16)
% 0.54/0.66 [65]P18(x651)+~P10(x652,x651)
% 0.54/0.66 [67]P18(x671)+~P10(x671,x672)
% 0.54/0.66 [68]P5(x681)+~P7(x682,x681)
% 0.54/0.66 [69]P5(x691)+~P7(x691,x692)
% 0.54/0.66 [71]P4(x711)+~P9(x712,x711)
% 0.54/0.66 [73]P4(x731)+~P12(x732,x731)
% 0.54/0.66 [74]P4(x741)+~P8(x742,x741)
% 0.54/0.66 [76]P4(x761)+~P9(x761,x762)
% 0.54/0.66 [77]P4(x771)+~P8(x771,x772)
% 0.54/0.66 [79]P11(x791)+~P6(x792,x791)
% 0.54/0.66 [81]P11(x811)+~P6(x811,x812)
% 0.54/0.66 [83]P19(x831)+~P12(x831,x832)
% 0.54/0.66 [85]~P8(x852,x851)+P8(x851,x852)
% 0.54/0.66 [84]~P6(x842,x841)+P2(x841)+~P2(x842)
% 0.54/0.66 [86]~P6(x861,x863)+P6(x861,x862)+~P6(x863,x862)
% 0.54/0.66 [89]~P9(x891,x893)+P9(x891,x892)+~P9(x893,x892)
% 0.54/0.66 [90]~P12(x901,x903)+P12(x901,x902)+~P9(x903,x902)
% 0.54/0.66 [91]~P8(x913,x912)+P8(x911,x912)+~P9(x911,x913)
% 0.54/0.66 [92]~P8(x921,x923)+P8(x921,x922)+~P9(x922,x923)
% 0.54/0.66 [93]~P10(x931,x933)+P7(x931,x932)+~P7(x933,x932)
% 0.54/0.66 [94]~P10(x943,x942)+P7(x941,x942)+~P7(x941,x943)
% 0.54/0.66 [95]~P7(x951,x953)+P10(x951,x952)+~P7(x953,x952)
% 0.54/0.66 [96]~P10(x961,x963)+P10(x961,x962)+~P10(x963,x962)
% 0.54/0.66 [97]~P8(x973,x972)+~P12(x971,x972)+~P12(x971,x973)
% 0.54/0.66 %EqnAxiom
% 0.54/0.66
% 0.54/0.66 %-------------------------------------------
% 0.54/0.66 cnf(98,plain,
% 0.54/0.66 (P9(a17,a10)),
% 0.54/0.66 inference(scs_inference,[],[11,12,89])).
% 0.54/0.66 cnf(107,plain,
% 0.54/0.66 (P6(a4,a7)),
% 0.54/0.66 inference(scs_inference,[],[7,8,86])).
% 0.54/0.66 cnf(109,plain,
% 0.54/0.66 (P9(a11,a10)),
% 0.54/0.66 inference(scs_inference,[],[98,7,8,13,86,89])).
% 0.54/0.66 cnf(128,plain,
% 0.54/0.66 (P9(a12,a10)),
% 0.54/0.66 inference(scs_inference,[],[109,14,89])).
% 0.54/0.66 cnf(138,plain,
% 0.54/0.66 (P6(a5,a7)),
% 0.54/0.66 inference(scs_inference,[],[107,9,86])).
% 0.54/0.66 cnf(140,plain,
% 0.54/0.66 (P9(a13,a10)),
% 0.54/0.66 inference(scs_inference,[],[128,15,107,9,86,89])).
% 0.54/0.66 cnf(148,plain,
% 0.54/0.66 (P9(a14,a10)),
% 0.54/0.66 inference(scs_inference,[],[140,16,89])).
% 0.54/0.66 cnf(160,plain,
% 0.54/0.66 (P9(a15,a10)),
% 0.54/0.66 inference(scs_inference,[],[148,17,138,10,86,89])).
% 0.54/0.66 cnf(168,plain,
% 0.54/0.66 ($false),
% 0.54/0.66 inference(scs_inference,[],[29,160,18,89]),
% 0.54/0.66 ['proof']).
% 0.54/0.66 % SZS output end Proof
% 0.54/0.66 % Total time :0.010000s
%------------------------------------------------------------------------------