%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CSR039+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 : n010.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:16 EDT 2024
% Result : Theorem 0.53s 0.87s
% Output : CNFRefutation 0.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : CSR039+1 : TPTP v8.2.0. Released v3.4.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n010.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.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Jun 19 20:56:54 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.51/0.57 start to proof:theBenchmark
% 0.53/0.84 %-------------------------------------------
% 0.53/0.84 % File :CSE---1.7
% 0.53/0.84 % Problem :theBenchmark
% 0.53/0.84 % Transform :cnf
% 0.53/0.84 % Format :tptp:raw
% 0.53/0.84 % Command :java -jar mcs_scs.jar %d %s
% 0.53/0.84
% 0.53/0.84 % Result :Theorem 0.220000s
% 0.53/0.84 % Output :CNFRefutation 0.220000s
% 0.53/0.84 %-------------------------------------------
% 0.53/0.85 %------------------------------------------------------------------------------
% 0.53/0.85 % File : CSR039+1 : TPTP v8.2.0. Released v3.4.0.
% 0.53/0.85 % Domain : Common Sense Reasoning
% 0.53/0.85 % Problem : Autogenerated Cyc Problem CSR039+1
% 0.53/0.85 % Version : Especial.
% 0.53/0.85 % English :
% 0.53/0.85
% 0.53/0.85 % Refs : [RS+] Reagan Smith et al., The Cyc TPTP Challenge Problem
% 0.53/0.85 % Source : [RS+]
% 0.53/0.85 % Names :
% 0.53/0.85
% 0.53/0.85 % Status : Theorem
% 0.53/0.85 % 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.50 v5.5.0, 0.08 v5.4.0, 0.13 v5.3.0, 0.22 v5.2.0, 0.07 v5.0.0, 0.20 v4.1.0, 0.22 v4.0.1, 0.21 v4.0.0, 0.20 v3.7.0, 0.00 v3.4.0
% 0.53/0.85 % Syntax : Number of formulae : 171 ( 45 unt; 0 def)
% 0.53/0.85 % Number of atoms : 310 ( 0 equ)
% 0.53/0.85 % Maximal formula atoms : 3 ( 1 avg)
% 0.53/0.85 % Number of connectives : 141 ( 2 ~; 0 |; 15 &)
% 0.53/0.85 % ( 0 <=>; 124 =>; 0 <=; 0 <~>)
% 0.53/0.85 % Maximal formula depth : 7 ( 3 avg)
% 0.53/0.85 % Maximal term depth : 4 ( 1 avg)
% 0.53/0.85 % Number of predicates : 45 ( 45 usr; 0 prp; 1-3 aty)
% 0.53/0.85 % Number of functors : 45 ( 45 usr; 42 con; 0-2 aty)
% 0.53/0.85 % Number of variables : 185 ( 185 !; 0 ?)
% 0.53/0.85 % SPC : FOF_THM_RFO_NEQ
% 0.53/0.85
% 0.53/0.85 % Comments : Autogenerated from the OpenCyc KB. Documentation can be found at
% 0.53/0.85 % http://opencyc.org/doc/#TPTP_Challenge_Problem_Set
% 0.53/0.85 % : Cyc(R) Knowledge Base Copyright(C) 1995-2007 Cycorp, Inc., Austin,
% 0.53/0.85 % TX, USA. All rights reserved.
% 0.53/0.85 % : OpenCyc Knowledge Base Copyright(C) 2001-2007 Cycorp, Inc.,
% 0.53/0.85 % Austin, TX, USA. All rights reserved.
% 0.53/0.85 %------------------------------------------------------------------------------
% 0.53/0.85 %$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.53/0.85 %$static(cyc_scaling_1,include('Axioms/CSR002+0.ax'))
% 0.53/0.85 %----Empty file include('Axioms/CSR002+0.ax').
% 0.53/0.85 %------------------------------------------------------------------------------
% 0.53/0.85 % Cyc Assertion #592971:
% 0.53/0.85 fof(just1,axiom,
% 0.53/0.85 genlmt(c_cycorpproductsmt,c_basekb) ).
% 0.53/0.85
% 0.53/0.85 % Cyc Assertion #600900:
% 0.53/0.85 fof(just2,axiom,
% 0.53/0.85 genlmt(c_cycnounlearnermt,c_cycorpproductsmt) ).
% 0.53/0.85
% 0.53/0.85 % Cyc Assertion #1322220:
% 0.53/0.85 fof(just3,axiom,
% 0.53/0.85 transitivebinarypredicate(c_genlmt) ).
% 0.53/0.85
% 0.53/0.85 % Cyc Assertion #1439735:
% 0.53/0.85 fof(just4,axiom,
% 0.53/0.85 genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7),c_machinelearningspindleheadmt) ).
% 0.53/0.85
% 0.53/0.85 % Cyc Assertion #1614635:
% 0.53/0.85 fof(just5,axiom,
% 0.53/0.85 genlmt(c_machinelearningspindleheadmt,c_cycnounlearnermt) ).
% 0.53/0.85
% 0.53/0.85 % Cyc Assertion #1650755:
% 0.53/0.85 fof(just6,axiom,
% 0.53/0.85 genlmt(c_basekb,c_universalvocabularymt) ).
% 0.53/0.85
% 0.53/0.85 % Cyc Assertion #1822756:
% 0.53/0.85 fof(just7,axiom,
% 0.53/0.85 genls(c_tptpcol_2_2,c_tptpcol_1_1) ).
% 0.53/0.85
% 0.53/0.85 fof(just8,axiom,
% 0.53/0.85 ! [OBJ] :
% 0.53/0.85 ( tptpcol_2_2(OBJ)
% 0.53/0.85 => tptpcol_1_1(OBJ) ) ).
% 0.53/0.85
% 0.53/0.85 % Cyc Assertion #1863715:
% 0.53/0.85 fof(just9,axiom,
% 0.53/0.85 genls(c_tptpcol_3_16386,c_tptpcol_2_2) ).
% 0.53/0.85
% 0.53/0.85 fof(just10,axiom,
% 0.53/0.85 ! [OBJ] :
% 0.53/0.85 ( tptpcol_3_16386(OBJ)
% 0.53/0.85 => tptpcol_2_2(OBJ) ) ).
% 0.53/0.85
% 0.53/0.85 % Cyc Assertion #1863717:
% 0.53/0.85 fof(just11,axiom,
% 0.53/0.85 genls(c_tptpcol_4_16387,c_tptpcol_3_16386) ).
% 0.53/0.85
% 0.53/0.85 fof(just12,axiom,
% 0.53/0.85 ! [OBJ] :
% 0.53/0.85 ( tptpcol_4_16387(OBJ)
% 0.53/0.85 => tptpcol_3_16386(OBJ) ) ).
% 0.53/0.85
% 0.53/0.85 % Cyc Assertion #1863719:
% 0.53/0.85 fof(just13,axiom,
% 0.53/0.85 genls(c_tptpcol_5_16388,c_tptpcol_4_16387) ).
% 0.53/0.85
% 0.53/0.85 fof(just14,axiom,
% 0.53/0.85 ! [OBJ] :
% 0.53/0.85 ( tptpcol_5_16388(OBJ)
% 0.53/0.85 => tptpcol_4_16387(OBJ) ) ).
% 0.53/0.85
% 0.53/0.85 % Cyc Assertion #1868838:
% 0.53/0.85 fof(just15,axiom,
% 0.53/0.85 genls(c_tptpcol_6_18436,c_tptpcol_5_16388) ).
% 0.53/0.85
% 0.53/0.85 fof(just16,axiom,
% 0.53/0.85 ! [OBJ] :
% 0.53/0.85 ( tptpcol_6_18436(OBJ)
% 0.53/0.85 => tptpcol_5_16388(OBJ) ) ).
% 0.53/0.85
% 0.53/0.85 % Cyc Assertion #1868840:
% 0.53/0.85 fof(just17,axiom,
% 0.53/0.85 genls(c_tptpcol_7_18437,c_tptpcol_6_18436) ).
% 0.53/0.85
% 0.53/0.85 fof(just18,axiom,
% 0.53/0.85 ! [OBJ] :
% 0.53/0.85 ( tptpcol_7_18437(OBJ)
% 0.53/0.85 => tptpcol_6_18436(OBJ) ) ).
% 0.53/0.85
% 0.53/0.85 % Cyc Assertion #1868842:
% 0.53/0.85 fof(just19,axiom,
% 0.53/0.85 genls(c_tptpcol_8_18438,c_tptpcol_7_18437) ).
% 0.53/0.85
% 0.53/0.85 fof(just20,axiom,
% 0.53/0.85 ! [OBJ] :
% 0.53/0.85 ( tptpcol_8_18438(OBJ)
% 0.53/0.85 => tptpcol_7_18437(OBJ) ) ).
% 0.53/0.85
% 0.53/0.85 % Cyc Assertion #1868844:
% 0.53/0.85 fof(just21,axiom,
% 0.53/0.85 genls(c_tptpcol_9_18439,c_tptpcol_8_18438) ).
% 0.53/0.85
% 0.53/0.85 fof(just22,axiom,
% 0.53/0.85 ! [OBJ] :
% 0.53/0.85 ( tptpcol_9_18439(OBJ)
% 0.53/0.85 => tptpcol_8_18438(OBJ) ) ).
% 0.53/0.85
% 0.53/0.85 % Cyc Assertion #1869163:
% 0.53/0.85 fof(just23,axiom,
% 0.53/0.85 genls(c_tptpcol_10_18567,c_tptpcol_9_18439) ).
% 0.53/0.85
% 0.53/0.85 fof(just24,axiom,
% 0.53/0.85 ! [OBJ] :
% 0.53/0.85 ( tptpcol_10_18567(OBJ)
% 0.53/0.85 => tptpcol_9_18439(OBJ) ) ).
% 0.53/0.85
% 0.53/0.85 % Cyc Assertion #1869322:
% 0.53/0.85 fof(just25,axiom,
% 0.53/0.85 genls(c_tptpcol_11_18631,c_tptpcol_10_18567) ).
% 0.53/0.85
% 0.53/0.85 fof(just26,axiom,
% 0.53/0.85 ! [OBJ] :
% 0.53/0.85 ( tptpcol_11_18631(OBJ)
% 0.53/0.85 => tptpcol_10_18567(OBJ) ) ).
% 0.53/0.85
% 0.53/0.85 % Cyc Assertion #1869401:
% 0.53/0.85 fof(just27,axiom,
% 0.53/0.85 genls(c_tptpcol_12_18663,c_tptpcol_11_18631) ).
% 0.53/0.85
% 0.53/0.85 fof(just28,axiom,
% 0.53/0.85 ! [OBJ] :
% 0.53/0.85 ( tptpcol_12_18663(OBJ)
% 0.53/0.85 => tptpcol_11_18631(OBJ) ) ).
% 0.53/0.85
% 0.53/0.85 % Cyc Assertion #1869403:
% 0.53/0.85 fof(just29,axiom,
% 0.53/0.85 genls(c_tptpcol_13_18664,c_tptpcol_12_18663) ).
% 0.53/0.85
% 0.53/0.85 fof(just30,axiom,
% 0.53/0.85 ! [OBJ] :
% 0.53/0.85 ( tptpcol_13_18664(OBJ)
% 0.53/0.85 => tptpcol_12_18663(OBJ) ) ).
% 0.53/0.85
% 0.53/0.85 % Cyc Assertion #1986593:
% 0.53/0.85 fof(just31,axiom,
% 0.53/0.85 genls(c_tptpcol_2_65537,c_tptpcol_1_65536) ).
% 0.53/0.85
% 0.53/0.85 fof(just32,axiom,
% 0.53/0.85 ! [OBJ] :
% 0.53/0.85 ( tptpcol_2_65537(OBJ)
% 0.53/0.85 => tptpcol_1_65536(OBJ) ) ).
% 0.53/0.85
% 0.53/0.85 % Cyc Assertion #2027552:
% 0.53/0.85 fof(just33,axiom,
% 0.53/0.85 genls(c_tptpcol_3_81921,c_tptpcol_2_65537) ).
% 0.53/0.85
% 0.53/0.85 fof(just34,axiom,
% 0.53/0.86 ! [OBJ] :
% 0.53/0.86 ( tptpcol_3_81921(OBJ)
% 0.53/0.86 => tptpcol_2_65537(OBJ) ) ).
% 0.53/0.86
% 0.53/0.86 % Cyc Assertion #2048031:
% 0.53/0.86 fof(just35,axiom,
% 0.53/0.86 genls(c_tptpcol_4_90113,c_tptpcol_3_81921) ).
% 0.53/0.86
% 0.53/0.86 fof(just36,axiom,
% 0.53/0.86 ! [OBJ] :
% 0.53/0.86 ( tptpcol_4_90113(OBJ)
% 0.53/0.86 => tptpcol_3_81921(OBJ) ) ).
% 0.53/0.86
% 0.53/0.86 % Cyc Assertion #2048033:
% 0.53/0.86 fof(just37,axiom,
% 0.53/0.86 genls(c_tptpcol_5_90114,c_tptpcol_4_90113) ).
% 0.53/0.86
% 0.53/0.86 fof(just38,axiom,
% 0.53/0.86 ! [OBJ] :
% 0.53/0.86 ( tptpcol_5_90114(OBJ)
% 0.53/0.86 => tptpcol_4_90113(OBJ) ) ).
% 0.53/0.86
% 0.53/0.86 % Cyc Assertion #2053152:
% 0.53/0.86 fof(just39,axiom,
% 0.53/0.86 genls(c_tptpcol_6_92162,c_tptpcol_5_90114) ).
% 0.53/0.86
% 0.53/0.86 fof(just40,axiom,
% 0.53/0.86 ! [OBJ] :
% 0.53/0.86 ( tptpcol_6_92162(OBJ)
% 0.53/0.86 => tptpcol_5_90114(OBJ) ) ).
% 0.53/0.86
% 0.53/0.86 % Cyc Assertion #2055711:
% 0.53/0.86 fof(just41,axiom,
% 0.53/0.86 genls(c_tptpcol_7_93186,c_tptpcol_6_92162) ).
% 0.53/0.86
% 0.53/0.86 fof(just42,axiom,
% 0.53/0.86 ! [OBJ] :
% 0.53/0.86 ( tptpcol_7_93186(OBJ)
% 0.53/0.86 => tptpcol_6_92162(OBJ) ) ).
% 0.53/0.86
% 0.53/0.86 % Cyc Assertion #2056990:
% 0.53/0.86 fof(just43,axiom,
% 0.53/0.86 genls(c_tptpcol_8_93698,c_tptpcol_7_93186) ).
% 0.53/0.86
% 0.53/0.86 fof(just44,axiom,
% 0.53/0.86 ! [OBJ] :
% 0.53/0.86 ( tptpcol_8_93698(OBJ)
% 0.53/0.86 => tptpcol_7_93186(OBJ) ) ).
% 0.53/0.86
% 0.53/0.86 % Cyc Assertion #2056992:
% 0.53/0.86 fof(just45,axiom,
% 0.53/0.86 genls(c_tptpcol_9_93699,c_tptpcol_8_93698) ).
% 0.53/0.86
% 0.53/0.86 fof(just46,axiom,
% 0.53/0.86 ! [OBJ] :
% 0.53/0.86 ( tptpcol_9_93699(OBJ)
% 0.53/0.86 => tptpcol_8_93698(OBJ) ) ).
% 0.53/0.86
% 0.53/0.86 % Cyc Assertion #2056994:
% 0.53/0.86 fof(just47,axiom,
% 0.53/0.86 genls(c_tptpcol_10_93700,c_tptpcol_9_93699) ).
% 0.53/0.86
% 0.53/0.86 fof(just48,axiom,
% 0.53/0.86 ! [OBJ] :
% 0.53/0.86 ( tptpcol_10_93700(OBJ)
% 0.53/0.86 => tptpcol_9_93699(OBJ) ) ).
% 0.53/0.86
% 0.53/0.86 % Cyc Assertion #2057153:
% 0.53/0.86 fof(just49,axiom,
% 0.53/0.86 genls(c_tptpcol_11_93764,c_tptpcol_10_93700) ).
% 0.53/0.86
% 0.53/0.86 fof(just50,axiom,
% 0.53/0.86 ! [OBJ] :
% 0.53/0.86 ( tptpcol_11_93764(OBJ)
% 0.53/0.86 => tptpcol_10_93700(OBJ) ) ).
% 0.53/0.86
% 0.53/0.86 % Cyc Assertion #2057155:
% 0.53/0.86 fof(just51,axiom,
% 0.53/0.86 genls(c_tptpcol_12_93765,c_tptpcol_11_93764) ).
% 0.53/0.86
% 0.53/0.86 fof(just52,axiom,
% 0.53/0.86 ! [OBJ] :
% 0.53/0.86 ( tptpcol_12_93765(OBJ)
% 0.53/0.86 => tptpcol_11_93764(OBJ) ) ).
% 0.53/0.86
% 0.53/0.86 % Cyc Assertion #2057157:
% 0.53/0.86 fof(just53,axiom,
% 0.53/0.86 genls(c_tptpcol_13_93766,c_tptpcol_12_93765) ).
% 0.53/0.86
% 0.53/0.86 fof(just54,axiom,
% 0.53/0.86 ! [OBJ] :
% 0.53/0.86 ( tptpcol_13_93766(OBJ)
% 0.53/0.86 => tptpcol_12_93765(OBJ) ) ).
% 0.53/0.86
% 0.53/0.86 % Cyc Assertion #2057176:
% 0.53/0.86 fof(just55,axiom,
% 0.53/0.86 genls(c_tptpcol_14_93774,c_tptpcol_13_93766) ).
% 0.53/0.86
% 0.53/0.86 fof(just56,axiom,
% 0.53/0.86 ! [OBJ] :
% 0.53/0.86 ( tptpcol_14_93774(OBJ)
% 0.53/0.86 => tptpcol_13_93766(OBJ) ) ).
% 0.53/0.86
% 0.53/0.86 % Cyc Assertion #2057178:
% 0.53/0.86 fof(just57,axiom,
% 0.53/0.86 genls(c_tptpcol_15_93775,c_tptpcol_14_93774) ).
% 0.53/0.86
% 0.53/0.86 fof(just58,axiom,
% 0.53/0.86 ! [OBJ] :
% 0.53/0.86 ( tptpcol_15_93775(OBJ)
% 0.53/0.86 => tptpcol_14_93774(OBJ) ) ).
% 0.53/0.86
% 0.53/0.86 % Cyc Assertion #2150427:
% 0.53/0.86 fof(just59,axiom,
% 0.53/0.86 disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536) ).
% 0.53/0.86
% 0.53/0.86 fof(just60,axiom,
% 0.53/0.86 ! [OBJ] :
% 0.53/0.86 ~ ( tptpcol_1_1(OBJ)
% 0.53/0.86 & tptpcol_1_65536(OBJ) ) ).
% 0.53/0.86
% 0.53/0.86 % Cyc Assertion #398814:
% 0.53/0.86 fof(just61,axiom,
% 0.53/0.86 ! [OBJ,COL1,COL2] :
% 0.53/0.86 ~ ( isa(OBJ,COL1)
% 0.53/0.86 & isa(OBJ,COL2)
% 0.53/0.86 & disjointwith(COL1,COL2) ) ).
% 0.53/0.86
% 0.53/0.86 % Cyc Assertion #831913:
% 0.53/0.86 fof(just62,axiom,
% 0.53/0.86 ! [SPECPRED,PRED,GENLPRED] :
% 0.53/0.86 ( ( genlinverse(SPECPRED,PRED)
% 0.53/0.86 & genlinverse(PRED,GENLPRED) )
% 0.53/0.86 => genlpreds(SPECPRED,GENLPRED) ) ).
% 0.53/0.86
% 0.53/0.86 % Cyc Constant #40273:
% 0.53/0.86 fof(just63,axiom,
% 0.53/0.86 ! [ARG1,INS] :
% 0.53/0.86 ( genlpreds(ARG1,INS)
% 0.53/0.86 => predicate(INS) ) ).
% 0.53/0.86
% 0.53/0.86 fof(just64,axiom,
% 0.53/0.86 ! [ARG1,INS] :
% 0.53/0.86 ( genlpreds(ARG1,INS)
% 0.53/0.86 => predicate(INS) ) ).
% 0.53/0.86
% 0.53/0.86 fof(just65,axiom,
% 0.53/0.86 ! [INS,ARG2] :
% 0.53/0.86 ( genlpreds(INS,ARG2)
% 0.53/0.86 => predicate(INS) ) ).
% 0.53/0.86
% 0.53/0.86 fof(just66,axiom,
% 0.53/0.86 ! [INS,ARG2] :
% 0.53/0.86 ( genlpreds(INS,ARG2)
% 0.53/0.86 => predicate(INS) ) ).
% 0.53/0.86
% 0.53/0.86 fof(just67,axiom,
% 0.53/0.86 ! [X,Y,Z] :
% 0.53/0.86 ( ( genlpreds(X,Y)
% 0.53/0.86 & genlpreds(Y,Z) )
% 0.53/0.86 => genlpreds(X,Z) ) ).
% 0.53/0.86
% 0.53/0.86 fof(just68,axiom,
% 0.53/0.86 ! [X] :
% 0.53/0.86 ( predicate(X)
% 0.53/0.86 => genlpreds(X,X) ) ).
% 0.53/0.86
% 0.53/0.86 fof(just69,axiom,
% 0.53/0.86 ! [X] :
% 0.53/0.86 ( predicate(X)
% 0.53/0.86 => genlpreds(X,X) ) ).
% 0.53/0.86
% 0.53/0.86 % Cyc Constant #45259:
% 0.53/0.86 fof(just70,axiom,
% 0.53/0.86 ! [ARG1,INS] :
% 0.53/0.86 ( genlinverse(ARG1,INS)
% 0.53/0.86 => binarypredicate(INS) ) ).
% 0.53/0.86
% 0.53/0.86 fof(just71,axiom,
% 0.53/0.86 ! [INS,ARG2] :
% 0.53/0.86 ( genlinverse(INS,ARG2)
% 0.53/0.86 => binarypredicate(INS) ) ).
% 0.53/0.86
% 0.53/0.86 fof(just72,axiom,
% 0.53/0.86 ! [OLD,ARG2,NEW] :
% 0.53/0.86 ( ( genlinverse(OLD,ARG2)
% 0.53/0.86 & genlpreds(NEW,OLD) )
% 0.53/0.86 => genlinverse(NEW,ARG2) ) ).
% 0.53/0.86
% 0.53/0.86 fof(just73,axiom,
% 0.53/0.86 ! [ARG1,OLD,NEW] :
% 0.53/0.86 ( ( genlinverse(ARG1,OLD)
% 0.53/0.86 & genlpreds(OLD,NEW) )
% 0.53/0.86 => genlinverse(ARG1,NEW) ) ).
% 0.53/0.86
% 0.53/0.86 % Cyc Constant #78648:
% 0.53/0.86 fof(just74,axiom,
% 0.53/0.86 ! [ARG1,INS] :
% 0.53/0.86 ( disjointwith(ARG1,INS)
% 0.53/0.86 => collection(INS) ) ).
% 0.53/0.86
% 0.53/0.86 fof(just75,axiom,
% 0.53/0.86 ! [INS,ARG2] :
% 0.53/0.86 ( disjointwith(INS,ARG2)
% 0.53/0.86 => collection(INS) ) ).
% 0.53/0.86
% 0.53/0.86 fof(just76,axiom,
% 0.53/0.86 ! [X,Y] :
% 0.53/0.86 ( disjointwith(X,Y)
% 0.53/0.86 => disjointwith(Y,X) ) ).
% 0.53/0.86
% 0.53/0.86 fof(just77,axiom,
% 0.53/0.86 ! [ARG1,OLD,NEW] :
% 0.53/0.86 ( ( disjointwith(ARG1,OLD)
% 0.53/0.86 & genls(NEW,OLD) )
% 0.53/0.86 => disjointwith(ARG1,NEW) ) ).
% 0.53/0.86
% 0.53/0.86 fof(just78,axiom,
% 0.53/0.86 ! [OLD,ARG2,NEW] :
% 0.53/0.86 ( ( disjointwith(OLD,ARG2)
% 0.53/0.86 & genls(NEW,OLD) )
% 0.53/0.86 => disjointwith(NEW,ARG2) ) ).
% 0.53/0.86
% 0.53/0.86 % Cyc Constant #223372:
% 0.53/0.86 fof(just79,axiom,
% 0.53/0.86 ! [X] :
% 0.53/0.86 ( isa(X,c_tptpcol_15_93775)
% 0.53/0.86 => tptpcol_15_93775(X) ) ).
% 0.53/0.86
% 0.53/0.86 fof(just80,axiom,
% 0.53/0.86 ! [X] :
% 0.53/0.86 ( tptpcol_15_93775(X)
% 0.53/0.86 => isa(X,c_tptpcol_15_93775) ) ).
% 0.53/0.86
% 0.53/0.86 % Cyc Constant #223371:
% 0.53/0.86 fof(just81,axiom,
% 0.53/0.86 ! [X] :
% 0.53/0.86 ( isa(X,c_tptpcol_14_93774)
% 0.53/0.86 => tptpcol_14_93774(X) ) ).
% 0.53/0.86
% 0.53/0.86 fof(just82,axiom,
% 0.53/0.86 ! [X] :
% 0.53/0.86 ( tptpcol_14_93774(X)
% 0.53/0.86 => isa(X,c_tptpcol_14_93774) ) ).
% 0.53/0.86
% 0.53/0.86 % Cyc Constant #223363:
% 0.53/0.86 fof(just83,axiom,
% 0.53/0.86 ! [X] :
% 0.53/0.86 ( isa(X,c_tptpcol_13_93766)
% 0.53/0.86 => tptpcol_13_93766(X) ) ).
% 0.53/0.86
% 0.53/0.86 fof(just84,axiom,
% 0.53/0.86 ! [X] :
% 0.53/0.86 ( tptpcol_13_93766(X)
% 0.53/0.86 => isa(X,c_tptpcol_13_93766) ) ).
% 0.53/0.86
% 0.53/0.86 % Cyc Constant #223362:
% 0.53/0.86 fof(just85,axiom,
% 0.53/0.86 ! [X] :
% 0.53/0.86 ( isa(X,c_tptpcol_12_93765)
% 0.53/0.86 => tptpcol_12_93765(X) ) ).
% 0.53/0.86
% 0.53/0.86 fof(just86,axiom,
% 0.53/0.86 ! [X] :
% 0.53/0.86 ( tptpcol_12_93765(X)
% 0.53/0.86 => isa(X,c_tptpcol_12_93765) ) ).
% 0.53/0.86
% 0.53/0.86 % Cyc Constant #223361:
% 0.53/0.86 fof(just87,axiom,
% 0.53/0.86 ! [X] :
% 0.53/0.86 ( isa(X,c_tptpcol_11_93764)
% 0.53/0.86 => tptpcol_11_93764(X) ) ).
% 0.53/0.86
% 0.53/0.86 fof(just88,axiom,
% 0.53/0.86 ! [X] :
% 0.53/0.86 ( tptpcol_11_93764(X)
% 0.53/0.86 => isa(X,c_tptpcol_11_93764) ) ).
% 0.53/0.86
% 0.53/0.86 % Cyc Constant #223297:
% 0.53/0.86 fof(just89,axiom,
% 0.53/0.86 ! [X] :
% 0.53/0.86 ( isa(X,c_tptpcol_10_93700)
% 0.53/0.86 => tptpcol_10_93700(X) ) ).
% 0.53/0.86
% 0.53/0.86 fof(just90,axiom,
% 0.53/0.86 ! [X] :
% 0.53/0.86 ( tptpcol_10_93700(X)
% 0.53/0.86 => isa(X,c_tptpcol_10_93700) ) ).
% 0.53/0.86
% 0.53/0.86 % Cyc Constant #223296:
% 0.53/0.86 fof(just91,axiom,
% 0.53/0.86 ! [X] :
% 0.53/0.86 ( isa(X,c_tptpcol_9_93699)
% 0.53/0.87 => tptpcol_9_93699(X) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just92,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( tptpcol_9_93699(X)
% 0.53/0.87 => isa(X,c_tptpcol_9_93699) ) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #223295:
% 0.53/0.87 fof(just93,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( isa(X,c_tptpcol_8_93698)
% 0.53/0.87 => tptpcol_8_93698(X) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just94,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( tptpcol_8_93698(X)
% 0.53/0.87 => isa(X,c_tptpcol_8_93698) ) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #222783:
% 0.53/0.87 fof(just95,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( isa(X,c_tptpcol_7_93186)
% 0.53/0.87 => tptpcol_7_93186(X) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just96,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( tptpcol_7_93186(X)
% 0.53/0.87 => isa(X,c_tptpcol_7_93186) ) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #221759:
% 0.53/0.87 fof(just97,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( isa(X,c_tptpcol_6_92162)
% 0.53/0.87 => tptpcol_6_92162(X) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just98,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( tptpcol_6_92162(X)
% 0.53/0.87 => isa(X,c_tptpcol_6_92162) ) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #219711:
% 0.53/0.87 fof(just99,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( isa(X,c_tptpcol_5_90114)
% 0.53/0.87 => tptpcol_5_90114(X) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just100,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( tptpcol_5_90114(X)
% 0.53/0.87 => isa(X,c_tptpcol_5_90114) ) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #219710:
% 0.53/0.87 fof(just101,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( isa(X,c_tptpcol_4_90113)
% 0.53/0.87 => tptpcol_4_90113(X) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just102,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( tptpcol_4_90113(X)
% 0.53/0.87 => isa(X,c_tptpcol_4_90113) ) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #211518:
% 0.53/0.87 fof(just103,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( isa(X,c_tptpcol_3_81921)
% 0.53/0.87 => tptpcol_3_81921(X) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just104,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( tptpcol_3_81921(X)
% 0.53/0.87 => isa(X,c_tptpcol_3_81921) ) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #195133:
% 0.53/0.87 fof(just105,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( isa(X,c_tptpcol_1_65536)
% 0.53/0.87 => tptpcol_1_65536(X) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just106,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( tptpcol_1_65536(X)
% 0.53/0.87 => isa(X,c_tptpcol_1_65536) ) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #195134:
% 0.53/0.87 fof(just107,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( isa(X,c_tptpcol_2_65537)
% 0.53/0.87 => tptpcol_2_65537(X) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just108,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( tptpcol_2_65537(X)
% 0.53/0.87 => isa(X,c_tptpcol_2_65537) ) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #148261:
% 0.53/0.87 fof(just109,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( isa(X,c_tptpcol_13_18664)
% 0.53/0.87 => tptpcol_13_18664(X) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just110,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( tptpcol_13_18664(X)
% 0.53/0.87 => isa(X,c_tptpcol_13_18664) ) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #148260:
% 0.53/0.87 fof(just111,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( isa(X,c_tptpcol_12_18663)
% 0.53/0.87 => tptpcol_12_18663(X) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just112,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( tptpcol_12_18663(X)
% 0.53/0.87 => isa(X,c_tptpcol_12_18663) ) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #148228:
% 0.53/0.87 fof(just113,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( isa(X,c_tptpcol_11_18631)
% 0.53/0.87 => tptpcol_11_18631(X) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just114,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( tptpcol_11_18631(X)
% 0.53/0.87 => isa(X,c_tptpcol_11_18631) ) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #148164:
% 0.53/0.87 fof(just115,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( isa(X,c_tptpcol_10_18567)
% 0.53/0.87 => tptpcol_10_18567(X) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just116,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( tptpcol_10_18567(X)
% 0.53/0.87 => isa(X,c_tptpcol_10_18567) ) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #148036:
% 0.53/0.87 fof(just117,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( isa(X,c_tptpcol_9_18439)
% 0.53/0.87 => tptpcol_9_18439(X) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just118,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( tptpcol_9_18439(X)
% 0.53/0.87 => isa(X,c_tptpcol_9_18439) ) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #148035:
% 0.53/0.87 fof(just119,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( isa(X,c_tptpcol_8_18438)
% 0.53/0.87 => tptpcol_8_18438(X) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just120,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( tptpcol_8_18438(X)
% 0.53/0.87 => isa(X,c_tptpcol_8_18438) ) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #148034:
% 0.53/0.87 fof(just121,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( isa(X,c_tptpcol_7_18437)
% 0.53/0.87 => tptpcol_7_18437(X) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just122,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( tptpcol_7_18437(X)
% 0.53/0.87 => isa(X,c_tptpcol_7_18437) ) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #148033:
% 0.53/0.87 fof(just123,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( isa(X,c_tptpcol_6_18436)
% 0.53/0.87 => tptpcol_6_18436(X) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just124,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( tptpcol_6_18436(X)
% 0.53/0.87 => isa(X,c_tptpcol_6_18436) ) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #145985:
% 0.53/0.87 fof(just125,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( isa(X,c_tptpcol_5_16388)
% 0.53/0.87 => tptpcol_5_16388(X) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just126,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( tptpcol_5_16388(X)
% 0.53/0.87 => isa(X,c_tptpcol_5_16388) ) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #145984:
% 0.53/0.87 fof(just127,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( isa(X,c_tptpcol_4_16387)
% 0.53/0.87 => tptpcol_4_16387(X) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just128,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( tptpcol_4_16387(X)
% 0.53/0.87 => isa(X,c_tptpcol_4_16387) ) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #145983:
% 0.53/0.87 fof(just129,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( isa(X,c_tptpcol_3_16386)
% 0.53/0.87 => tptpcol_3_16386(X) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just130,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( tptpcol_3_16386(X)
% 0.53/0.87 => isa(X,c_tptpcol_3_16386) ) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #129598:
% 0.53/0.87 fof(just131,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( isa(X,c_tptpcol_1_1)
% 0.53/0.87 => tptpcol_1_1(X) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just132,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( tptpcol_1_1(X)
% 0.53/0.87 => isa(X,c_tptpcol_1_1) ) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #129599:
% 0.53/0.87 fof(just133,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( isa(X,c_tptpcol_2_2)
% 0.53/0.87 => tptpcol_2_2(X) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just134,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( tptpcol_2_2(X)
% 0.53/0.87 => isa(X,c_tptpcol_2_2) ) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #0:
% 0.53/0.87 fof(just135,axiom,
% 0.53/0.87 ! [ARG1,INS] :
% 0.53/0.87 ( genls(ARG1,INS)
% 0.53/0.87 => collection(INS) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just136,axiom,
% 0.53/0.87 ! [ARG1,INS] :
% 0.53/0.87 ( genls(ARG1,INS)
% 0.53/0.87 => collection(INS) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just137,axiom,
% 0.53/0.87 ! [INS,ARG2] :
% 0.53/0.87 ( genls(INS,ARG2)
% 0.53/0.87 => collection(INS) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just138,axiom,
% 0.53/0.87 ! [INS,ARG2] :
% 0.53/0.87 ( genls(INS,ARG2)
% 0.53/0.87 => collection(INS) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just139,axiom,
% 0.53/0.87 ! [X,Y,Z] :
% 0.53/0.87 ( ( genls(X,Y)
% 0.53/0.87 & genls(Y,Z) )
% 0.53/0.87 => genls(X,Z) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just140,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( collection(X)
% 0.53/0.87 => genls(X,X) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just141,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( collection(X)
% 0.53/0.87 => genls(X,X) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just142,axiom,
% 0.53/0.87 ! [OLD,ARG2,NEW] :
% 0.53/0.87 ( ( genls(OLD,ARG2)
% 0.53/0.87 & genls(NEW,OLD) )
% 0.53/0.87 => genls(NEW,ARG2) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just143,axiom,
% 0.53/0.87 ! [ARG1,OLD,NEW] :
% 0.53/0.87 ( ( genls(ARG1,OLD)
% 0.53/0.87 & genls(OLD,NEW) )
% 0.53/0.87 => genls(ARG1,NEW) ) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #129091:
% 0.53/0.87 fof(just144,axiom,
% 0.53/0.87 ! [ARG1] : natfunction(f_urlfn(ARG1),c_urlfn) ).
% 0.53/0.87
% 0.53/0.87 fof(just145,axiom,
% 0.53/0.87 ! [ARG1] : natargument(f_urlfn(ARG1),n_1,ARG1) ).
% 0.53/0.87
% 0.53/0.87 fof(just146,axiom,
% 0.53/0.87 ! [ARG1] : uniformresourcelocator(f_urlfn(ARG1)) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #78971:
% 0.53/0.87 fof(just147,axiom,
% 0.53/0.87 ! [ARG1] : natfunction(f_urlreferentfn(ARG1),c_urlreferentfn) ).
% 0.53/0.87
% 0.53/0.87 fof(just148,axiom,
% 0.53/0.87 ! [ARG1] : natargument(f_urlreferentfn(ARG1),n_1,ARG1) ).
% 0.53/0.87
% 0.53/0.87 fof(just149,axiom,
% 0.53/0.87 ! [ARG1] : computerdataartifact(f_urlreferentfn(ARG1)) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #71728:
% 0.53/0.87 fof(just150,axiom,
% 0.53/0.87 ! [ARG1,ARG2] : natfunction(f_contentmtofcdafromeventfn(ARG1,ARG2),c_contentmtofcdafromeventfn) ).
% 0.53/0.87
% 0.53/0.87 fof(just151,axiom,
% 0.53/0.87 ! [ARG1,ARG2] : natargument(f_contentmtofcdafromeventfn(ARG1,ARG2),n_1,ARG1) ).
% 0.53/0.87
% 0.53/0.87 fof(just152,axiom,
% 0.53/0.87 ! [ARG1,ARG2] : natargument(f_contentmtofcdafromeventfn(ARG1,ARG2),n_2,ARG2) ).
% 0.53/0.87
% 0.53/0.87 fof(just153,axiom,
% 0.53/0.87 ! [ARG1,ARG2] : microtheory(f_contentmtofcdafromeventfn(ARG1,ARG2)) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #127156:
% 0.53/0.87 fof(just154,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( isa(X,c_transitivebinarypredicate)
% 0.53/0.87 => transitivebinarypredicate(X) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just155,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( transitivebinarypredicate(X)
% 0.53/0.87 => isa(X,c_transitivebinarypredicate) ) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #72115:
% 0.53/0.87 fof(just156,axiom,
% 0.53/0.87 ! [ARG1,INS] :
% 0.53/0.87 ( isa(ARG1,INS)
% 0.53/0.87 => collection(INS) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just157,axiom,
% 0.53/0.87 ! [ARG1,INS] :
% 0.53/0.87 ( isa(ARG1,INS)
% 0.53/0.87 => collection(INS) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just158,axiom,
% 0.53/0.87 ! [INS,ARG2] :
% 0.53/0.87 ( isa(INS,ARG2)
% 0.53/0.87 => thing(INS) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just159,axiom,
% 0.53/0.87 ! [INS,ARG2] :
% 0.53/0.87 ( isa(INS,ARG2)
% 0.53/0.87 => thing(INS) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just160,axiom,
% 0.53/0.87 ! [ARG1,OLD,NEW] :
% 0.53/0.87 ( ( isa(ARG1,OLD)
% 0.53/0.87 & genls(OLD,NEW) )
% 0.53/0.87 => isa(ARG1,NEW) ) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #95028:
% 0.53/0.87 fof(just161,axiom,
% 0.53/0.87 mtvisible(c_universalvocabularymt) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #19550:
% 0.53/0.87 fof(just162,axiom,
% 0.53/0.87 ! [SPECMT,GENLMT] :
% 0.53/0.87 ( ( mtvisible(SPECMT)
% 0.53/0.87 & genlmt(SPECMT,GENLMT) )
% 0.53/0.87 => mtvisible(GENLMT) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just163,axiom,
% 0.53/0.87 ! [ARG1,INS] :
% 0.53/0.87 ( genlmt(ARG1,INS)
% 0.53/0.87 => microtheory(INS) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just164,axiom,
% 0.53/0.87 ! [ARG1,INS] :
% 0.53/0.87 ( genlmt(ARG1,INS)
% 0.53/0.87 => microtheory(INS) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just165,axiom,
% 0.53/0.87 ! [INS,ARG2] :
% 0.53/0.87 ( genlmt(INS,ARG2)
% 0.53/0.87 => microtheory(INS) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just166,axiom,
% 0.53/0.87 ! [INS,ARG2] :
% 0.53/0.87 ( genlmt(INS,ARG2)
% 0.53/0.87 => microtheory(INS) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just167,axiom,
% 0.53/0.87 ! [X,Y,Z] :
% 0.53/0.87 ( ( genlmt(X,Y)
% 0.53/0.87 & genlmt(Y,Z) )
% 0.53/0.87 => genlmt(X,Z) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just168,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( microtheory(X)
% 0.53/0.87 => genlmt(X,X) ) ).
% 0.53/0.87
% 0.53/0.87 fof(just169,axiom,
% 0.53/0.87 ! [X] :
% 0.53/0.87 ( microtheory(X)
% 0.53/0.87 => genlmt(X,X) ) ).
% 0.53/0.87
% 0.53/0.87 % Cyc Constant #27757:
% 0.53/0.87 fof(just170,axiom,
% 0.53/0.87 mtvisible(c_basekb) ).
% 0.53/0.87
% 0.53/0.87 fof(query39,conjecture,
% 0.53/0.87 ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7))
% 0.53/0.87 => disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664) ) ).
% 0.53/0.87
% 0.53/0.87 %------------------------------------------------------------------------------
% 0.53/0.87 %-------------------------------------------
% 0.53/0.87 % Proof found
% 0.53/0.87 % SZS status Theorem for theBenchmark
% 0.53/0.87 % SZS output start Proof
% 0.53/0.87 %ClaNum:172(EqnAxiom:0)
% 0.53/0.87 %VarNum:301(SingletonVarNum:160)
% 0.53/0.87 %MaxLitNum:3
% 0.53/0.87 %MaxfuncDepth:3
% 0.53/0.87 %SharedTerms:82
% 0.53/0.87 %goalClause: 41 47
% 0.53/0.87 %singleGoalClaCount:2
% 0.53/0.87 [1]P1(a1)
% 0.53/0.87 [2]P2(a2)
% 0.53/0.87 [3]P2(a6)
% 0.53/0.87 [6]P6(a3,a2)
% 0.53/0.87 [7]P6(a2,a6)
% 0.53/0.87 [8]P6(a4,a3)
% 0.53/0.87 [9]P6(a7,a4)
% 0.53/0.87 [10]P9(a8,a9)
% 0.53/0.87 [11]P9(a21,a8)
% 0.53/0.87 [12]P9(a23,a21)
% 0.53/0.87 [13]P9(a25,a23)
% 0.53/0.87 [14]P9(a27,a25)
% 0.53/0.87 [15]P9(a29,a27)
% 0.53/0.87 [16]P9(a31,a29)
% 0.53/0.87 [17]P9(a33,a31)
% 0.53/0.87 [18]P9(a10,a33)
% 0.53/0.87 [19]P9(a11,a10)
% 0.53/0.87 [20]P9(a13,a11)
% 0.53/0.87 [21]P9(a15,a13)
% 0.53/0.87 [22]P9(a22,a20)
% 0.53/0.87 [23]P9(a24,a22)
% 0.53/0.87 [24]P9(a26,a24)
% 0.53/0.87 [25]P9(a28,a26)
% 0.53/0.87 [26]P9(a30,a28)
% 0.53/0.87 [27]P9(a32,a30)
% 0.53/0.87 [28]P9(a34,a32)
% 0.53/0.87 [29]P9(a35,a34)
% 0.53/0.87 [30]P9(a12,a35)
% 0.53/0.87 [31]P9(a14,a12)
% 0.53/0.87 [32]P9(a16,a14)
% 0.53/0.87 [33]P9(a17,a16)
% 0.53/0.87 [34]P9(a18,a17)
% 0.53/0.87 [35]P9(a19,a18)
% 0.53/0.87 [36]P7(a9,a20)
% 0.53/0.87 [47]~P7(a19,a15)
% 0.53/0.87 [41]P2(f41(f42(f38(a43)),a36))
% 0.53/0.87 [44]P6(f41(f42(f38(a43)),a36),a7)
% 0.53/0.87 [4]P45(f38(x41))
% 0.53/0.87 [5]P3(f42(x51))
% 0.53/0.87 [37]P13(f38(x371),a39)
% 0.53/0.87 [38]P13(f42(x381),a40)
% 0.53/0.87 [42]P14(f38(x421),a44,x421)
% 0.53/0.87 [43]P14(f42(x431),a44,x431)
% 0.53/0.87 [39]P11(f41(x391,x392))
% 0.53/0.87 [40]P13(f41(x401,x402),a5)
% 0.53/0.87 [45]P14(f41(x451,x452),a44,x451)
% 0.53/0.87 [46]P14(f41(x461,x462),a45,x462)
% 0.53/0.87 [48]~P30(x481)+P15(x481)
% 0.53/0.87 [49]~P15(x491)+P16(x491)
% 0.53/0.87 [50]~P32(x501)+P30(x501)
% 0.53/0.87 [51]~P34(x511)+P32(x511)
% 0.53/0.87 [52]~P36(x521)+P34(x521)
% 0.53/0.87 [53]~P38(x531)+P36(x531)
% 0.53/0.87 [54]~P40(x541)+P38(x541)
% 0.53/0.87 [55]~P42(x551)+P40(x551)
% 0.53/0.87 [56]~P17(x561)+P42(x561)
% 0.53/0.87 [57]~P20(x571)+P17(x571)
% 0.53/0.87 [58]~P22(x581)+P20(x581)
% 0.53/0.87 [59]~P24(x591)+P22(x591)
% 0.53/0.87 [60]~P33(x601)+P31(x601)
% 0.53/0.87 [61]~P31(x611)+P29(x611)
% 0.53/0.87 [62]~P35(x621)+P33(x621)
% 0.53/0.87 [63]~P37(x631)+P35(x631)
% 0.53/0.87 [64]~P39(x641)+P37(x641)
% 0.53/0.87 [65]~P41(x651)+P39(x651)
% 0.53/0.87 [66]~P43(x661)+P41(x661)
% 0.53/0.87 [67]~P44(x671)+P43(x671)
% 0.53/0.87 [68]~P21(x681)+P44(x681)
% 0.53/0.87 [69]~P23(x691)+P21(x691)
% 0.53/0.87 [70]~P25(x701)+P23(x701)
% 0.53/0.87 [71]~P26(x711)+P25(x711)
% 0.53/0.87 [72]~P27(x721)+P26(x721)
% 0.53/0.87 [73]~P28(x731)+P27(x731)
% 0.53/0.87 [74]~P29(x741)+~P16(x741)
% 0.53/0.87 [75]~P15(x751)+P12(x751,a8)
% 0.53/0.87 [76]~P16(x761)+P12(x761,a9)
% 0.53/0.87 [77]~P30(x771)+P12(x771,a21)
% 0.53/0.87 [78]~P32(x781)+P12(x781,a23)
% 0.53/0.87 [79]~P34(x791)+P12(x791,a25)
% 0.53/0.87 [80]~P36(x801)+P12(x801,a27)
% 0.53/0.87 [81]~P38(x811)+P12(x811,a29)
% 0.53/0.87 [82]~P40(x821)+P12(x821,a31)
% 0.53/0.87 [83]~P42(x831)+P12(x831,a33)
% 0.53/0.87 [84]~P17(x841)+P12(x841,a10)
% 0.53/0.87 [85]~P20(x851)+P12(x851,a11)
% 0.53/0.87 [86]~P22(x861)+P12(x861,a13)
% 0.53/0.87 [87]~P24(x871)+P12(x871,a15)
% 0.53/0.87 [88]~P31(x881)+P12(x881,a22)
% 0.53/0.87 [89]~P29(x891)+P12(x891,a20)
% 0.53/0.87 [90]~P33(x901)+P12(x901,a24)
% 0.53/0.87 [91]~P35(x911)+P12(x911,a26)
% 0.53/0.87 [92]~P37(x921)+P12(x921,a28)
% 0.53/0.87 [93]~P39(x931)+P12(x931,a30)
% 0.53/0.87 [94]~P41(x941)+P12(x941,a32)
% 0.53/0.87 [95]~P43(x951)+P12(x951,a34)
% 0.53/0.87 [96]~P44(x961)+P12(x961,a35)
% 0.53/0.87 [97]~P21(x971)+P12(x971,a12)
% 0.53/0.87 [98]~P23(x981)+P12(x981,a14)
% 0.53/0.87 [99]~P25(x991)+P12(x991,a16)
% 0.53/0.87 [100]~P26(x1001)+P12(x1001,a17)
% 0.53/0.87 [101]~P27(x1011)+P12(x1011,a18)
% 0.53/0.87 [102]~P28(x1021)+P12(x1021,a19)
% 0.53/0.87 [103]~P1(x1031)+P12(x1031,a37)
% 0.53/0.87 [105]~P11(x1051)+P6(x1051,x1051)
% 0.53/0.87 [107]~P4(x1071)+P9(x1071,x1071)
% 0.53/0.87 [109]~P18(x1091)+P10(x1091,x1091)
% 0.53/0.87 [110]P1(x1101)+~P12(x1101,a37)
% 0.53/0.87 [111]P15(x1111)+~P12(x1111,a8)
% 0.53/0.87 [112]P16(x1121)+~P12(x1121,a9)
% 0.53/0.87 [113]P30(x1131)+~P12(x1131,a21)
% 0.53/0.87 [114]P32(x1141)+~P12(x1141,a23)
% 0.53/0.87 [115]P34(x1151)+~P12(x1151,a25)
% 0.53/0.87 [116]P36(x1161)+~P12(x1161,a27)
% 0.53/0.87 [117]P38(x1171)+~P12(x1171,a29)
% 0.53/0.87 [118]P40(x1181)+~P12(x1181,a31)
% 0.53/0.87 [119]P42(x1191)+~P12(x1191,a33)
% 0.53/0.87 [120]P17(x1201)+~P12(x1201,a10)
% 0.53/0.87 [121]P20(x1211)+~P12(x1211,a11)
% 0.53/0.87 [122]P22(x1221)+~P12(x1221,a13)
% 0.53/0.87 [123]P24(x1231)+~P12(x1231,a15)
% 0.53/0.87 [124]P31(x1241)+~P12(x1241,a22)
% 0.53/0.87 [125]P29(x1251)+~P12(x1251,a20)
% 0.53/0.87 [126]P33(x1261)+~P12(x1261,a24)
% 0.53/0.87 [127]P35(x1271)+~P12(x1271,a26)
% 0.53/0.87 [128]P37(x1281)+~P12(x1281,a28)
% 0.53/0.87 [129]P39(x1291)+~P12(x1291,a30)
% 0.53/0.87 [130]P41(x1301)+~P12(x1301,a32)
% 0.53/0.87 [131]P43(x1311)+~P12(x1311,a34)
% 0.53/0.87 [132]P44(x1321)+~P12(x1321,a35)
% 0.53/0.87 [133]P21(x1331)+~P12(x1331,a12)
% 0.53/0.87 [134]P23(x1341)+~P12(x1341,a14)
% 0.53/0.87 [135]P25(x1351)+~P12(x1351,a16)
% 0.53/0.87 [136]P26(x1361)+~P12(x1361,a17)
% 0.53/0.87 [137]P27(x1371)+~P12(x1371,a18)
% 0.53/0.87 [138]P28(x1381)+~P12(x1381,a19)
% 0.53/0.87 [140]P18(x1401)+~P10(x1402,x1401)
% 0.53/0.87 [142]P18(x1421)+~P10(x1421,x1422)
% 0.53/0.87 [143]P5(x1431)+~P8(x1432,x1431)
% 0.53/0.87 [144]P5(x1441)+~P8(x1441,x1442)
% 0.53/0.87 [146]P4(x1461)+~P9(x1462,x1461)
% 0.53/0.87 [147]P4(x1471)+~P7(x1472,x1471)
% 0.53/0.87 [149]P4(x1491)+~P12(x1492,x1491)
% 0.53/0.87 [151]P4(x1511)+~P9(x1511,x1512)
% 0.53/0.87 [152]P4(x1521)+~P7(x1521,x1522)
% 0.53/0.87 [154]P11(x1541)+~P6(x1542,x1541)
% 0.53/0.87 [156]P11(x1561)+~P6(x1561,x1562)
% 0.53/0.87 [158]P19(x1581)+~P12(x1581,x1582)
% 0.53/0.87 [160]~P7(x1602,x1601)+P7(x1601,x1602)
% 0.53/0.87 [159]~P6(x1592,x1591)+P2(x1591)+~P2(x1592)
% 0.53/0.87 [161]~P6(x1611,x1613)+P6(x1611,x1612)+~P6(x1613,x1612)
% 0.53/0.87 [164]~P9(x1641,x1643)+P9(x1641,x1642)+~P9(x1643,x1642)
% 0.53/0.87 [165]~P7(x1653,x1652)+P7(x1651,x1652)+~P9(x1651,x1653)
% 0.53/0.87 [166]~P7(x1661,x1663)+P7(x1661,x1662)+~P9(x1662,x1663)
% 0.53/0.87 [167]~P12(x1671,x1673)+P12(x1671,x1672)+~P9(x1673,x1672)
% 0.53/0.87 [168]~P10(x1681,x1683)+P8(x1681,x1682)+~P8(x1683,x1682)
% 0.53/0.87 [169]~P10(x1693,x1692)+P8(x1691,x1692)+~P8(x1691,x1693)
% 0.53/0.87 [170]~P8(x1701,x1703)+P10(x1701,x1702)+~P8(x1703,x1702)
% 0.53/0.87 [171]~P10(x1711,x1713)+P10(x1711,x1712)+~P10(x1713,x1712)
% 0.53/0.87 [172]~P12(x1723,x1721)+~P7(x1721,x1722)+~P12(x1723,x1722)
% 0.53/0.87 %EqnAxiom
% 0.53/0.87
% 0.53/0.87 %-------------------------------------------
% 0.53/0.87 cnf(175,plain,
% 0.53/0.87 (P7(a8,a20)),
% 0.53/0.87 inference(scs_inference,[],[47,10,36,160,165])).
% 0.53/0.88 cnf(177,plain,
% 0.53/0.88 (~P7(a19,a13)),
% 0.53/0.88 inference(scs_inference,[],[47,10,21,36,160,165,166])).
% 0.53/0.88 cnf(179,plain,
% 0.53/0.88 (P6(a4,a2)),
% 0.53/0.88 inference(scs_inference,[],[47,6,8,10,21,36,160,165,166,161])).
% 0.53/0.88 cnf(181,plain,
% 0.53/0.88 (P9(a21,a9)),
% 0.53/0.88 inference(scs_inference,[],[47,6,8,10,11,21,36,160,165,166,161,164])).
% 0.53/0.88 cnf(189,plain,
% 0.53/0.88 (P6(a3,a6)),
% 0.53/0.88 inference(scs_inference,[],[177,6,7,160,161])).
% 0.53/0.88 cnf(191,plain,
% 0.53/0.88 (~P7(a19,a11)),
% 0.53/0.88 inference(scs_inference,[],[177,6,7,20,160,161,166])).
% 0.53/0.88 cnf(193,plain,
% 0.53/0.88 (~P7(a11,a19)),
% 0.53/0.88 inference(scs_inference,[],[177,6,7,20,160,161,166,165])).
% 0.53/0.88 cnf(195,plain,
% 0.53/0.88 (P9(a25,a21)),
% 0.53/0.88 inference(scs_inference,[],[177,6,7,12,13,20,160,161,166,165,164])).
% 0.53/0.88 cnf(219,plain,
% 0.53/0.88 (~P7(a19,a10)),
% 0.53/0.88 inference(scs_inference,[],[191,19,166])).
% 0.53/0.88 cnf(221,plain,
% 0.53/0.88 (~P7(a10,a19)),
% 0.53/0.88 inference(scs_inference,[],[191,193,19,166,165])).
% 0.53/0.88 cnf(223,plain,
% 0.53/0.88 (P6(a7,a2)),
% 0.53/0.88 inference(scs_inference,[],[191,193,179,9,19,166,165,161])).
% 0.53/0.88 cnf(225,plain,
% 0.53/0.88 (P9(a29,a25)),
% 0.53/0.88 inference(scs_inference,[],[191,193,179,9,14,15,19,166,165,161,164])).
% 0.53/0.88 cnf(235,plain,
% 0.53/0.88 (~P7(a19,a33)),
% 0.53/0.88 inference(scs_inference,[],[219,18,166])).
% 0.53/0.88 cnf(237,plain,
% 0.53/0.88 (P6(a4,a6)),
% 0.53/0.88 inference(scs_inference,[],[219,18,189,8,166,161])).
% 0.53/0.88 cnf(241,plain,
% 0.53/0.88 (P9(a33,a29)),
% 0.53/0.88 inference(scs_inference,[],[219,221,16,17,18,189,8,166,161,165,164])).
% 0.53/0.88 cnf(253,plain,
% 0.53/0.88 (P9(a24,a20)),
% 0.53/0.88 inference(scs_inference,[],[175,22,23,166,164])).
% 0.53/0.88 cnf(255,plain,
% 0.53/0.88 (~P7(a18,a15)),
% 0.53/0.88 inference(scs_inference,[],[47,175,22,23,35,166,164,165])).
% 0.53/0.88 cnf(259,plain,
% 0.53/0.88 (~P7(a15,a18)),
% 0.53/0.88 inference(scs_inference,[],[47,175,22,23,35,223,44,166,164,165,161,160])).
% 0.53/0.88 cnf(291,plain,
% 0.53/0.88 (~P7(a15,a17)),
% 0.53/0.88 inference(scs_inference,[],[259,34,166])).
% 0.53/0.88 cnf(295,plain,
% 0.53/0.88 (~P7(a17,a15)),
% 0.53/0.88 inference(scs_inference,[],[255,259,34,237,9,166,161,165])).
% 0.53/0.88 cnf(297,plain,
% 0.53/0.88 (P9(a28,a24)),
% 0.53/0.88 inference(scs_inference,[],[255,259,24,25,34,237,9,166,161,165,164])).
% 0.53/0.88 cnf(307,plain,
% 0.53/0.88 (~P7(a16,a15)),
% 0.53/0.88 inference(scs_inference,[],[295,33,165])).
% 0.53/0.88 cnf(311,plain,
% 0.53/0.88 (P9(a32,a28)),
% 0.53/0.88 inference(scs_inference,[],[291,295,26,27,33,165,166,164])).
% 0.53/0.88 cnf(323,plain,
% 0.53/0.88 (~P7(a14,a15)),
% 0.53/0.88 inference(scs_inference,[],[307,32,165])).
% 0.53/0.88 cnf(327,plain,
% 0.53/0.88 (P9(a35,a32)),
% 0.53/0.88 inference(scs_inference,[],[307,28,29,32,8,9,165,161,164])).
% 0.53/0.88 cnf(339,plain,
% 0.53/0.88 (P9(a14,a35)),
% 0.53/0.88 inference(scs_inference,[],[30,31,164])).
% 0.53/0.88 cnf(353,plain,
% 0.53/0.88 (P7(a21,a20)),
% 0.53/0.88 inference(scs_inference,[],[181,36,165])).
% 0.53/0.88 cnf(355,plain,
% 0.53/0.88 (P9(a25,a9)),
% 0.53/0.88 inference(scs_inference,[],[181,195,36,165,164])).
% 0.53/0.88 cnf(359,plain,
% 0.53/0.88 (~P7(a19,a29)),
% 0.53/0.88 inference(scs_inference,[],[235,181,195,241,36,9,44,165,164,161,166])).
% 0.53/0.88 cnf(361,plain,
% 0.53/0.88 (~P7(a29,a19)),
% 0.53/0.88 inference(scs_inference,[],[235,181,195,241,36,9,44,165,164,161,166,160])).
% 0.53/0.88 cnf(391,plain,
% 0.53/0.88 (~P7(a19,a25)),
% 0.53/0.88 inference(scs_inference,[],[359,361,225,165,166])).
% 0.53/0.88 cnf(393,plain,
% 0.53/0.88 (P9(a33,a25)),
% 0.53/0.88 inference(scs_inference,[],[359,361,225,241,165,166,164])).
% 0.53/0.88 cnf(399,plain,
% 0.53/0.88 (~P7(a35,a15)),
% 0.53/0.88 inference(scs_inference,[],[323,339,165])).
% 0.53/0.88 cnf(401,plain,
% 0.53/0.88 (P9(a28,a20)),
% 0.53/0.88 inference(scs_inference,[],[323,253,297,339,165,164])).
% 0.53/0.88 cnf(405,plain,
% 0.53/0.88 (~P7(a15,a35)),
% 0.53/0.88 inference(scs_inference,[],[323,353,253,297,339,165,164,166,160])).
% 0.53/0.88 cnf(415,plain,
% 0.53/0.88 (P9(a35,a28)),
% 0.53/0.88 inference(scs_inference,[],[399,405,311,327,165,166,164])).
% 0.53/0.88 cnf(421,plain,
% 0.53/0.88 (P7(a25,a20)),
% 0.53/0.88 inference(scs_inference,[],[355,36,165])).
% 0.53/0.88 cnf(423,plain,
% 0.53/0.88 (P9(a33,a9)),
% 0.53/0.88 inference(scs_inference,[],[355,393,36,165,164])).
% 0.53/0.88 cnf(437,plain,
% 0.53/0.88 (P9(a35,a20)),
% 0.53/0.88 inference(scs_inference,[],[399,421,401,415,165,166,164])).
% 0.53/0.88 cnf(447,plain,
% 0.53/0.88 (P9(a10,a9)),
% 0.53/0.88 inference(scs_inference,[],[423,18,36,165,164])).
% 0.53/0.88 cnf(449,plain,
% 0.53/0.88 (P7(a8,a35)),
% 0.53/0.88 inference(scs_inference,[],[175,423,437,18,36,165,164,166])).
% 0.53/0.88 cnf(458,plain,
% 0.53/0.88 (P9(a11,a9)),
% 0.53/0.88 inference(scs_inference,[],[391,447,13,19,36,165,166,164])).
% 0.53/0.88 cnf(466,plain,
% 0.53/0.88 (P9(a13,a9)),
% 0.53/0.88 inference(scs_inference,[],[458,20,36,165,164])).
% 0.53/0.88 cnf(478,plain,
% 0.53/0.88 (P9(a15,a9)),
% 0.53/0.88 inference(scs_inference,[],[235,466,17,21,36,165,166,164])).
% 0.53/0.88 cnf(484,plain,
% 0.53/0.88 (P7(a15,a20)),
% 0.53/0.88 inference(scs_inference,[],[478,36,165])).
% 0.53/0.88 cnf(486,plain,
% 0.53/0.88 (P9(a25,a8)),
% 0.53/0.88 inference(scs_inference,[],[478,11,195,36,165,164])).
% 0.53/0.88 cnf(492,plain,
% 0.53/0.88 (P7(a25,a35)),
% 0.53/0.88 inference(scs_inference,[],[449,486,165])).
% 0.53/0.88 cnf(568,plain,
% 0.53/0.88 ($false),
% 0.53/0.88 inference(scs_inference,[],[399,484,492,339,437,32,165,164,166,160]),
% 0.53/0.88 ['proof']).
% 0.53/0.88 % SZS output end Proof
% 0.53/0.88 % Total time :0.220000s
%------------------------------------------------------------------------------