%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CSR040+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 : n019.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:18 EDT 2024
% Result : Theorem 0.62s 0.64s
% Output : CNFRefutation 0.62s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : CSR040+1 : TPTP v8.2.0. Released v3.4.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n019.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 : Thu Jun 20 00:41:24 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.19/0.56 start to proof:theBenchmark
% 0.54/0.62 %-------------------------------------------
% 0.54/0.62 % File :CSE---1.7
% 0.54/0.62 % Problem :theBenchmark
% 0.54/0.62 % Transform :cnf
% 0.54/0.62 % Format :tptp:raw
% 0.54/0.62 % Command :java -jar mcs_scs.jar %d %s
% 0.54/0.62
% 0.54/0.62 % Result :Theorem 0.020000s
% 0.54/0.62 % Output :CNFRefutation 0.020000s
% 0.54/0.62 %-------------------------------------------
% 0.54/0.62 %------------------------------------------------------------------------------
% 0.54/0.62 % File : CSR040+1 : TPTP v8.2.0. Released v3.4.0.
% 0.54/0.62 % Domain : Common Sense Reasoning
% 0.54/0.62 % Problem : Autogenerated Cyc Problem CSR040+1
% 0.54/0.62 % Version : Especial.
% 0.54/0.62 % English :
% 0.54/0.62
% 0.54/0.62 % Refs : [RS+] Reagan Smith et al., The Cyc TPTP Challenge Problem
% 0.54/0.62 % Source : [RS+]
% 0.54/0.62 % Names :
% 0.54/0.62
% 0.54/0.62 % Status : Theorem
% 0.54/0.62 % 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.07 v6.3.0, 0.08 v6.2.0, 0.09 v6.1.0, 0.04 v6.0.0, 0.25 v5.5.0, 0.12 v5.4.0, 0.17 v5.3.0, 0.22 v5.2.0, 0.07 v5.0.0, 0.15 v4.1.0, 0.11 v4.0.1, 0.05 v3.7.0, 0.00 v3.4.0
% 0.54/0.62 % Syntax : Number of formulae : 146 ( 42 unt; 0 def)
% 0.54/0.62 % Number of atoms : 263 ( 0 equ)
% 0.54/0.62 % Maximal formula atoms : 3 ( 1 avg)
% 0.54/0.62 % Number of connectives : 120 ( 3 ~; 0 |; 15 &)
% 0.54/0.62 % ( 0 <=>; 102 =>; 0 <=; 0 <~>)
% 0.54/0.62 % Maximal formula depth : 7 ( 3 avg)
% 0.54/0.62 % Maximal term depth : 4 ( 1 avg)
% 0.54/0.62 % Number of predicates : 37 ( 37 usr; 0 prp; 1-3 aty)
% 0.54/0.62 % Number of functors : 40 ( 40 usr; 37 con; 0-2 aty)
% 0.54/0.62 % Number of variables : 163 ( 163 !; 0 ?)
% 0.54/0.62 % SPC : FOF_THM_RFO_NEQ
% 0.54/0.62
% 0.54/0.62 % Comments : Autogenerated from the OpenCyc KB. Documentation can be found at
% 0.54/0.62 % http://opencyc.org/doc/#TPTP_Challenge_Problem_Set
% 0.54/0.62 % : Cyc(R) Knowledge Base Copyright(C) 1995-2007 Cycorp, Inc., Austin,
% 0.54/0.62 % TX, USA. All rights reserved.
% 0.54/0.62 % : OpenCyc Knowledge Base Copyright(C) 2001-2007 Cycorp, Inc.,
% 0.54/0.62 % Austin, TX, USA. All rights reserved.
% 0.54/0.62 %------------------------------------------------------------------------------
% 0.54/0.62 %$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.62 %$static(cyc_scaling_1,include('Axioms/CSR002+0.ax'))
% 0.54/0.62 %----Empty file include('Axioms/CSR002+0.ax').
% 0.54/0.62 %------------------------------------------------------------------------------
% 0.54/0.62 % Cyc Assertion #146206:
% 0.54/0.62 fof(just1,axiom,
% 0.54/0.62 genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14),c_machinelearningspindleheadmt) ).
% 0.54/0.62
% 0.54/0.62 % Cyc Assertion #592971:
% 0.54/0.62 fof(just2,axiom,
% 0.54/0.62 genlmt(c_cycorpproductsmt,c_basekb) ).
% 0.54/0.62
% 0.54/0.62 % Cyc Assertion #595427:
% 0.54/0.62 fof(just3,axiom,
% 0.54/0.62 genls(c_firstordercollection,c_fixedordercollection) ).
% 0.54/0.62
% 0.54/0.62 fof(just4,axiom,
% 0.54/0.62 ! [OBJ] :
% 0.54/0.62 ( firstordercollection(OBJ)
% 0.54/0.62 => fixedordercollection(OBJ) ) ).
% 0.54/0.62
% 0.54/0.62 % Cyc Assertion #600900:
% 0.54/0.62 fof(just5,axiom,
% 0.54/0.62 genlmt(c_cycnounlearnermt,c_cycorpproductsmt) ).
% 0.54/0.62
% 0.54/0.62 % Cyc Assertion #954903:
% 0.54/0.62 fof(just6,axiom,
% 0.54/0.62 genlmt(c_universalvocabularymt,c_corecyclmt) ).
% 0.54/0.62
% 0.54/0.62 % Cyc Assertion #1322220:
% 0.54/0.62 fof(just7,axiom,
% 0.54/0.62 transitivebinarypredicate(c_genlmt) ).
% 0.54/0.62
% 0.54/0.62 % Cyc Assertion #1326245:
% 0.54/0.62 fof(just8,axiom,
% 0.54/0.62 genlmt(c_corecyclmt,c_logicaltruthmt) ).
% 0.54/0.62
% 0.54/0.62 % Cyc Assertion #1558442:
% 0.54/0.62 fof(just9,axiom,
% 0.54/0.62 ! [OBJ] :
% 0.54/0.62 ~ ( collection(OBJ)
% 0.54/0.62 & individual(OBJ) ) ).
% 0.54/0.62
% 0.54/0.62 fof(just10,axiom,
% 0.54/0.62 disjointwith(c_collection,c_individual) ).
% 0.54/0.62
% 0.54/0.62 % Cyc Assertion #1614635:
% 0.54/0.62 fof(just11,axiom,
% 0.54/0.62 genlmt(c_machinelearningspindleheadmt,c_cycnounlearnermt) ).
% 0.54/0.62
% 0.54/0.62 % Cyc Assertion #1650755:
% 0.54/0.62 fof(just12,axiom,
% 0.54/0.62 genlmt(c_basekb,c_universalvocabularymt) ).
% 0.54/0.62
% 0.54/0.62 % Cyc Assertion #1778144:
% 0.54/0.62 fof(just13,axiom,
% 0.54/0.62 genls(c_fixedordercollection,c_collection) ).
% 0.54/0.62
% 0.54/0.62 fof(just14,axiom,
% 0.54/0.62 ! [OBJ] :
% 0.54/0.62 ( fixedordercollection(OBJ)
% 0.54/0.62 => collection(OBJ) ) ).
% 0.54/0.62
% 0.54/0.63 % Cyc Assertion #1822752:
% 0.54/0.63 fof(just15,axiom,
% 0.54/0.63 genls(c_tptpcol_0_0,c_individual) ).
% 0.54/0.63
% 0.54/0.63 fof(just16,axiom,
% 0.54/0.63 ! [OBJ] :
% 0.54/0.63 ( tptpcol_0_0(OBJ)
% 0.54/0.63 => individual(OBJ) ) ).
% 0.54/0.63
% 0.54/0.63 % Cyc Assertion #1978206:
% 0.54/0.63 fof(just17,axiom,
% 0.54/0.63 firstordercollection(c_tptpcol_16_62187) ).
% 0.54/0.63
% 0.54/0.63 % Cyc Assertion #1986591:
% 0.54/0.63 fof(just18,axiom,
% 0.54/0.63 genls(c_tptpcol_1_65536,c_tptpcol_0_0) ).
% 0.54/0.63
% 0.54/0.63 fof(just19,axiom,
% 0.54/0.63 ! [OBJ] :
% 0.54/0.63 ( tptpcol_1_65536(OBJ)
% 0.54/0.63 => tptpcol_0_0(OBJ) ) ).
% 0.54/0.63
% 0.54/0.63 % Cyc Assertion #2068510:
% 0.54/0.63 fof(just20,axiom,
% 0.54/0.63 genls(c_tptpcol_2_98304,c_tptpcol_1_65536) ).
% 0.54/0.63
% 0.54/0.63 fof(just21,axiom,
% 0.54/0.63 ! [OBJ] :
% 0.54/0.63 ( tptpcol_2_98304(OBJ)
% 0.54/0.63 => tptpcol_1_65536(OBJ) ) ).
% 0.54/0.63
% 0.54/0.63 % Cyc Assertion #2068512:
% 0.54/0.63 fof(just22,axiom,
% 0.54/0.63 genls(c_tptpcol_3_98305,c_tptpcol_2_98304) ).
% 0.54/0.63
% 0.54/0.63 fof(just23,axiom,
% 0.54/0.63 ! [OBJ] :
% 0.54/0.63 ( tptpcol_3_98305(OBJ)
% 0.54/0.63 => tptpcol_2_98304(OBJ) ) ).
% 0.54/0.63
% 0.54/0.63 % Cyc Assertion #2088991:
% 0.54/0.63 fof(just24,axiom,
% 0.54/0.63 genls(c_tptpcol_4_106497,c_tptpcol_3_98305) ).
% 0.54/0.63
% 0.54/0.63 fof(just25,axiom,
% 0.54/0.63 ! [OBJ] :
% 0.54/0.63 ( tptpcol_4_106497(OBJ)
% 0.54/0.63 => tptpcol_3_98305(OBJ) ) ).
% 0.54/0.63
% 0.54/0.63 % Cyc Assertion #2088993:
% 0.54/0.63 fof(just26,axiom,
% 0.54/0.63 genls(c_tptpcol_5_106498,c_tptpcol_4_106497) ).
% 0.54/0.63
% 0.54/0.63 fof(just27,axiom,
% 0.54/0.63 ! [OBJ] :
% 0.54/0.63 ( tptpcol_5_106498(OBJ)
% 0.54/0.63 => tptpcol_4_106497(OBJ) ) ).
% 0.54/0.63
% 0.54/0.63 % Cyc Assertion #2094112:
% 0.54/0.63 fof(just28,axiom,
% 0.54/0.63 genls(c_tptpcol_6_108546,c_tptpcol_5_106498) ).
% 0.54/0.63
% 0.54/0.63 fof(just29,axiom,
% 0.54/0.63 ! [OBJ] :
% 0.54/0.63 ( tptpcol_6_108546(OBJ)
% 0.54/0.63 => tptpcol_5_106498(OBJ) ) ).
% 0.54/0.63
% 0.54/0.63 % Cyc Assertion #2094114:
% 0.54/0.63 fof(just30,axiom,
% 0.54/0.63 genls(c_tptpcol_7_108547,c_tptpcol_6_108546) ).
% 0.54/0.63
% 0.54/0.63 fof(just31,axiom,
% 0.54/0.63 ! [OBJ] :
% 0.54/0.63 ( tptpcol_7_108547(OBJ)
% 0.54/0.63 => tptpcol_6_108546(OBJ) ) ).
% 0.54/0.63
% 0.54/0.63 % Cyc Assertion #2095393:
% 0.54/0.63 fof(just32,axiom,
% 0.54/0.63 genls(c_tptpcol_8_109059,c_tptpcol_7_108547) ).
% 0.54/0.63
% 0.54/0.63 fof(just33,axiom,
% 0.54/0.63 ! [OBJ] :
% 0.54/0.63 ( tptpcol_8_109059(OBJ)
% 0.54/0.63 => tptpcol_7_108547(OBJ) ) ).
% 0.54/0.63
% 0.54/0.63 % Cyc Assertion #2095395:
% 0.54/0.63 fof(just34,axiom,
% 0.54/0.63 genls(c_tptpcol_9_109060,c_tptpcol_8_109059) ).
% 0.54/0.63
% 0.54/0.63 fof(just35,axiom,
% 0.54/0.63 ! [OBJ] :
% 0.54/0.63 ( tptpcol_9_109060(OBJ)
% 0.54/0.63 => tptpcol_8_109059(OBJ) ) ).
% 0.54/0.63
% 0.54/0.63 % Cyc Assertion #2095397:
% 0.54/0.63 fof(just36,axiom,
% 0.54/0.63 genls(c_tptpcol_10_109061,c_tptpcol_9_109060) ).
% 0.54/0.63
% 0.54/0.63 fof(just37,axiom,
% 0.54/0.63 ! [OBJ] :
% 0.54/0.63 ( tptpcol_10_109061(OBJ)
% 0.54/0.63 => tptpcol_9_109060(OBJ) ) ).
% 0.54/0.63
% 0.54/0.63 % Cyc Assertion #2095556:
% 0.54/0.63 fof(just38,axiom,
% 0.54/0.63 genls(c_tptpcol_11_109125,c_tptpcol_10_109061) ).
% 0.54/0.63
% 0.54/0.63 fof(just39,axiom,
% 0.54/0.63 ! [OBJ] :
% 0.54/0.63 ( tptpcol_11_109125(OBJ)
% 0.54/0.63 => tptpcol_10_109061(OBJ) ) ).
% 0.54/0.63
% 0.54/0.63 % Cyc Assertion #2095635:
% 0.54/0.63 fof(just40,axiom,
% 0.54/0.63 genls(c_tptpcol_12_109157,c_tptpcol_11_109125) ).
% 0.54/0.63
% 0.54/0.63 fof(just41,axiom,
% 0.54/0.63 ! [OBJ] :
% 0.54/0.63 ( tptpcol_12_109157(OBJ)
% 0.54/0.63 => tptpcol_11_109125(OBJ) ) ).
% 0.54/0.63
% 0.54/0.63 % Cyc Assertion #2095674:
% 0.54/0.63 fof(just42,axiom,
% 0.54/0.63 genls(c_tptpcol_13_109173,c_tptpcol_12_109157) ).
% 0.54/0.63
% 0.54/0.63 fof(just43,axiom,
% 0.54/0.63 ! [OBJ] :
% 0.54/0.63 ( tptpcol_13_109173(OBJ)
% 0.54/0.63 => tptpcol_12_109157(OBJ) ) ).
% 0.54/0.63
% 0.54/0.63 % Cyc Assertion #2095693:
% 0.54/0.63 fof(just44,axiom,
% 0.54/0.63 genls(c_tptpcol_14_109181,c_tptpcol_13_109173) ).
% 0.54/0.63
% 0.54/0.63 fof(just45,axiom,
% 0.54/0.63 ! [OBJ] :
% 0.54/0.63 ( tptpcol_14_109181(OBJ)
% 0.54/0.63 => tptpcol_13_109173(OBJ) ) ).
% 0.54/0.63
% 0.54/0.63 % Cyc Assertion #2095702:
% 0.54/0.63 fof(just46,axiom,
% 0.54/0.63 genls(c_tptpcol_15_109185,c_tptpcol_14_109181) ).
% 0.54/0.63
% 0.54/0.63 fof(just47,axiom,
% 0.54/0.63 ! [OBJ] :
% 0.54/0.63 ( tptpcol_15_109185(OBJ)
% 0.54/0.63 => tptpcol_14_109181(OBJ) ) ).
% 0.54/0.63
% 0.54/0.63 % Cyc Assertion #398814:
% 0.54/0.63 fof(just48,axiom,
% 0.54/0.63 ! [OBJ,COL1,COL2] :
% 0.54/0.63 ~ ( isa(OBJ,COL1)
% 0.54/0.63 & isa(OBJ,COL2)
% 0.54/0.63 & disjointwith(COL1,COL2) ) ).
% 0.54/0.63
% 0.54/0.63 % Cyc Assertion #831913:
% 0.54/0.63 fof(just49,axiom,
% 0.54/0.63 ! [SPECPRED,PRED,GENLPRED] :
% 0.54/0.63 ( ( genlinverse(SPECPRED,PRED)
% 0.54/0.63 & genlinverse(PRED,GENLPRED) )
% 0.54/0.63 => genlpreds(SPECPRED,GENLPRED) ) ).
% 0.54/0.63
% 0.54/0.63 % Cyc Constant #40273:
% 0.54/0.63 fof(just50,axiom,
% 0.54/0.63 ! [ARG1,INS] :
% 0.54/0.63 ( genlpreds(ARG1,INS)
% 0.54/0.63 => predicate(INS) ) ).
% 0.54/0.63
% 0.54/0.63 fof(just51,axiom,
% 0.54/0.63 ! [ARG1,INS] :
% 0.54/0.63 ( genlpreds(ARG1,INS)
% 0.54/0.63 => predicate(INS) ) ).
% 0.54/0.63
% 0.54/0.63 fof(just52,axiom,
% 0.54/0.63 ! [INS,ARG2] :
% 0.54/0.63 ( genlpreds(INS,ARG2)
% 0.54/0.63 => predicate(INS) ) ).
% 0.54/0.63
% 0.54/0.63 fof(just53,axiom,
% 0.54/0.63 ! [INS,ARG2] :
% 0.54/0.63 ( genlpreds(INS,ARG2)
% 0.54/0.63 => predicate(INS) ) ).
% 0.54/0.63
% 0.54/0.63 fof(just54,axiom,
% 0.54/0.63 ! [X,Y,Z] :
% 0.54/0.63 ( ( genlpreds(X,Y)
% 0.54/0.63 & genlpreds(Y,Z) )
% 0.54/0.63 => genlpreds(X,Z) ) ).
% 0.54/0.63
% 0.54/0.63 fof(just55,axiom,
% 0.54/0.63 ! [X] :
% 0.54/0.63 ( predicate(X)
% 0.54/0.63 => genlpreds(X,X) ) ).
% 0.54/0.63
% 0.54/0.63 fof(just56,axiom,
% 0.54/0.63 ! [X] :
% 0.54/0.63 ( predicate(X)
% 0.54/0.63 => genlpreds(X,X) ) ).
% 0.54/0.63
% 0.54/0.63 % Cyc Constant #45259:
% 0.54/0.63 fof(just57,axiom,
% 0.54/0.63 ! [ARG1,INS] :
% 0.54/0.63 ( genlinverse(ARG1,INS)
% 0.54/0.63 => binarypredicate(INS) ) ).
% 0.54/0.63
% 0.54/0.63 fof(just58,axiom,
% 0.54/0.63 ! [INS,ARG2] :
% 0.54/0.63 ( genlinverse(INS,ARG2)
% 0.54/0.63 => binarypredicate(INS) ) ).
% 0.54/0.63
% 0.54/0.63 fof(just59,axiom,
% 0.54/0.63 ! [OLD,ARG2,NEW] :
% 0.54/0.63 ( ( genlinverse(OLD,ARG2)
% 0.54/0.63 & genlpreds(NEW,OLD) )
% 0.54/0.63 => genlinverse(NEW,ARG2) ) ).
% 0.54/0.63
% 0.54/0.63 fof(just60,axiom,
% 0.54/0.63 ! [ARG1,OLD,NEW] :
% 0.54/0.63 ( ( genlinverse(ARG1,OLD)
% 0.54/0.63 & genlpreds(OLD,NEW) )
% 0.54/0.63 => genlinverse(ARG1,NEW) ) ).
% 0.54/0.63
% 0.54/0.63 % Cyc Constant #238782:
% 0.54/0.63 fof(just61,axiom,
% 0.54/0.63 ! [X] :
% 0.54/0.63 ( isa(X,c_tptpcol_15_109185)
% 0.54/0.63 => tptpcol_15_109185(X) ) ).
% 0.54/0.63
% 0.54/0.63 fof(just62,axiom,
% 0.54/0.63 ! [X] :
% 0.54/0.63 ( tptpcol_15_109185(X)
% 0.54/0.63 => isa(X,c_tptpcol_15_109185) ) ).
% 0.54/0.63
% 0.54/0.63 % Cyc Constant #238778:
% 0.54/0.63 fof(just63,axiom,
% 0.54/0.63 ! [X] :
% 0.54/0.63 ( isa(X,c_tptpcol_14_109181)
% 0.54/0.63 => tptpcol_14_109181(X) ) ).
% 0.54/0.63
% 0.54/0.63 fof(just64,axiom,
% 0.54/0.63 ! [X] :
% 0.54/0.63 ( tptpcol_14_109181(X)
% 0.54/0.63 => isa(X,c_tptpcol_14_109181) ) ).
% 0.54/0.63
% 0.54/0.63 % Cyc Constant #238770:
% 0.54/0.63 fof(just65,axiom,
% 0.54/0.63 ! [X] :
% 0.54/0.63 ( isa(X,c_tptpcol_13_109173)
% 0.54/0.63 => tptpcol_13_109173(X) ) ).
% 0.54/0.63
% 0.54/0.63 fof(just66,axiom,
% 0.54/0.63 ! [X] :
% 0.54/0.63 ( tptpcol_13_109173(X)
% 0.54/0.63 => isa(X,c_tptpcol_13_109173) ) ).
% 0.54/0.63
% 0.54/0.63 % Cyc Constant #238754:
% 0.54/0.63 fof(just67,axiom,
% 0.54/0.63 ! [X] :
% 0.54/0.63 ( isa(X,c_tptpcol_12_109157)
% 0.54/0.63 => tptpcol_12_109157(X) ) ).
% 0.54/0.63
% 0.54/0.63 fof(just68,axiom,
% 0.54/0.63 ! [X] :
% 0.54/0.63 ( tptpcol_12_109157(X)
% 0.54/0.63 => isa(X,c_tptpcol_12_109157) ) ).
% 0.54/0.63
% 0.54/0.63 % Cyc Constant #238722:
% 0.54/0.63 fof(just69,axiom,
% 0.54/0.63 ! [X] :
% 0.54/0.63 ( isa(X,c_tptpcol_11_109125)
% 0.54/0.63 => tptpcol_11_109125(X) ) ).
% 0.54/0.63
% 0.54/0.63 fof(just70,axiom,
% 0.54/0.63 ! [X] :
% 0.54/0.63 ( tptpcol_11_109125(X)
% 0.54/0.63 => isa(X,c_tptpcol_11_109125) ) ).
% 0.54/0.63
% 0.54/0.63 % Cyc Constant #238658:
% 0.54/0.63 fof(just71,axiom,
% 0.54/0.63 ! [X] :
% 0.54/0.63 ( isa(X,c_tptpcol_10_109061)
% 0.54/0.63 => tptpcol_10_109061(X) ) ).
% 0.54/0.63
% 0.54/0.63 fof(just72,axiom,
% 0.54/0.63 ! [X] :
% 0.54/0.63 ( tptpcol_10_109061(X)
% 0.62/0.63 => isa(X,c_tptpcol_10_109061) ) ).
% 0.62/0.63
% 0.62/0.63 % Cyc Constant #238657:
% 0.62/0.63 fof(just73,axiom,
% 0.62/0.63 ! [X] :
% 0.62/0.63 ( isa(X,c_tptpcol_9_109060)
% 0.62/0.63 => tptpcol_9_109060(X) ) ).
% 0.62/0.63
% 0.62/0.63 fof(just74,axiom,
% 0.62/0.63 ! [X] :
% 0.62/0.63 ( tptpcol_9_109060(X)
% 0.62/0.63 => isa(X,c_tptpcol_9_109060) ) ).
% 0.62/0.63
% 0.62/0.63 % Cyc Constant #238656:
% 0.62/0.63 fof(just75,axiom,
% 0.62/0.63 ! [X] :
% 0.62/0.63 ( isa(X,c_tptpcol_8_109059)
% 0.62/0.63 => tptpcol_8_109059(X) ) ).
% 0.62/0.63
% 0.62/0.63 fof(just76,axiom,
% 0.62/0.63 ! [X] :
% 0.62/0.63 ( tptpcol_8_109059(X)
% 0.62/0.63 => isa(X,c_tptpcol_8_109059) ) ).
% 0.62/0.63
% 0.62/0.63 % Cyc Constant #238144:
% 0.62/0.63 fof(just77,axiom,
% 0.62/0.63 ! [X] :
% 0.62/0.63 ( isa(X,c_tptpcol_7_108547)
% 0.62/0.63 => tptpcol_7_108547(X) ) ).
% 0.62/0.63
% 0.62/0.63 fof(just78,axiom,
% 0.62/0.63 ! [X] :
% 0.62/0.63 ( tptpcol_7_108547(X)
% 0.62/0.63 => isa(X,c_tptpcol_7_108547) ) ).
% 0.62/0.63
% 0.62/0.63 % Cyc Constant #238143:
% 0.62/0.63 fof(just79,axiom,
% 0.62/0.63 ! [X] :
% 0.62/0.63 ( isa(X,c_tptpcol_6_108546)
% 0.62/0.63 => tptpcol_6_108546(X) ) ).
% 0.62/0.63
% 0.62/0.63 fof(just80,axiom,
% 0.62/0.63 ! [X] :
% 0.62/0.63 ( tptpcol_6_108546(X)
% 0.62/0.63 => isa(X,c_tptpcol_6_108546) ) ).
% 0.62/0.63
% 0.62/0.63 % Cyc Constant #236095:
% 0.62/0.63 fof(just81,axiom,
% 0.62/0.63 ! [X] :
% 0.62/0.63 ( isa(X,c_tptpcol_5_106498)
% 0.62/0.63 => tptpcol_5_106498(X) ) ).
% 0.62/0.63
% 0.62/0.63 fof(just82,axiom,
% 0.62/0.63 ! [X] :
% 0.62/0.63 ( tptpcol_5_106498(X)
% 0.62/0.63 => isa(X,c_tptpcol_5_106498) ) ).
% 0.62/0.63
% 0.62/0.63 % Cyc Constant #236094:
% 0.62/0.63 fof(just83,axiom,
% 0.62/0.63 ! [X] :
% 0.62/0.63 ( isa(X,c_tptpcol_4_106497)
% 0.62/0.63 => tptpcol_4_106497(X) ) ).
% 0.62/0.63
% 0.62/0.63 fof(just84,axiom,
% 0.62/0.63 ! [X] :
% 0.62/0.63 ( tptpcol_4_106497(X)
% 0.62/0.63 => isa(X,c_tptpcol_4_106497) ) ).
% 0.62/0.63
% 0.62/0.63 % Cyc Constant #227902:
% 0.62/0.63 fof(just85,axiom,
% 0.62/0.63 ! [X] :
% 0.62/0.63 ( isa(X,c_tptpcol_3_98305)
% 0.62/0.63 => tptpcol_3_98305(X) ) ).
% 0.62/0.63
% 0.62/0.63 fof(just86,axiom,
% 0.62/0.63 ! [X] :
% 0.62/0.63 ( tptpcol_3_98305(X)
% 0.62/0.63 => isa(X,c_tptpcol_3_98305) ) ).
% 0.62/0.63
% 0.62/0.63 % Cyc Constant #227901:
% 0.62/0.63 fof(just87,axiom,
% 0.62/0.63 ! [X] :
% 0.62/0.63 ( isa(X,c_tptpcol_2_98304)
% 0.62/0.63 => tptpcol_2_98304(X) ) ).
% 0.62/0.63
% 0.62/0.63 fof(just88,axiom,
% 0.62/0.63 ! [X] :
% 0.62/0.63 ( tptpcol_2_98304(X)
% 0.62/0.63 => isa(X,c_tptpcol_2_98304) ) ).
% 0.62/0.63
% 0.62/0.63 % Cyc Constant #195133:
% 0.62/0.63 fof(just89,axiom,
% 0.62/0.63 ! [X] :
% 0.62/0.63 ( isa(X,c_tptpcol_1_65536)
% 0.62/0.63 => tptpcol_1_65536(X) ) ).
% 0.62/0.63
% 0.62/0.63 fof(just90,axiom,
% 0.62/0.63 ! [X] :
% 0.62/0.63 ( tptpcol_1_65536(X)
% 0.62/0.63 => isa(X,c_tptpcol_1_65536) ) ).
% 0.62/0.63
% 0.62/0.63 % Cyc Constant #191784:
% 0.62/0.63 fof(just91,axiom,
% 0.62/0.63 ! [X] :
% 0.62/0.63 ( isa(X,c_tptpcol_16_62187)
% 0.62/0.63 => tptpcol_16_62187(X) ) ).
% 0.62/0.63
% 0.62/0.63 fof(just92,axiom,
% 0.62/0.64 ! [X] :
% 0.62/0.64 ( tptpcol_16_62187(X)
% 0.62/0.64 => isa(X,c_tptpcol_16_62187) ) ).
% 0.62/0.64
% 0.62/0.64 % Cyc Constant #129596:
% 0.62/0.64 fof(just93,axiom,
% 0.62/0.64 ! [X] :
% 0.62/0.64 ( isa(X,c_tptpcol_0_0)
% 0.62/0.64 => tptpcol_0_0(X) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just94,axiom,
% 0.62/0.64 ! [X] :
% 0.62/0.64 ( tptpcol_0_0(X)
% 0.62/0.64 => isa(X,c_tptpcol_0_0) ) ).
% 0.62/0.64
% 0.62/0.64 % Cyc Constant #113597:
% 0.62/0.64 fof(just95,axiom,
% 0.62/0.64 ! [X] :
% 0.62/0.64 ( isa(X,c_individual)
% 0.62/0.64 => individual(X) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just96,axiom,
% 0.62/0.64 ! [X] :
% 0.62/0.64 ( individual(X)
% 0.62/0.64 => isa(X,c_individual) ) ).
% 0.62/0.64
% 0.62/0.64 % Cyc Constant #19726:
% 0.62/0.64 fof(just97,axiom,
% 0.62/0.64 ! [X] :
% 0.62/0.64 ( isa(X,c_collection)
% 0.62/0.64 => collection(X) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just98,axiom,
% 0.62/0.64 ! [X] :
% 0.62/0.64 ( collection(X)
% 0.62/0.64 => isa(X,c_collection) ) ).
% 0.62/0.64
% 0.62/0.64 % Cyc Constant #78648:
% 0.62/0.64 fof(just99,axiom,
% 0.62/0.64 ! [ARG1,INS] :
% 0.62/0.64 ( disjointwith(ARG1,INS)
% 0.62/0.64 => collection(INS) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just100,axiom,
% 0.62/0.64 ! [INS,ARG2] :
% 0.62/0.64 ( disjointwith(INS,ARG2)
% 0.62/0.64 => collection(INS) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just101,axiom,
% 0.62/0.64 ! [X,Y] :
% 0.62/0.64 ( disjointwith(X,Y)
% 0.62/0.64 => disjointwith(Y,X) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just102,axiom,
% 0.62/0.64 ! [ARG1,OLD,NEW] :
% 0.62/0.64 ( ( disjointwith(ARG1,OLD)
% 0.62/0.64 & genls(NEW,OLD) )
% 0.62/0.64 => disjointwith(ARG1,NEW) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just103,axiom,
% 0.62/0.64 ! [OLD,ARG2,NEW] :
% 0.62/0.64 ( ( disjointwith(OLD,ARG2)
% 0.62/0.64 & genls(NEW,OLD) )
% 0.62/0.64 => disjointwith(NEW,ARG2) ) ).
% 0.62/0.64
% 0.62/0.64 % Cyc Constant #52963:
% 0.62/0.64 fof(just104,axiom,
% 0.62/0.64 mtvisible(c_logicaltruthmt) ).
% 0.62/0.64
% 0.62/0.64 % Cyc Constant #127156:
% 0.62/0.64 fof(just105,axiom,
% 0.62/0.64 ! [X] :
% 0.62/0.64 ( isa(X,c_transitivebinarypredicate)
% 0.62/0.64 => transitivebinarypredicate(X) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just106,axiom,
% 0.62/0.64 ! [X] :
% 0.62/0.64 ( transitivebinarypredicate(X)
% 0.62/0.64 => isa(X,c_transitivebinarypredicate) ) ).
% 0.62/0.64
% 0.62/0.64 % Cyc Constant #72115:
% 0.62/0.64 fof(just107,axiom,
% 0.62/0.64 ! [ARG1,INS] :
% 0.62/0.64 ( isa(ARG1,INS)
% 0.62/0.64 => collection(INS) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just108,axiom,
% 0.62/0.64 ! [ARG1,INS] :
% 0.62/0.64 ( isa(ARG1,INS)
% 0.62/0.64 => collection(INS) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just109,axiom,
% 0.62/0.64 ! [INS,ARG2] :
% 0.62/0.64 ( isa(INS,ARG2)
% 0.62/0.64 => thing(INS) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just110,axiom,
% 0.62/0.64 ! [INS,ARG2] :
% 0.62/0.64 ( isa(INS,ARG2)
% 0.62/0.64 => thing(INS) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just111,axiom,
% 0.62/0.64 ! [ARG1,OLD,NEW] :
% 0.62/0.64 ( ( isa(ARG1,OLD)
% 0.62/0.64 & genls(OLD,NEW) )
% 0.62/0.64 => isa(ARG1,NEW) ) ).
% 0.62/0.64
% 0.62/0.64 % Cyc Constant #80185:
% 0.62/0.64 fof(just112,axiom,
% 0.62/0.64 mtvisible(c_corecyclmt) ).
% 0.62/0.64
% 0.62/0.64 % Cyc Constant #108004:
% 0.62/0.64 fof(just113,axiom,
% 0.62/0.64 ! [X] :
% 0.62/0.64 ( isa(X,c_fixedordercollection)
% 0.62/0.64 => fixedordercollection(X) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just114,axiom,
% 0.62/0.64 ! [X] :
% 0.62/0.64 ( fixedordercollection(X)
% 0.62/0.64 => isa(X,c_fixedordercollection) ) ).
% 0.62/0.64
% 0.62/0.64 % Cyc Constant #108957:
% 0.62/0.64 fof(just115,axiom,
% 0.62/0.64 ! [X] :
% 0.62/0.64 ( isa(X,c_firstordercollection)
% 0.62/0.64 => firstordercollection(X) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just116,axiom,
% 0.62/0.64 ! [X] :
% 0.62/0.64 ( firstordercollection(X)
% 0.62/0.64 => isa(X,c_firstordercollection) ) ).
% 0.62/0.64
% 0.62/0.64 % Cyc Constant #0:
% 0.62/0.64 fof(just117,axiom,
% 0.62/0.64 ! [ARG1,INS] :
% 0.62/0.64 ( genls(ARG1,INS)
% 0.62/0.64 => collection(INS) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just118,axiom,
% 0.62/0.64 ! [ARG1,INS] :
% 0.62/0.64 ( genls(ARG1,INS)
% 0.62/0.64 => collection(INS) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just119,axiom,
% 0.62/0.64 ! [INS,ARG2] :
% 0.62/0.64 ( genls(INS,ARG2)
% 0.62/0.64 => collection(INS) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just120,axiom,
% 0.62/0.64 ! [INS,ARG2] :
% 0.62/0.64 ( genls(INS,ARG2)
% 0.62/0.64 => collection(INS) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just121,axiom,
% 0.62/0.64 ! [X,Y,Z] :
% 0.62/0.64 ( ( genls(X,Y)
% 0.62/0.64 & genls(Y,Z) )
% 0.62/0.64 => genls(X,Z) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just122,axiom,
% 0.62/0.64 ! [X] :
% 0.62/0.64 ( collection(X)
% 0.62/0.64 => genls(X,X) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just123,axiom,
% 0.62/0.64 ! [X] :
% 0.62/0.64 ( collection(X)
% 0.62/0.64 => genls(X,X) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just124,axiom,
% 0.62/0.64 ! [OLD,ARG2,NEW] :
% 0.62/0.64 ( ( genls(OLD,ARG2)
% 0.62/0.64 & genls(NEW,OLD) )
% 0.62/0.64 => genls(NEW,ARG2) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just125,axiom,
% 0.62/0.64 ! [ARG1,OLD,NEW] :
% 0.62/0.64 ( ( genls(ARG1,OLD)
% 0.62/0.64 & genls(OLD,NEW) )
% 0.62/0.64 => genls(ARG1,NEW) ) ).
% 0.62/0.64
% 0.62/0.64 % Cyc Constant #27757:
% 0.62/0.64 fof(just126,axiom,
% 0.62/0.64 mtvisible(c_basekb) ).
% 0.62/0.64
% 0.62/0.64 % Cyc Constant #129091:
% 0.62/0.64 fof(just127,axiom,
% 0.62/0.64 ! [ARG1] : natfunction(f_urlfn(ARG1),c_urlfn) ).
% 0.62/0.64
% 0.62/0.64 fof(just128,axiom,
% 0.62/0.64 ! [ARG1] : natargument(f_urlfn(ARG1),n_1,ARG1) ).
% 0.62/0.64
% 0.62/0.64 fof(just129,axiom,
% 0.62/0.64 ! [ARG1] : uniformresourcelocator(f_urlfn(ARG1)) ).
% 0.62/0.64
% 0.62/0.64 % Cyc Constant #78971:
% 0.62/0.64 fof(just130,axiom,
% 0.62/0.64 ! [ARG1] : natfunction(f_urlreferentfn(ARG1),c_urlreferentfn) ).
% 0.62/0.64
% 0.62/0.64 fof(just131,axiom,
% 0.62/0.64 ! [ARG1] : natargument(f_urlreferentfn(ARG1),n_1,ARG1) ).
% 0.62/0.64
% 0.62/0.64 fof(just132,axiom,
% 0.62/0.64 ! [ARG1] : computerdataartifact(f_urlreferentfn(ARG1)) ).
% 0.62/0.64
% 0.62/0.64 % Cyc Constant #71728:
% 0.62/0.64 fof(just133,axiom,
% 0.62/0.64 ! [ARG1,ARG2] : natfunction(f_contentmtofcdafromeventfn(ARG1,ARG2),c_contentmtofcdafromeventfn) ).
% 0.62/0.64
% 0.62/0.64 fof(just134,axiom,
% 0.62/0.64 ! [ARG1,ARG2] : natargument(f_contentmtofcdafromeventfn(ARG1,ARG2),n_1,ARG1) ).
% 0.62/0.64
% 0.62/0.64 fof(just135,axiom,
% 0.62/0.64 ! [ARG1,ARG2] : natargument(f_contentmtofcdafromeventfn(ARG1,ARG2),n_2,ARG2) ).
% 0.62/0.64
% 0.62/0.64 fof(just136,axiom,
% 0.62/0.64 ! [ARG1,ARG2] : microtheory(f_contentmtofcdafromeventfn(ARG1,ARG2)) ).
% 0.62/0.64
% 0.62/0.64 % Cyc Constant #19550:
% 0.62/0.64 fof(just137,axiom,
% 0.62/0.64 ! [SPECMT,GENLMT] :
% 0.62/0.64 ( ( mtvisible(SPECMT)
% 0.62/0.64 & genlmt(SPECMT,GENLMT) )
% 0.62/0.64 => mtvisible(GENLMT) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just138,axiom,
% 0.62/0.64 ! [ARG1,INS] :
% 0.62/0.64 ( genlmt(ARG1,INS)
% 0.62/0.64 => microtheory(INS) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just139,axiom,
% 0.62/0.64 ! [ARG1,INS] :
% 0.62/0.64 ( genlmt(ARG1,INS)
% 0.62/0.64 => microtheory(INS) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just140,axiom,
% 0.62/0.64 ! [INS,ARG2] :
% 0.62/0.64 ( genlmt(INS,ARG2)
% 0.62/0.64 => microtheory(INS) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just141,axiom,
% 0.62/0.64 ! [INS,ARG2] :
% 0.62/0.64 ( genlmt(INS,ARG2)
% 0.62/0.64 => microtheory(INS) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just142,axiom,
% 0.62/0.64 ! [X,Y,Z] :
% 0.62/0.64 ( ( genlmt(X,Y)
% 0.62/0.64 & genlmt(Y,Z) )
% 0.62/0.64 => genlmt(X,Z) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just143,axiom,
% 0.62/0.64 ! [X] :
% 0.62/0.64 ( microtheory(X)
% 0.62/0.64 => genlmt(X,X) ) ).
% 0.62/0.64
% 0.62/0.64 fof(just144,axiom,
% 0.62/0.64 ! [X] :
% 0.62/0.64 ( microtheory(X)
% 0.62/0.64 => genlmt(X,X) ) ).
% 0.62/0.64
% 0.62/0.64 % Cyc Constant #95028:
% 0.62/0.64 fof(just145,axiom,
% 0.62/0.64 mtvisible(c_universalvocabularymt) ).
% 0.62/0.64
% 0.62/0.64 fof(query40,conjecture,
% 0.62/0.64 ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))
% 0.62/0.64 => ~ tptpcol_15_109185(c_tptpcol_16_62187) ) ).
% 0.62/0.64
% 0.62/0.64 %------------------------------------------------------------------------------
% 0.62/0.64 %-------------------------------------------
% 0.62/0.64 % Proof found
% 0.62/0.64 % SZS status Theorem for theBenchmark
% 0.62/0.64 % SZS output start Proof
% 0.62/0.64 %ClaNum:147(EqnAxiom:0)
% 0.62/0.64 %VarNum:257(SingletonVarNum:138)
% 0.62/0.64 %MaxLitNum:3
% 0.62/0.64 %MaxfuncDepth:3
% 0.62/0.64 %SharedTerms:74
% 0.62/0.64 %goalClause: 3 39
% 0.62/0.64 %singleGoalClaCount:2
% 0.62/0.64 [1]P1(a1)
% 0.62/0.64 [2]P6(a2)
% 0.62/0.64 [3]P7(a1)
% 0.62/0.64 [4]P8(a3)
% 0.62/0.64 [5]P8(a21)
% 0.62/0.64 [6]P8(a4)
% 0.62/0.64 [7]P8(a11)
% 0.62/0.64 [10]P9(a13,a7)
% 0.62/0.64 [11]P9(a8,a3)
% 0.62/0.64 [12]P9(a3,a21)
% 0.62/0.64 [13]P9(a7,a8)
% 0.62/0.64 [14]P9(a21,a4)
% 0.62/0.64 [15]P9(a4,a11)
% 0.62/0.64 [16]P12(a9,a10)
% 0.62/0.64 [17]P12(a10,a5)
% 0.62/0.64 [18]P12(a14,a12)
% 0.62/0.64 [19]P12(a22,a14)
% 0.62/0.64 [20]P12(a23,a22)
% 0.62/0.64 [21]P12(a24,a23)
% 0.62/0.64 [22]P12(a25,a24)
% 0.62/0.64 [23]P12(a26,a25)
% 0.62/0.64 [24]P12(a27,a26)
% 0.62/0.64 [25]P12(a28,a27)
% 0.62/0.64 [26]P12(a29,a28)
% 0.62/0.64 [27]P12(a30,a29)
% 0.62/0.64 [28]P12(a15,a30)
% 0.62/0.64 [29]P12(a16,a15)
% 0.62/0.64 [30]P12(a17,a16)
% 0.62/0.64 [31]P12(a18,a17)
% 0.62/0.64 [32]P12(a19,a18)
% 0.62/0.64 [33]P12(a20,a19)
% 0.62/0.64 [34]P5(a5,a12)
% 0.62/0.64 [39]P8(f36(f37(f33(a38)),a31))
% 0.62/0.64 [42]P9(f36(f37(f33(a38)),a31),a13)
% 0.62/0.64 [8]P37(f33(x81))
% 0.62/0.64 [9]P2(f37(x91))
% 0.62/0.64 [35]P17(f33(x351),a34)
% 0.62/0.64 [36]P17(f37(x361),a35)
% 0.62/0.64 [40]P18(f33(x401),a39,x401)
% 0.62/0.64 [41]P18(f37(x411),a39,x411)
% 0.62/0.64 [37]P14(f36(x371,x372))
% 0.62/0.64 [38]P17(f36(x381,x382),a6)
% 0.62/0.64 [43]P18(f36(x431,x432),a39,x431)
% 0.62/0.64 [44]P18(f36(x441,x442),a40,x442)
% 0.62/0.64 [45]~P1(x451)+P10(x451)
% 0.62/0.64 [46]~P10(x461)+P3(x461)
% 0.62/0.64 [47]~P19(x471)+P15(x471)
% 0.62/0.64 [48]~P27(x481)+P19(x481)
% 0.62/0.64 [49]~P29(x491)+P27(x491)
% 0.62/0.64 [50]~P30(x501)+P29(x501)
% 0.62/0.64 [51]~P31(x511)+P30(x511)
% 0.62/0.64 [52]~P32(x521)+P31(x521)
% 0.62/0.64 [53]~P33(x531)+P32(x531)
% 0.62/0.64 [54]~P34(x541)+P33(x541)
% 0.62/0.64 [55]~P35(x551)+P34(x551)
% 0.62/0.64 [56]~P36(x561)+P35(x561)
% 0.62/0.64 [57]~P22(x571)+P36(x571)
% 0.62/0.64 [58]~P23(x581)+P22(x581)
% 0.62/0.64 [59]~P24(x591)+P23(x591)
% 0.62/0.64 [60]~P25(x601)+P24(x601)
% 0.62/0.64 [61]~P26(x611)+P25(x611)
% 0.62/0.64 [62]~P7(x621)+P26(x621)
% 0.62/0.64 [63]~P15(x631)+~P3(x631)
% 0.62/0.64 [64]~P1(x641)+P16(x641,a9)
% 0.62/0.64 [65]~P10(x651)+P16(x651,a10)
% 0.62/0.64 [66]~P3(x661)+P16(x661,a5)
% 0.62/0.64 [67]~P15(x671)+P16(x671,a12)
% 0.62/0.64 [68]~P19(x681)+P16(x681,a14)
% 0.62/0.64 [69]~P28(x691)+P16(x691,a1)
% 0.62/0.64 [70]~P27(x701)+P16(x701,a22)
% 0.62/0.64 [71]~P29(x711)+P16(x711,a23)
% 0.62/0.64 [72]~P30(x721)+P16(x721,a24)
% 0.62/0.64 [73]~P31(x731)+P16(x731,a25)
% 0.62/0.64 [74]~P32(x741)+P16(x741,a26)
% 0.62/0.64 [75]~P33(x751)+P16(x751,a27)
% 0.62/0.64 [76]~P34(x761)+P16(x761,a28)
% 0.62/0.64 [77]~P35(x771)+P16(x771,a29)
% 0.62/0.64 [78]~P36(x781)+P16(x781,a30)
% 0.62/0.64 [79]~P22(x791)+P16(x791,a15)
% 0.62/0.64 [80]~P23(x801)+P16(x801,a16)
% 0.62/0.64 [81]~P24(x811)+P16(x811,a17)
% 0.62/0.64 [82]~P25(x821)+P16(x821,a18)
% 0.62/0.64 [83]~P26(x831)+P16(x831,a19)
% 0.62/0.64 [84]~P7(x841)+P16(x841,a20)
% 0.62/0.64 [85]~P6(x851)+P16(x851,a32)
% 0.62/0.64 [87]~P14(x871)+P9(x871,x871)
% 0.62/0.64 [89]~P3(x891)+P12(x891,x891)
% 0.62/0.64 [91]~P20(x911)+P13(x911,x911)
% 0.62/0.64 [92]P1(x921)+~P16(x921,a9)
% 0.62/0.64 [93]P10(x931)+~P16(x931,a10)
% 0.62/0.64 [94]P6(x941)+~P16(x941,a32)
% 0.62/0.64 [95]P3(x951)+~P16(x951,a5)
% 0.62/0.64 [96]P15(x961)+~P16(x961,a12)
% 0.62/0.64 [97]P19(x971)+~P16(x971,a14)
% 0.62/0.64 [98]P27(x981)+~P16(x981,a22)
% 0.62/0.64 [99]P29(x991)+~P16(x991,a23)
% 0.62/0.64 [100]P30(x1001)+~P16(x1001,a24)
% 0.62/0.64 [101]P31(x1011)+~P16(x1011,a25)
% 0.62/0.64 [102]P32(x1021)+~P16(x1021,a26)
% 0.62/0.64 [103]P33(x1031)+~P16(x1031,a27)
% 0.62/0.64 [104]P34(x1041)+~P16(x1041,a28)
% 0.62/0.64 [105]P35(x1051)+~P16(x1051,a29)
% 0.62/0.64 [106]P36(x1061)+~P16(x1061,a30)
% 0.62/0.64 [107]P22(x1071)+~P16(x1071,a15)
% 0.62/0.64 [108]P23(x1081)+~P16(x1081,a16)
% 0.62/0.64 [109]P24(x1091)+~P16(x1091,a17)
% 0.62/0.64 [110]P25(x1101)+~P16(x1101,a18)
% 0.62/0.64 [111]P26(x1111)+~P16(x1111,a19)
% 0.62/0.64 [112]P7(x1121)+~P16(x1121,a20)
% 0.62/0.64 [113]P28(x1131)+~P16(x1131,a1)
% 0.62/0.64 [115]P3(x1151)+~P12(x1152,x1151)
% 0.62/0.64 [116]P3(x1161)+~P5(x1162,x1161)
% 0.62/0.64 [118]P3(x1181)+~P16(x1182,x1181)
% 0.62/0.64 [120]P3(x1201)+~P12(x1201,x1202)
% 0.62/0.64 [121]P3(x1211)+~P5(x1211,x1212)
% 0.62/0.64 [123]P20(x1231)+~P13(x1232,x1231)
% 0.62/0.64 [125]P20(x1251)+~P13(x1251,x1252)
% 0.62/0.64 [126]P4(x1261)+~P11(x1262,x1261)
% 0.62/0.64 [127]P4(x1271)+~P11(x1271,x1272)
% 0.62/0.64 [129]P21(x1291)+~P16(x1291,x1292)
% 0.62/0.64 [131]P14(x1311)+~P9(x1312,x1311)
% 0.62/0.64 [133]P14(x1331)+~P9(x1331,x1332)
% 0.62/0.64 [135]~P5(x1352,x1351)+P5(x1351,x1352)
% 0.62/0.64 [134]~P9(x1342,x1341)+P8(x1341)+~P8(x1342)
% 0.62/0.64 [136]~P9(x1361,x1363)+P9(x1361,x1362)+~P9(x1363,x1362)
% 0.62/0.64 [139]~P12(x1391,x1393)+P12(x1391,x1392)+~P12(x1393,x1392)
% 0.62/0.64 [140]~P5(x1403,x1402)+P5(x1401,x1402)+~P12(x1401,x1403)
% 0.62/0.64 [141]~P5(x1411,x1413)+P5(x1411,x1412)+~P12(x1412,x1413)
% 0.62/0.64 [142]~P16(x1421,x1423)+P16(x1421,x1422)+~P12(x1423,x1422)
% 0.62/0.64 [143]~P13(x1431,x1433)+P11(x1431,x1432)+~P11(x1433,x1432)
% 0.62/0.64 [144]~P13(x1443,x1442)+P11(x1441,x1442)+~P11(x1441,x1443)
% 0.62/0.64 [145]~P11(x1451,x1453)+P13(x1451,x1452)+~P11(x1453,x1452)
% 0.62/0.64 [146]~P13(x1461,x1463)+P13(x1461,x1462)+~P13(x1463,x1462)
% 0.62/0.64 [147]~P16(x1473,x1471)+~P5(x1471,x1472)+~P16(x1473,x1472)
% 0.62/0.64 %EqnAxiom
% 0.62/0.64
% 0.62/0.64 %-------------------------------------------
% 0.62/0.64 cnf(150,plain,
% 0.62/0.64 (P12(a9,a5)),
% 0.62/0.64 inference(scs_inference,[],[10,42,16,17,136,139])).
% 0.62/0.64 cnf(154,plain,
% 0.62/0.64 (P5(a5,a14)),
% 0.62/0.64 inference(scs_inference,[],[10,42,16,17,18,34,136,139,140,141])).
% 0.62/0.64 cnf(158,plain,
% 0.62/0.64 (P16(a1,a10)),
% 0.62/0.64 inference(scs_inference,[],[10,42,16,17,18,34,1,136,139,140,141,142,64])).
% 0.62/0.64 cnf(163,plain,
% 0.62/0.64 (P16(a1,a5)),
% 0.62/0.64 inference(scs_inference,[],[158,17,93,147,142])).
% 0.62/0.64 cnf(165,plain,
% 0.62/0.64 (P9(a7,a3)),
% 0.62/0.64 inference(scs_inference,[],[11,13,158,17,93,147,142,136])).
% 0.62/0.64 cnf(167,plain,
% 0.62/0.64 (P5(a9,a14)),
% 0.62/0.64 inference(scs_inference,[],[11,13,158,150,154,17,93,147,142,136,140])).
% 0.62/0.64 cnf(169,plain,
% 0.62/0.64 (P5(a5,a22)),
% 0.62/0.64 inference(scs_inference,[],[11,13,158,19,150,154,17,93,147,142,136,140,141])).
% 0.62/0.64 cnf(171,plain,
% 0.62/0.64 (P12(a23,a14)),
% 0.62/0.64 inference(scs_inference,[],[11,13,158,19,20,150,154,17,93,147,142,136,140,141,139])).
% 0.62/0.64 cnf(199,plain,
% 0.62/0.64 (~P23(a1)),
% 0.62/0.64 inference(scs_inference,[],[11,13,158,19,20,150,154,17,93,147,142,136,140,141,139,95,63,47,48,49,50,51,52,53,54,55,56,57,58])).
% 0.62/0.64 cnf(215,plain,
% 0.62/0.64 (~P26(a1)),
% 0.62/0.64 inference(scs_inference,[],[12,163,165,21,22,167,169,171,150,199,59,60,147,140,136,141,139,61])).
% 0.62/0.64 cnf(225,plain,
% 0.62/0.64 ($false),
% 0.62/0.64 inference(scs_inference,[],[3,215,62]),
% 0.62/0.64 ['proof']).
% 0.62/0.64 % SZS output end Proof
% 0.62/0.64 % Total time :0.020000s
%------------------------------------------------------------------------------