%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CSR049+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 : n006.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:33 EDT 2024
% Result : Theorem 0.73s 0.78s
% Output : CNFRefutation 0.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : CSR049+1 : TPTP v8.2.0. Released v3.4.0.
% 0.04/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.32 % Computer : n006.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Wed Jun 19 20:31:38 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.19/0.54 start to proof:theBenchmark
% 0.52/0.75 %-------------------------------------------
% 0.52/0.75 % File :CSE---1.7
% 0.52/0.75 % Problem :theBenchmark
% 0.52/0.75 % Transform :cnf
% 0.52/0.75 % Format :tptp:raw
% 0.52/0.75 % Command :java -jar mcs_scs.jar %d %s
% 0.52/0.75
% 0.52/0.75 % Result :Theorem 0.140000s
% 0.52/0.75 % Output :CNFRefutation 0.140000s
% 0.52/0.75 %-------------------------------------------
% 0.52/0.75 %------------------------------------------------------------------------------
% 0.52/0.75 % File : CSR049+1 : TPTP v8.2.0. Released v3.4.0.
% 0.52/0.75 % Domain : Common Sense Reasoning
% 0.52/0.75 % Problem : Autogenerated Cyc Problem CSR049+1
% 0.52/0.75 % Version : Especial.
% 0.52/0.75 % English :
% 0.52/0.75
% 0.52/0.75 % Refs : [RS+] Reagan Smith et al., The Cyc TPTP Challenge Problem
% 0.52/0.75 % Source : [RS+]
% 0.52/0.75 % Names :
% 0.52/0.75
% 0.52/0.75 % Status : Theorem
% 0.52/0.75 % Rating : 0.00 v7.0.0, 0.25 v6.4.0, 0.00 v5.5.0, 0.11 v5.3.0, 0.09 v5.2.0, 0.00 v4.1.0, 0.11 v4.0.0, 0.10 v3.7.0, 0.00 v3.4.0
% 0.52/0.75 % Syntax : Number of formulae : 177 ( 39 unt; 0 def)
% 0.52/0.75 % Number of atoms : 328 ( 0 equ)
% 0.52/0.75 % Maximal formula atoms : 3 ( 1 avg)
% 0.52/0.75 % Number of connectives : 153 ( 2 ~; 0 |; 15 &)
% 0.52/0.75 % ( 0 <=>; 136 =>; 0 <=; 0 <~>)
% 0.52/0.75 % Maximal formula depth : 7 ( 3 avg)
% 0.52/0.75 % Maximal term depth : 1 ( 1 avg)
% 0.52/0.75 % Number of predicates : 45 ( 45 usr; 0 prp; 1-2 aty)
% 0.52/0.75 % Number of functors : 40 ( 40 usr; 40 con; 0-0 aty)
% 0.52/0.75 % Number of variables : 183 ( 183 !; 0 ?)
% 0.52/0.75 % SPC : FOF_THM_EPR_NEQ
% 0.52/0.75
% 0.52/0.75 % Comments : Autogenerated from the OpenCyc KB. Documentation can be found at
% 0.52/0.75 % http://opencyc.org/doc/#TPTP_Challenge_Problem_Set
% 0.52/0.75 % : Cyc(R) Knowledge Base Copyright(C) 1995-2007 Cycorp, Inc., Austin,
% 0.52/0.75 % TX, USA. All rights reserved.
% 0.52/0.75 % : OpenCyc Knowledge Base Copyright(C) 2001-2007 Cycorp, Inc.,
% 0.52/0.75 % Austin, TX, USA. All rights reserved.
% 0.52/0.75 %------------------------------------------------------------------------------
% 0.52/0.75 %$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.52/0.75 %$static(cyc_scaling_1,include('Axioms/CSR002+0.ax'))
% 0.52/0.75 %----Empty file include('Axioms/CSR002+0.ax').
% 0.52/0.75 %------------------------------------------------------------------------------
% 0.52/0.75 % Cyc Assertion #752062:
% 0.52/0.75 fof(just1,axiom,
% 0.52/0.75 genlmt(c_gregoriancalendarmt,c_basekb) ).
% 0.52/0.75
% 0.52/0.75 % Cyc Assertion #935028:
% 0.52/0.75 fof(just2,axiom,
% 0.52/0.75 genlmt(c_unitedstatesgeographypeoplemt,c_peopledatamt) ).
% 0.52/0.75
% 0.52/0.75 % Cyc Assertion #1315163:
% 0.52/0.75 fof(just3,axiom,
% 0.52/0.75 genlmt(c_unitedstatessociallifemt,c_gregoriancalendarmt) ).
% 0.52/0.75
% 0.52/0.75 % Cyc Assertion #1322220:
% 0.52/0.75 fof(just4,axiom,
% 0.52/0.76 transitivebinarypredicate(c_genlmt) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #1650755:
% 0.52/0.76 fof(just5,axiom,
% 0.52/0.76 genlmt(c_basekb,c_universalvocabularymt) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #1785295:
% 0.52/0.76 fof(just6,axiom,
% 0.52/0.76 genlmt(c_peopledatamt,c_unitedstatessociallifemt) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #1822756:
% 0.52/0.76 fof(just7,axiom,
% 0.52/0.76 genls(c_tptpcol_2_2,c_tptpcol_1_1) ).
% 0.52/0.76
% 0.52/0.76 fof(just8,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_2_2(OBJ)
% 0.52/0.76 => tptpcol_1_1(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #1863715:
% 0.52/0.76 fof(just9,axiom,
% 0.52/0.76 genls(c_tptpcol_3_16386,c_tptpcol_2_2) ).
% 0.52/0.76
% 0.52/0.76 fof(just10,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_3_16386(OBJ)
% 0.52/0.76 => tptpcol_2_2(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #1884194:
% 0.52/0.76 fof(just11,axiom,
% 0.52/0.76 genls(c_tptpcol_4_24578,c_tptpcol_3_16386) ).
% 0.52/0.76
% 0.52/0.76 fof(just12,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_4_24578(OBJ)
% 0.52/0.76 => tptpcol_3_16386(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #1884196:
% 0.52/0.76 fof(just13,axiom,
% 0.52/0.76 genls(c_tptpcol_5_24579,c_tptpcol_4_24578) ).
% 0.52/0.76
% 0.52/0.76 fof(just14,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_5_24579(OBJ)
% 0.52/0.76 => tptpcol_4_24578(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #1889315:
% 0.52/0.76 fof(just15,axiom,
% 0.52/0.76 genls(c_tptpcol_6_26627,c_tptpcol_5_24579) ).
% 0.52/0.76
% 0.52/0.76 fof(just16,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_6_26627(OBJ)
% 0.52/0.76 => tptpcol_5_24579(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #1889317:
% 0.52/0.76 fof(just17,axiom,
% 0.52/0.76 genls(c_tptpcol_7_26628,c_tptpcol_6_26627) ).
% 0.52/0.76
% 0.52/0.76 fof(just18,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_7_26628(OBJ)
% 0.52/0.76 => tptpcol_6_26627(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #1889319:
% 0.52/0.76 fof(just19,axiom,
% 0.52/0.76 genls(c_tptpcol_8_26629,c_tptpcol_7_26628) ).
% 0.52/0.76
% 0.52/0.76 fof(just20,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_8_26629(OBJ)
% 0.52/0.76 => tptpcol_7_26628(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #1889958:
% 0.52/0.76 fof(just21,axiom,
% 0.52/0.76 genls(c_tptpcol_9_26885,c_tptpcol_8_26629) ).
% 0.52/0.76
% 0.52/0.76 fof(just22,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_9_26885(OBJ)
% 0.52/0.76 => tptpcol_8_26629(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #1889960:
% 0.52/0.76 fof(just23,axiom,
% 0.52/0.76 genls(c_tptpcol_10_26886,c_tptpcol_9_26885) ).
% 0.52/0.76
% 0.52/0.76 fof(just24,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_10_26886(OBJ)
% 0.52/0.76 => tptpcol_9_26885(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #1889962:
% 0.52/0.76 fof(just25,axiom,
% 0.52/0.76 genls(c_tptpcol_11_26887,c_tptpcol_10_26886) ).
% 0.52/0.76
% 0.52/0.76 fof(just26,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_11_26887(OBJ)
% 0.52/0.76 => tptpcol_10_26886(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #1890041:
% 0.52/0.76 fof(just27,axiom,
% 0.52/0.76 genls(c_tptpcol_12_26919,c_tptpcol_11_26887) ).
% 0.52/0.76
% 0.52/0.76 fof(just28,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_12_26919(OBJ)
% 0.52/0.76 => tptpcol_11_26887(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #1890043:
% 0.52/0.76 fof(just29,axiom,
% 0.52/0.76 genls(c_tptpcol_13_26920,c_tptpcol_12_26919) ).
% 0.52/0.76
% 0.52/0.76 fof(just30,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_13_26920(OBJ)
% 0.52/0.76 => tptpcol_12_26919(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #1890045:
% 0.52/0.76 fof(just31,axiom,
% 0.52/0.76 genls(c_tptpcol_14_26921,c_tptpcol_13_26920) ).
% 0.52/0.76
% 0.52/0.76 fof(just32,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_14_26921(OBJ)
% 0.52/0.76 => tptpcol_13_26920(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #1890054:
% 0.52/0.76 fof(just33,axiom,
% 0.52/0.76 genls(c_tptpcol_15_26925,c_tptpcol_14_26921) ).
% 0.52/0.76
% 0.52/0.76 fof(just34,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_15_26925(OBJ)
% 0.52/0.76 => tptpcol_14_26921(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #1890056:
% 0.52/0.76 fof(just35,axiom,
% 0.52/0.76 genls(c_tptpcol_16_26926,c_tptpcol_15_26925) ).
% 0.52/0.76
% 0.52/0.76 fof(just36,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_16_26926(OBJ)
% 0.52/0.76 => tptpcol_15_26925(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #1986593:
% 0.52/0.76 fof(just37,axiom,
% 0.52/0.76 genls(c_tptpcol_2_65537,c_tptpcol_1_65536) ).
% 0.52/0.76
% 0.52/0.76 fof(just38,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_2_65537(OBJ)
% 0.52/0.76 => tptpcol_1_65536(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #2027552:
% 0.52/0.76 fof(just39,axiom,
% 0.52/0.76 genls(c_tptpcol_3_81921,c_tptpcol_2_65537) ).
% 0.52/0.76
% 0.52/0.76 fof(just40,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_3_81921(OBJ)
% 0.52/0.76 => tptpcol_2_65537(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #2048031:
% 0.52/0.76 fof(just41,axiom,
% 0.52/0.76 genls(c_tptpcol_4_90113,c_tptpcol_3_81921) ).
% 0.52/0.76
% 0.52/0.76 fof(just42,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_4_90113(OBJ)
% 0.52/0.76 => tptpcol_3_81921(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #2048033:
% 0.52/0.76 fof(just43,axiom,
% 0.52/0.76 genls(c_tptpcol_5_90114,c_tptpcol_4_90113) ).
% 0.52/0.76
% 0.52/0.76 fof(just44,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_5_90114(OBJ)
% 0.52/0.76 => tptpcol_4_90113(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #2053152:
% 0.52/0.76 fof(just45,axiom,
% 0.52/0.76 genls(c_tptpcol_6_92162,c_tptpcol_5_90114) ).
% 0.52/0.76
% 0.52/0.76 fof(just46,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_6_92162(OBJ)
% 0.52/0.76 => tptpcol_5_90114(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #2053154:
% 0.52/0.76 fof(just47,axiom,
% 0.52/0.76 genls(c_tptpcol_7_92163,c_tptpcol_6_92162) ).
% 0.52/0.76
% 0.52/0.76 fof(just48,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_7_92163(OBJ)
% 0.52/0.76 => tptpcol_6_92162(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #2053156:
% 0.52/0.76 fof(just49,axiom,
% 0.52/0.76 genls(c_tptpcol_8_92164,c_tptpcol_7_92163) ).
% 0.52/0.76
% 0.52/0.76 fof(just50,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_8_92164(OBJ)
% 0.52/0.76 => tptpcol_7_92163(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #2053158:
% 0.52/0.76 fof(just51,axiom,
% 0.52/0.76 genls(c_tptpcol_9_92165,c_tptpcol_8_92164) ).
% 0.52/0.76
% 0.52/0.76 fof(just52,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_9_92165(OBJ)
% 0.52/0.76 => tptpcol_8_92164(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #2053160:
% 0.52/0.76 fof(just53,axiom,
% 0.52/0.76 genls(c_tptpcol_10_92166,c_tptpcol_9_92165) ).
% 0.52/0.76
% 0.52/0.76 fof(just54,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_10_92166(OBJ)
% 0.52/0.76 => tptpcol_9_92165(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #2053319:
% 0.52/0.76 fof(just55,axiom,
% 0.52/0.76 genls(c_tptpcol_11_92230,c_tptpcol_10_92166) ).
% 0.52/0.76
% 0.52/0.76 fof(just56,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_11_92230(OBJ)
% 0.52/0.76 => tptpcol_10_92166(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #2053398:
% 0.52/0.76 fof(just57,axiom,
% 0.52/0.76 genls(c_tptpcol_12_92262,c_tptpcol_11_92230) ).
% 0.52/0.76
% 0.52/0.76 fof(just58,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_12_92262(OBJ)
% 0.52/0.76 => tptpcol_11_92230(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #2053400:
% 0.52/0.76 fof(just59,axiom,
% 0.52/0.76 genls(c_tptpcol_13_92263,c_tptpcol_12_92262) ).
% 0.52/0.76
% 0.52/0.76 fof(just60,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.76 ( tptpcol_13_92263(OBJ)
% 0.52/0.76 => tptpcol_12_92262(OBJ) ) ).
% 0.52/0.76
% 0.52/0.76 % Cyc Assertion #2053402:
% 0.52/0.76 fof(just61,axiom,
% 0.52/0.76 genls(c_tptpcol_14_92264,c_tptpcol_13_92263) ).
% 0.52/0.76
% 0.52/0.76 fof(just62,axiom,
% 0.52/0.76 ! [OBJ] :
% 0.52/0.77 ( tptpcol_14_92264(OBJ)
% 0.52/0.77 => tptpcol_13_92263(OBJ) ) ).
% 0.52/0.77
% 0.52/0.77 % Cyc Assertion #2053411:
% 0.52/0.77 fof(just63,axiom,
% 0.52/0.77 genls(c_tptpcol_15_92268,c_tptpcol_14_92264) ).
% 0.52/0.77
% 0.52/0.77 fof(just64,axiom,
% 0.52/0.77 ! [OBJ] :
% 0.52/0.77 ( tptpcol_15_92268(OBJ)
% 0.52/0.77 => tptpcol_14_92264(OBJ) ) ).
% 0.52/0.77
% 0.52/0.77 % Cyc Assertion #2053413:
% 0.52/0.77 fof(just65,axiom,
% 0.52/0.77 genls(c_tptpcol_16_92269,c_tptpcol_15_92268) ).
% 0.52/0.77
% 0.52/0.77 fof(just66,axiom,
% 0.52/0.77 ! [OBJ] :
% 0.52/0.77 ( tptpcol_16_92269(OBJ)
% 0.52/0.77 => tptpcol_15_92268(OBJ) ) ).
% 0.52/0.77
% 0.52/0.77 % Cyc Assertion #2150427:
% 0.52/0.77 fof(just67,axiom,
% 0.52/0.77 disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536) ).
% 0.52/0.77
% 0.52/0.77 fof(just68,axiom,
% 0.52/0.77 ! [OBJ] :
% 0.52/0.77 ~ ( tptpcol_1_1(OBJ)
% 0.52/0.77 & tptpcol_1_65536(OBJ) ) ).
% 0.52/0.77
% 0.52/0.77 % Cyc Assertion #398814:
% 0.52/0.77 fof(just69,axiom,
% 0.52/0.77 ! [OBJ,COL1,COL2] :
% 0.52/0.77 ~ ( isa(OBJ,COL1)
% 0.52/0.77 & isa(OBJ,COL2)
% 0.52/0.77 & disjointwith(COL1,COL2) ) ).
% 0.52/0.77
% 0.52/0.77 % Cyc Assertion #831913:
% 0.52/0.77 fof(just70,axiom,
% 0.52/0.77 ! [SPECPRED,PRED,GENLPRED] :
% 0.52/0.77 ( ( genlinverse(SPECPRED,PRED)
% 0.52/0.77 & genlinverse(PRED,GENLPRED) )
% 0.52/0.77 => genlpreds(SPECPRED,GENLPRED) ) ).
% 0.52/0.77
% 0.52/0.77 % Cyc Constant #40273:
% 0.52/0.77 fof(just71,axiom,
% 0.52/0.77 ! [ARG1,INS] :
% 0.52/0.77 ( genlpreds(ARG1,INS)
% 0.52/0.77 => predicate(INS) ) ).
% 0.52/0.77
% 0.52/0.77 fof(just72,axiom,
% 0.52/0.77 ! [ARG1,INS] :
% 0.52/0.77 ( genlpreds(ARG1,INS)
% 0.52/0.77 => predicate(INS) ) ).
% 0.52/0.77
% 0.52/0.77 fof(just73,axiom,
% 0.52/0.77 ! [INS,ARG2] :
% 0.52/0.77 ( genlpreds(INS,ARG2)
% 0.52/0.77 => predicate(INS) ) ).
% 0.52/0.77
% 0.52/0.77 fof(just74,axiom,
% 0.52/0.77 ! [INS,ARG2] :
% 0.52/0.77 ( genlpreds(INS,ARG2)
% 0.52/0.77 => predicate(INS) ) ).
% 0.52/0.77
% 0.52/0.77 fof(just75,axiom,
% 0.52/0.77 ! [X,Y,Z] :
% 0.52/0.77 ( ( genlpreds(X,Y)
% 0.52/0.77 & genlpreds(Y,Z) )
% 0.52/0.77 => genlpreds(X,Z) ) ).
% 0.52/0.77
% 0.52/0.77 fof(just76,axiom,
% 0.52/0.77 ! [X] :
% 0.52/0.77 ( predicate(X)
% 0.52/0.77 => genlpreds(X,X) ) ).
% 0.52/0.77
% 0.52/0.77 fof(just77,axiom,
% 0.52/0.77 ! [X] :
% 0.52/0.77 ( predicate(X)
% 0.52/0.77 => genlpreds(X,X) ) ).
% 0.52/0.77
% 0.52/0.77 % Cyc Constant #45259:
% 0.52/0.77 fof(just78,axiom,
% 0.52/0.77 ! [ARG1,INS] :
% 0.52/0.77 ( genlinverse(ARG1,INS)
% 0.52/0.77 => binarypredicate(INS) ) ).
% 0.52/0.77
% 0.52/0.77 fof(just79,axiom,
% 0.52/0.77 ! [INS,ARG2] :
% 0.52/0.77 ( genlinverse(INS,ARG2)
% 0.52/0.77 => binarypredicate(INS) ) ).
% 0.52/0.77
% 0.52/0.77 fof(just80,axiom,
% 0.52/0.77 ! [OLD,ARG2,NEW] :
% 0.52/0.77 ( ( genlinverse(OLD,ARG2)
% 0.52/0.77 & genlpreds(NEW,OLD) )
% 0.52/0.77 => genlinverse(NEW,ARG2) ) ).
% 0.52/0.77
% 0.52/0.77 fof(just81,axiom,
% 0.52/0.77 ! [ARG1,OLD,NEW] :
% 0.52/0.77 ( ( genlinverse(ARG1,OLD)
% 0.52/0.77 & genlpreds(OLD,NEW) )
% 0.52/0.77 => genlinverse(ARG1,NEW) ) ).
% 0.52/0.77
% 0.52/0.77 % Cyc Constant #78648:
% 0.52/0.77 fof(just82,axiom,
% 0.52/0.77 ! [ARG1,INS] :
% 0.52/0.77 ( disjointwith(ARG1,INS)
% 0.52/0.77 => collection(INS) ) ).
% 0.52/0.77
% 0.52/0.77 fof(just83,axiom,
% 0.52/0.77 ! [INS,ARG2] :
% 0.52/0.77 ( disjointwith(INS,ARG2)
% 0.52/0.77 => collection(INS) ) ).
% 0.52/0.77
% 0.52/0.77 fof(just84,axiom,
% 0.52/0.77 ! [X,Y] :
% 0.52/0.77 ( disjointwith(X,Y)
% 0.52/0.77 => disjointwith(Y,X) ) ).
% 0.52/0.77
% 0.52/0.77 fof(just85,axiom,
% 0.52/0.77 ! [ARG1,OLD,NEW] :
% 0.52/0.77 ( ( disjointwith(ARG1,OLD)
% 0.52/0.77 & genls(NEW,OLD) )
% 0.52/0.77 => disjointwith(ARG1,NEW) ) ).
% 0.52/0.77
% 0.52/0.77 fof(just86,axiom,
% 0.52/0.77 ! [OLD,ARG2,NEW] :
% 0.52/0.77 ( ( disjointwith(OLD,ARG2)
% 0.52/0.77 & genls(NEW,OLD) )
% 0.73/0.77 => disjointwith(NEW,ARG2) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #221866:
% 0.73/0.77 fof(just87,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_16_92269)
% 0.73/0.77 => tptpcol_16_92269(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just88,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_16_92269(X)
% 0.73/0.77 => isa(X,c_tptpcol_16_92269) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #221865:
% 0.73/0.77 fof(just89,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_15_92268)
% 0.73/0.77 => tptpcol_15_92268(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just90,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_15_92268(X)
% 0.73/0.77 => isa(X,c_tptpcol_15_92268) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #221861:
% 0.73/0.77 fof(just91,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_14_92264)
% 0.73/0.77 => tptpcol_14_92264(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just92,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_14_92264(X)
% 0.73/0.77 => isa(X,c_tptpcol_14_92264) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #221860:
% 0.73/0.77 fof(just93,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_13_92263)
% 0.73/0.77 => tptpcol_13_92263(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just94,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_13_92263(X)
% 0.73/0.77 => isa(X,c_tptpcol_13_92263) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #221859:
% 0.73/0.77 fof(just95,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_12_92262)
% 0.73/0.77 => tptpcol_12_92262(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just96,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_12_92262(X)
% 0.73/0.77 => isa(X,c_tptpcol_12_92262) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #221827:
% 0.73/0.77 fof(just97,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_11_92230)
% 0.73/0.77 => tptpcol_11_92230(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just98,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_11_92230(X)
% 0.73/0.77 => isa(X,c_tptpcol_11_92230) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #221763:
% 0.73/0.77 fof(just99,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_10_92166)
% 0.73/0.77 => tptpcol_10_92166(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just100,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_10_92166(X)
% 0.73/0.77 => isa(X,c_tptpcol_10_92166) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #221762:
% 0.73/0.77 fof(just101,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_9_92165)
% 0.73/0.77 => tptpcol_9_92165(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just102,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_9_92165(X)
% 0.73/0.77 => isa(X,c_tptpcol_9_92165) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #221761:
% 0.73/0.77 fof(just103,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_8_92164)
% 0.73/0.77 => tptpcol_8_92164(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just104,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_8_92164(X)
% 0.73/0.77 => isa(X,c_tptpcol_8_92164) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #221760:
% 0.73/0.77 fof(just105,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_7_92163)
% 0.73/0.77 => tptpcol_7_92163(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just106,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_7_92163(X)
% 0.73/0.77 => isa(X,c_tptpcol_7_92163) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #221759:
% 0.73/0.77 fof(just107,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_6_92162)
% 0.73/0.77 => tptpcol_6_92162(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just108,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_6_92162(X)
% 0.73/0.77 => isa(X,c_tptpcol_6_92162) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #219711:
% 0.73/0.77 fof(just109,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_5_90114)
% 0.73/0.77 => tptpcol_5_90114(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just110,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_5_90114(X)
% 0.73/0.77 => isa(X,c_tptpcol_5_90114) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #219710:
% 0.73/0.77 fof(just111,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_4_90113)
% 0.73/0.77 => tptpcol_4_90113(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just112,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_4_90113(X)
% 0.73/0.77 => isa(X,c_tptpcol_4_90113) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #211518:
% 0.73/0.77 fof(just113,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_3_81921)
% 0.73/0.77 => tptpcol_3_81921(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just114,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_3_81921(X)
% 0.73/0.77 => isa(X,c_tptpcol_3_81921) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #195133:
% 0.73/0.77 fof(just115,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_1_65536)
% 0.73/0.77 => tptpcol_1_65536(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just116,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_1_65536(X)
% 0.73/0.77 => isa(X,c_tptpcol_1_65536) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #195134:
% 0.73/0.77 fof(just117,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_2_65537)
% 0.73/0.77 => tptpcol_2_65537(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just118,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_2_65537(X)
% 0.73/0.77 => isa(X,c_tptpcol_2_65537) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #156523:
% 0.73/0.77 fof(just119,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_16_26926)
% 0.73/0.77 => tptpcol_16_26926(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just120,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_16_26926(X)
% 0.73/0.77 => isa(X,c_tptpcol_16_26926) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #156522:
% 0.73/0.77 fof(just121,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_15_26925)
% 0.73/0.77 => tptpcol_15_26925(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just122,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_15_26925(X)
% 0.73/0.77 => isa(X,c_tptpcol_15_26925) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #156518:
% 0.73/0.77 fof(just123,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_14_26921)
% 0.73/0.77 => tptpcol_14_26921(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just124,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_14_26921(X)
% 0.73/0.77 => isa(X,c_tptpcol_14_26921) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #156517:
% 0.73/0.77 fof(just125,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_13_26920)
% 0.73/0.77 => tptpcol_13_26920(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just126,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_13_26920(X)
% 0.73/0.77 => isa(X,c_tptpcol_13_26920) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #156516:
% 0.73/0.77 fof(just127,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_12_26919)
% 0.73/0.77 => tptpcol_12_26919(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just128,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_12_26919(X)
% 0.73/0.77 => isa(X,c_tptpcol_12_26919) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #156484:
% 0.73/0.77 fof(just129,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_11_26887)
% 0.73/0.77 => tptpcol_11_26887(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just130,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_11_26887(X)
% 0.73/0.77 => isa(X,c_tptpcol_11_26887) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #156483:
% 0.73/0.77 fof(just131,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_10_26886)
% 0.73/0.77 => tptpcol_10_26886(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just132,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_10_26886(X)
% 0.73/0.77 => isa(X,c_tptpcol_10_26886) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #156482:
% 0.73/0.77 fof(just133,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_9_26885)
% 0.73/0.77 => tptpcol_9_26885(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just134,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_9_26885(X)
% 0.73/0.77 => isa(X,c_tptpcol_9_26885) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #156226:
% 0.73/0.77 fof(just135,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_8_26629)
% 0.73/0.77 => tptpcol_8_26629(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just136,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_8_26629(X)
% 0.73/0.77 => isa(X,c_tptpcol_8_26629) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #156225:
% 0.73/0.77 fof(just137,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_7_26628)
% 0.73/0.77 => tptpcol_7_26628(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just138,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_7_26628(X)
% 0.73/0.77 => isa(X,c_tptpcol_7_26628) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #156224:
% 0.73/0.77 fof(just139,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_6_26627)
% 0.73/0.77 => tptpcol_6_26627(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just140,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( tptpcol_6_26627(X)
% 0.73/0.77 => isa(X,c_tptpcol_6_26627) ) ).
% 0.73/0.77
% 0.73/0.77 % Cyc Constant #154176:
% 0.73/0.77 fof(just141,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.77 ( isa(X,c_tptpcol_5_24579)
% 0.73/0.77 => tptpcol_5_24579(X) ) ).
% 0.73/0.77
% 0.73/0.77 fof(just142,axiom,
% 0.73/0.77 ! [X] :
% 0.73/0.78 ( tptpcol_5_24579(X)
% 0.73/0.78 => isa(X,c_tptpcol_5_24579) ) ).
% 0.73/0.78
% 0.73/0.78 % Cyc Constant #154175:
% 0.73/0.78 fof(just143,axiom,
% 0.73/0.78 ! [X] :
% 0.73/0.78 ( isa(X,c_tptpcol_4_24578)
% 0.73/0.78 => tptpcol_4_24578(X) ) ).
% 0.73/0.78
% 0.73/0.78 fof(just144,axiom,
% 0.73/0.78 ! [X] :
% 0.73/0.78 ( tptpcol_4_24578(X)
% 0.73/0.78 => isa(X,c_tptpcol_4_24578) ) ).
% 0.73/0.78
% 0.73/0.78 % Cyc Constant #145983:
% 0.73/0.78 fof(just145,axiom,
% 0.73/0.78 ! [X] :
% 0.73/0.78 ( isa(X,c_tptpcol_3_16386)
% 0.73/0.78 => tptpcol_3_16386(X) ) ).
% 0.73/0.78
% 0.73/0.78 fof(just146,axiom,
% 0.73/0.78 ! [X] :
% 0.73/0.78 ( tptpcol_3_16386(X)
% 0.73/0.78 => isa(X,c_tptpcol_3_16386) ) ).
% 0.73/0.78
% 0.73/0.78 % Cyc Constant #129598:
% 0.73/0.78 fof(just147,axiom,
% 0.73/0.78 ! [X] :
% 0.73/0.78 ( isa(X,c_tptpcol_1_1)
% 0.73/0.78 => tptpcol_1_1(X) ) ).
% 0.73/0.78
% 0.73/0.78 fof(just148,axiom,
% 0.73/0.78 ! [X] :
% 0.73/0.78 ( tptpcol_1_1(X)
% 0.73/0.78 => isa(X,c_tptpcol_1_1) ) ).
% 0.73/0.78
% 0.73/0.78 % Cyc Constant #129599:
% 0.73/0.78 fof(just149,axiom,
% 0.73/0.78 ! [X] :
% 0.73/0.78 ( isa(X,c_tptpcol_2_2)
% 0.73/0.78 => tptpcol_2_2(X) ) ).
% 0.73/0.78
% 0.73/0.78 fof(just150,axiom,
% 0.73/0.78 ! [X] :
% 0.73/0.78 ( tptpcol_2_2(X)
% 0.73/0.78 => isa(X,c_tptpcol_2_2) ) ).
% 0.73/0.78
% 0.73/0.78 % Cyc Constant #0:
% 0.73/0.78 fof(just151,axiom,
% 0.73/0.78 ! [ARG1,INS] :
% 0.73/0.78 ( genls(ARG1,INS)
% 0.73/0.78 => collection(INS) ) ).
% 0.73/0.78
% 0.73/0.78 fof(just152,axiom,
% 0.73/0.78 ! [ARG1,INS] :
% 0.73/0.78 ( genls(ARG1,INS)
% 0.73/0.78 => collection(INS) ) ).
% 0.73/0.78
% 0.73/0.78 fof(just153,axiom,
% 0.73/0.78 ! [INS,ARG2] :
% 0.73/0.78 ( genls(INS,ARG2)
% 0.73/0.78 => collection(INS) ) ).
% 0.73/0.78
% 0.73/0.78 fof(just154,axiom,
% 0.73/0.78 ! [INS,ARG2] :
% 0.73/0.78 ( genls(INS,ARG2)
% 0.73/0.78 => collection(INS) ) ).
% 0.73/0.78
% 0.73/0.78 fof(just155,axiom,
% 0.73/0.78 ! [X,Y,Z] :
% 0.73/0.78 ( ( genls(X,Y)
% 0.73/0.78 & genls(Y,Z) )
% 0.73/0.78 => genls(X,Z) ) ).
% 0.73/0.78
% 0.73/0.78 fof(just156,axiom,
% 0.73/0.78 ! [X] :
% 0.73/0.78 ( collection(X)
% 0.73/0.78 => genls(X,X) ) ).
% 0.73/0.78
% 0.73/0.78 fof(just157,axiom,
% 0.73/0.78 ! [X] :
% 0.73/0.78 ( collection(X)
% 0.73/0.78 => genls(X,X) ) ).
% 0.73/0.78
% 0.73/0.78 fof(just158,axiom,
% 0.73/0.78 ! [OLD,ARG2,NEW] :
% 0.73/0.78 ( ( genls(OLD,ARG2)
% 0.73/0.78 & genls(NEW,OLD) )
% 0.73/0.78 => genls(NEW,ARG2) ) ).
% 0.73/0.78
% 0.73/0.78 fof(just159,axiom,
% 0.73/0.78 ! [ARG1,OLD,NEW] :
% 0.73/0.78 ( ( genls(ARG1,OLD)
% 0.73/0.78 & genls(OLD,NEW) )
% 0.73/0.78 => genls(ARG1,NEW) ) ).
% 0.73/0.78
% 0.73/0.78 % Cyc Constant #127156:
% 0.73/0.78 fof(just160,axiom,
% 0.73/0.78 ! [X] :
% 0.73/0.78 ( isa(X,c_transitivebinarypredicate)
% 0.73/0.78 => transitivebinarypredicate(X) ) ).
% 0.73/0.78
% 0.73/0.78 fof(just161,axiom,
% 0.73/0.78 ! [X] :
% 0.73/0.78 ( transitivebinarypredicate(X)
% 0.73/0.78 => isa(X,c_transitivebinarypredicate) ) ).
% 0.73/0.78
% 0.73/0.78 % Cyc Constant #72115:
% 0.73/0.78 fof(just162,axiom,
% 0.73/0.78 ! [ARG1,INS] :
% 0.73/0.78 ( isa(ARG1,INS)
% 0.73/0.78 => collection(INS) ) ).
% 0.73/0.78
% 0.73/0.78 fof(just163,axiom,
% 0.73/0.78 ! [ARG1,INS] :
% 0.73/0.78 ( isa(ARG1,INS)
% 0.73/0.78 => collection(INS) ) ).
% 0.73/0.78
% 0.73/0.78 fof(just164,axiom,
% 0.73/0.78 ! [INS,ARG2] :
% 0.73/0.78 ( isa(INS,ARG2)
% 0.73/0.78 => thing(INS) ) ).
% 0.73/0.78
% 0.73/0.78 fof(just165,axiom,
% 0.73/0.78 ! [INS,ARG2] :
% 0.73/0.78 ( isa(INS,ARG2)
% 0.73/0.78 => thing(INS) ) ).
% 0.73/0.78
% 0.73/0.78 fof(just166,axiom,
% 0.73/0.78 ! [ARG1,OLD,NEW] :
% 0.73/0.78 ( ( isa(ARG1,OLD)
% 0.73/0.78 & genls(OLD,NEW) )
% 0.73/0.78 => isa(ARG1,NEW) ) ).
% 0.73/0.78
% 0.73/0.78 % Cyc Constant #95028:
% 0.73/0.78 fof(just167,axiom,
% 0.73/0.78 mtvisible(c_universalvocabularymt) ).
% 0.73/0.78
% 0.73/0.78 % Cyc Constant #19550:
% 0.73/0.78 fof(just168,axiom,
% 0.73/0.78 ! [SPECMT,GENLMT] :
% 0.73/0.78 ( ( mtvisible(SPECMT)
% 0.73/0.78 & genlmt(SPECMT,GENLMT) )
% 0.73/0.78 => mtvisible(GENLMT) ) ).
% 0.73/0.78
% 0.73/0.78 fof(just169,axiom,
% 0.73/0.78 ! [ARG1,INS] :
% 0.73/0.78 ( genlmt(ARG1,INS)
% 0.73/0.78 => microtheory(INS) ) ).
% 0.73/0.78
% 0.73/0.78 fof(just170,axiom,
% 0.73/0.78 ! [ARG1,INS] :
% 0.73/0.78 ( genlmt(ARG1,INS)
% 0.73/0.78 => microtheory(INS) ) ).
% 0.73/0.78
% 0.73/0.78 fof(just171,axiom,
% 0.73/0.78 ! [INS,ARG2] :
% 0.73/0.78 ( genlmt(INS,ARG2)
% 0.73/0.78 => microtheory(INS) ) ).
% 0.73/0.78
% 0.73/0.78 fof(just172,axiom,
% 0.73/0.78 ! [INS,ARG2] :
% 0.73/0.78 ( genlmt(INS,ARG2)
% 0.73/0.78 => microtheory(INS) ) ).
% 0.73/0.78
% 0.73/0.78 fof(just173,axiom,
% 0.73/0.78 ! [X,Y,Z] :
% 0.73/0.78 ( ( genlmt(X,Y)
% 0.73/0.78 & genlmt(Y,Z) )
% 0.73/0.78 => genlmt(X,Z) ) ).
% 0.73/0.78
% 0.73/0.78 fof(just174,axiom,
% 0.73/0.78 ! [X] :
% 0.73/0.78 ( microtheory(X)
% 0.73/0.78 => genlmt(X,X) ) ).
% 0.73/0.78
% 0.73/0.78 fof(just175,axiom,
% 0.73/0.78 ! [X] :
% 0.73/0.78 ( microtheory(X)
% 0.73/0.78 => genlmt(X,X) ) ).
% 0.73/0.78
% 0.73/0.78 % Cyc Constant #27757:
% 0.73/0.78 fof(just176,axiom,
% 0.73/0.78 mtvisible(c_basekb) ).
% 0.73/0.78
% 0.73/0.78 fof(query49,conjecture,
% 0.73/0.78 ( mtvisible(c_unitedstatesgeographypeoplemt)
% 0.73/0.78 => disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269) ) ).
% 0.73/0.78
% 0.73/0.78 %------------------------------------------------------------------------------
% 0.73/0.78 %-------------------------------------------
% 0.73/0.78 % Proof found
% 0.73/0.78 % SZS status Theorem for theBenchmark
% 0.73/0.78 % SZS output start Proof
% 0.73/0.78 %ClaNum:178(EqnAxiom:0)
% 0.73/0.78 %VarNum:307(SingletonVarNum:158)
% 0.73/0.78 %MaxLitNum:3
% 0.73/0.78 %MaxfuncDepth:0
% 0.73/0.78 %SharedTerms:81
% 0.73/0.78 %goalClause: 3 41
% 0.73/0.78 %singleGoalClaCount:2
% 0.73/0.78 [1]P1(a1)
% 0.73/0.78 [2]P2(a2)
% 0.73/0.78 [3]P2(a3)
% 0.73/0.78 [4]P2(a39)
% 0.73/0.78 [5]P3(a4,a2)
% 0.73/0.78 [6]P3(a2,a39)
% 0.73/0.78 [7]P3(a3,a5)
% 0.73/0.78 [8]P3(a5,a40)
% 0.73/0.78 [9]P3(a40,a4)
% 0.73/0.78 [10]P8(a6,a7)
% 0.73/0.78 [11]P8(a23,a6)
% 0.73/0.78 [12]P8(a25,a23)
% 0.73/0.78 [13]P8(a27,a25)
% 0.73/0.78 [14]P8(a29,a27)
% 0.73/0.78 [15]P8(a31,a29)
% 0.73/0.78 [16]P8(a33,a31)
% 0.73/0.78 [17]P8(a35,a33)
% 0.73/0.78 [18]P8(a8,a35)
% 0.73/0.78 [19]P8(a9,a8)
% 0.73/0.78 [20]P8(a11,a9)
% 0.73/0.78 [21]P8(a13,a11)
% 0.73/0.78 [22]P8(a15,a13)
% 0.73/0.78 [23]P8(a17,a15)
% 0.73/0.78 [24]P8(a19,a17)
% 0.73/0.78 [25]P8(a24,a22)
% 0.73/0.78 [26]P8(a26,a24)
% 0.73/0.78 [27]P8(a28,a26)
% 0.73/0.78 [28]P8(a30,a28)
% 0.73/0.78 [29]P8(a32,a30)
% 0.73/0.78 [30]P8(a34,a32)
% 0.73/0.78 [31]P8(a36,a34)
% 0.73/0.78 [32]P8(a37,a36)
% 0.73/0.78 [33]P8(a10,a37)
% 0.73/0.78 [34]P8(a12,a10)
% 0.73/0.78 [35]P8(a14,a12)
% 0.73/0.78 [36]P8(a16,a14)
% 0.73/0.78 [37]P8(a18,a16)
% 0.73/0.78 [38]P8(a20,a18)
% 0.73/0.78 [39]P8(a21,a20)
% 0.73/0.78 [40]P4(a7,a22)
% 0.73/0.78 [41]~P4(a19,a21)
% 0.73/0.78 [42]~P31(x421)+P12(x421)
% 0.73/0.78 [43]~P12(x431)+P13(x431)
% 0.73/0.78 [44]~P33(x441)+P31(x441)
% 0.73/0.78 [45]~P35(x451)+P33(x451)
% 0.73/0.78 [46]~P37(x461)+P35(x461)
% 0.73/0.78 [47]~P39(x471)+P37(x471)
% 0.73/0.78 [48]~P41(x481)+P39(x481)
% 0.73/0.78 [49]~P43(x491)+P41(x491)
% 0.73/0.78 [50]~P14(x501)+P43(x501)
% 0.73/0.78 [51]~P17(x511)+P14(x511)
% 0.73/0.78 [52]~P19(x521)+P17(x521)
% 0.73/0.78 [53]~P21(x531)+P19(x531)
% 0.73/0.78 [54]~P23(x541)+P21(x541)
% 0.73/0.78 [55]~P25(x551)+P23(x551)
% 0.73/0.78 [56]~P27(x561)+P25(x561)
% 0.73/0.78 [57]~P34(x571)+P32(x571)
% 0.73/0.78 [58]~P32(x581)+P30(x581)
% 0.73/0.78 [59]~P36(x591)+P34(x591)
% 0.73/0.78 [60]~P38(x601)+P36(x601)
% 0.73/0.78 [61]~P40(x611)+P38(x611)
% 0.73/0.78 [62]~P42(x621)+P40(x621)
% 0.73/0.78 [63]~P44(x631)+P42(x631)
% 0.73/0.78 [64]~P45(x641)+P44(x641)
% 0.73/0.78 [65]~P18(x651)+P45(x651)
% 0.73/0.78 [66]~P20(x661)+P18(x661)
% 0.73/0.78 [67]~P22(x671)+P20(x671)
% 0.73/0.78 [68]~P24(x681)+P22(x681)
% 0.73/0.78 [69]~P26(x691)+P24(x691)
% 0.73/0.78 [70]~P28(x701)+P26(x701)
% 0.73/0.78 [71]~P29(x711)+P28(x711)
% 0.73/0.78 [72]~P30(x721)+~P13(x721)
% 0.73/0.78 [73]~P12(x731)+P10(x731,a6)
% 0.73/0.78 [74]~P13(x741)+P10(x741,a7)
% 0.73/0.78 [75]~P31(x751)+P10(x751,a23)
% 0.73/0.78 [76]~P33(x761)+P10(x761,a25)
% 0.73/0.78 [77]~P35(x771)+P10(x771,a27)
% 0.73/0.78 [78]~P37(x781)+P10(x781,a29)
% 0.73/0.78 [79]~P39(x791)+P10(x791,a31)
% 0.73/0.78 [80]~P41(x801)+P10(x801,a33)
% 0.73/0.78 [81]~P43(x811)+P10(x811,a35)
% 0.73/0.78 [82]~P14(x821)+P10(x821,a8)
% 0.73/0.78 [83]~P17(x831)+P10(x831,a9)
% 0.73/0.78 [84]~P19(x841)+P10(x841,a11)
% 0.73/0.78 [85]~P21(x851)+P10(x851,a13)
% 0.73/0.78 [86]~P23(x861)+P10(x861,a15)
% 0.73/0.78 [87]~P25(x871)+P10(x871,a17)
% 0.73/0.78 [88]~P27(x881)+P10(x881,a19)
% 0.73/0.78 [89]~P32(x891)+P10(x891,a24)
% 0.73/0.78 [90]~P30(x901)+P10(x901,a22)
% 0.73/0.78 [91]~P34(x911)+P10(x911,a26)
% 0.73/0.78 [92]~P36(x921)+P10(x921,a28)
% 0.73/0.78 [93]~P38(x931)+P10(x931,a30)
% 0.73/0.78 [94]~P40(x941)+P10(x941,a32)
% 0.73/0.78 [95]~P42(x951)+P10(x951,a34)
% 0.73/0.78 [96]~P44(x961)+P10(x961,a36)
% 0.73/0.78 [97]~P45(x971)+P10(x971,a37)
% 0.73/0.78 [98]~P18(x981)+P10(x981,a10)
% 0.73/0.78 [99]~P20(x991)+P10(x991,a12)
% 0.73/0.78 [100]~P22(x1001)+P10(x1001,a14)
% 0.73/0.78 [101]~P24(x1011)+P10(x1011,a16)
% 0.73/0.78 [102]~P26(x1021)+P10(x1021,a18)
% 0.73/0.78 [103]~P28(x1031)+P10(x1031,a20)
% 0.73/0.78 [104]~P29(x1041)+P10(x1041,a21)
% 0.73/0.78 [105]~P1(x1051)+P10(x1051,a38)
% 0.73/0.78 [107]~P11(x1071)+P3(x1071,x1071)
% 0.73/0.78 [109]~P5(x1091)+P8(x1091,x1091)
% 0.73/0.78 [111]~P15(x1111)+P9(x1111,x1111)
% 0.73/0.78 [112]P1(x1121)+~P10(x1121,a38)
% 0.73/0.78 [113]P12(x1131)+~P10(x1131,a6)
% 0.73/0.78 [114]P13(x1141)+~P10(x1141,a7)
% 0.73/0.78 [115]P31(x1151)+~P10(x1151,a23)
% 0.73/0.78 [116]P33(x1161)+~P10(x1161,a25)
% 0.73/0.78 [117]P35(x1171)+~P10(x1171,a27)
% 0.73/0.78 [118]P37(x1181)+~P10(x1181,a29)
% 0.73/0.78 [119]P39(x1191)+~P10(x1191,a31)
% 0.73/0.78 [120]P41(x1201)+~P10(x1201,a33)
% 0.73/0.78 [121]P43(x1211)+~P10(x1211,a35)
% 0.73/0.78 [122]P14(x1221)+~P10(x1221,a8)
% 0.73/0.78 [123]P17(x1231)+~P10(x1231,a9)
% 0.73/0.78 [124]P19(x1241)+~P10(x1241,a11)
% 0.73/0.78 [125]P21(x1251)+~P10(x1251,a13)
% 0.73/0.78 [126]P23(x1261)+~P10(x1261,a15)
% 0.73/0.78 [127]P25(x1271)+~P10(x1271,a17)
% 0.73/0.78 [128]P27(x1281)+~P10(x1281,a19)
% 0.73/0.78 [129]P32(x1291)+~P10(x1291,a24)
% 0.73/0.78 [130]P30(x1301)+~P10(x1301,a22)
% 0.73/0.78 [131]P34(x1311)+~P10(x1311,a26)
% 0.73/0.78 [132]P36(x1321)+~P10(x1321,a28)
% 0.73/0.78 [133]P38(x1331)+~P10(x1331,a30)
% 0.73/0.78 [134]P40(x1341)+~P10(x1341,a32)
% 0.73/0.78 [135]P42(x1351)+~P10(x1351,a34)
% 0.73/0.78 [136]P44(x1361)+~P10(x1361,a36)
% 0.73/0.78 [137]P45(x1371)+~P10(x1371,a37)
% 0.73/0.78 [138]P18(x1381)+~P10(x1381,a10)
% 0.73/0.78 [139]P20(x1391)+~P10(x1391,a12)
% 0.73/0.78 [140]P22(x1401)+~P10(x1401,a14)
% 0.73/0.78 [141]P24(x1411)+~P10(x1411,a16)
% 0.73/0.78 [142]P26(x1421)+~P10(x1421,a18)
% 0.73/0.78 [143]P28(x1431)+~P10(x1431,a20)
% 0.73/0.78 [144]P29(x1441)+~P10(x1441,a21)
% 0.73/0.78 [146]P15(x1461)+~P9(x1462,x1461)
% 0.73/0.78 [148]P15(x1481)+~P9(x1481,x1482)
% 0.73/0.78 [149]P6(x1491)+~P7(x1492,x1491)
% 0.73/0.78 [150]P6(x1501)+~P7(x1501,x1502)
% 0.73/0.78 [152]P5(x1521)+~P8(x1522,x1521)
% 0.73/0.78 [153]P5(x1531)+~P4(x1532,x1531)
% 0.73/0.78 [155]P5(x1551)+~P10(x1552,x1551)
% 0.73/0.78 [157]P5(x1571)+~P8(x1571,x1572)
% 0.73/0.78 [158]P5(x1581)+~P4(x1581,x1582)
% 0.73/0.78 [160]P16(x1601)+~P10(x1601,x1602)
% 0.73/0.78 [162]P11(x1621)+~P3(x1622,x1621)
% 0.73/0.78 [164]P11(x1641)+~P3(x1641,x1642)
% 0.73/0.78 [166]~P4(x1662,x1661)+P4(x1661,x1662)
% 0.73/0.78 [165]~P3(x1652,x1651)+P2(x1651)+~P2(x1652)
% 0.73/0.78 [167]~P3(x1671,x1673)+P3(x1671,x1672)+~P3(x1673,x1672)
% 0.73/0.78 [170]~P8(x1701,x1703)+P8(x1701,x1702)+~P8(x1703,x1702)
% 0.73/0.78 [171]~P4(x1713,x1712)+P4(x1711,x1712)+~P8(x1711,x1713)
% 0.73/0.78 [172]~P4(x1721,x1723)+P4(x1721,x1722)+~P8(x1722,x1723)
% 0.73/0.78 [173]~P10(x1731,x1733)+P10(x1731,x1732)+~P8(x1733,x1732)
% 0.73/0.78 [174]~P9(x1741,x1743)+P7(x1741,x1742)+~P7(x1743,x1742)
% 0.73/0.78 [175]~P9(x1753,x1752)+P7(x1751,x1752)+~P7(x1751,x1753)
% 0.73/0.78 [176]~P7(x1761,x1763)+P9(x1761,x1762)+~P7(x1763,x1762)
% 0.73/0.78 [177]~P9(x1771,x1773)+P9(x1771,x1772)+~P9(x1773,x1772)
% 0.73/0.78 [178]~P10(x1783,x1781)+~P4(x1781,x1782)+~P10(x1783,x1782)
% 0.73/0.78 %EqnAxiom
% 0.73/0.78
% 0.73/0.78 %-------------------------------------------
% 0.73/0.78 cnf(179,plain,
% 0.73/0.78 (~P4(a21,a19)),
% 0.73/0.78 inference(scs_inference,[],[41,166])).
% 0.73/0.78 cnf(181,plain,
% 0.73/0.78 (P4(a6,a22)),
% 0.73/0.78 inference(scs_inference,[],[41,10,40,166,171])).
% 0.73/0.78 cnf(183,plain,
% 0.73/0.78 (~P4(a21,a17)),
% 0.73/0.78 inference(scs_inference,[],[41,10,24,40,166,171,172])).
% 0.73/0.78 cnf(185,plain,
% 0.73/0.78 (P3(a40,a2)),
% 0.73/0.78 inference(scs_inference,[],[41,5,9,10,24,40,166,171,172,167])).
% 0.73/0.78 cnf(187,plain,
% 0.73/0.78 (P8(a23,a7)),
% 0.73/0.78 inference(scs_inference,[],[41,5,9,10,11,24,40,166,171,172,167,170])).
% 0.73/0.78 cnf(195,plain,
% 0.73/0.78 (~P4(a21,a15)),
% 0.73/0.78 inference(scs_inference,[],[183,23,166,172])).
% 0.73/0.78 cnf(197,plain,
% 0.73/0.78 (~P4(a15,a21)),
% 0.73/0.78 inference(scs_inference,[],[183,23,166,172,171])).
% 0.73/0.78 cnf(199,plain,
% 0.73/0.78 (P3(a4,a39)),
% 0.73/0.78 inference(scs_inference,[],[183,5,6,23,166,172,171,167])).
% 0.73/0.78 cnf(201,plain,
% 0.73/0.78 (P8(a27,a23)),
% 0.73/0.78 inference(scs_inference,[],[183,5,6,12,13,23,166,172,171,167,170])).
% 0.73/0.78 cnf(231,plain,
% 0.73/0.78 (~P4(a13,a21)),
% 0.73/0.78 inference(scs_inference,[],[197,22,171])).
% 0.73/0.78 cnf(233,plain,
% 0.73/0.78 (~P4(a21,a13)),
% 0.73/0.78 inference(scs_inference,[],[195,197,22,171,172])).
% 0.73/0.78 cnf(235,plain,
% 0.73/0.78 (P3(a5,a2)),
% 0.73/0.78 inference(scs_inference,[],[195,197,185,8,22,171,172,167])).
% 0.73/0.78 cnf(237,plain,
% 0.73/0.78 (P8(a31,a27)),
% 0.73/0.78 inference(scs_inference,[],[195,197,185,8,14,15,22,171,172,167,170])).
% 0.73/0.78 cnf(245,plain,
% 0.73/0.78 (~P4(a11,a21)),
% 0.73/0.78 inference(scs_inference,[],[231,21,171])).
% 0.73/0.78 cnf(247,plain,
% 0.73/0.78 (~P4(a21,a11)),
% 0.73/0.78 inference(scs_inference,[],[231,233,21,171,172])).
% 0.73/0.78 cnf(249,plain,
% 0.73/0.78 (P3(a40,a39)),
% 0.73/0.78 inference(scs_inference,[],[231,233,21,199,9,171,172,167])).
% 0.73/0.78 cnf(251,plain,
% 0.73/0.78 (P8(a35,a31)),
% 0.73/0.78 inference(scs_inference,[],[231,233,16,17,21,199,9,171,172,167,170])).
% 0.73/0.78 cnf(263,plain,
% 0.73/0.78 (~P4(a21,a9)),
% 0.73/0.78 inference(scs_inference,[],[245,247,7,20,235,167,171,172])).
% 0.73/0.78 cnf(265,plain,
% 0.73/0.78 (P8(a9,a35)),
% 0.73/0.78 inference(scs_inference,[],[245,247,7,18,19,20,235,167,171,172,170])).
% 0.73/0.78 cnf(275,plain,
% 0.73/0.78 (P3(a5,a39)),
% 0.73/0.78 inference(scs_inference,[],[249,8,167])).
% 0.73/0.78 cnf(277,plain,
% 0.73/0.78 (P4(a6,a24)),
% 0.73/0.78 inference(scs_inference,[],[181,25,249,8,167,172])).
% 0.73/0.78 cnf(279,plain,
% 0.73/0.78 (~P4(a20,a19)),
% 0.73/0.78 inference(scs_inference,[],[179,181,25,39,249,8,167,172,171])).
% 0.73/0.78 cnf(281,plain,
% 0.73/0.78 (P8(a26,a22)),
% 0.73/0.78 inference(scs_inference,[],[179,181,25,26,39,249,8,167,172,171,170])).
% 0.73/0.78 cnf(283,plain,
% 0.73/0.78 (~P4(a19,a20)),
% 0.73/0.78 inference(scs_inference,[],[179,181,25,26,39,249,8,167,172,171,170,166])).
% 0.73/0.78 cnf(317,plain,
% 0.73/0.78 (~P4(a18,a19)),
% 0.73/0.78 inference(scs_inference,[],[279,38,171])).
% 0.73/0.78 cnf(321,plain,
% 0.73/0.78 (~P4(a19,a18)),
% 0.73/0.78 inference(scs_inference,[],[279,283,38,275,7,171,167,172])).
% 0.73/0.78 cnf(323,plain,
% 0.73/0.78 (P8(a30,a26)),
% 0.73/0.78 inference(scs_inference,[],[279,283,27,28,38,275,7,171,167,172,170])).
% 0.73/0.78 cnf(331,plain,
% 0.73/0.78 (~P4(a19,a16)),
% 0.73/0.78 inference(scs_inference,[],[321,37,172])).
% 0.73/0.78 cnf(333,plain,
% 0.73/0.78 (~P4(a16,a19)),
% 0.73/0.78 inference(scs_inference,[],[317,321,37,172,171])).
% 0.73/0.78 cnf(335,plain,
% 0.73/0.78 (P3(a3,a40)),
% 0.73/0.78 inference(scs_inference,[],[317,321,37,7,8,172,171,167])).
% 0.73/0.78 cnf(337,plain,
% 0.73/0.78 (P8(a34,a30)),
% 0.73/0.78 inference(scs_inference,[],[317,321,29,30,37,7,8,172,171,167,170])).
% 0.73/0.78 cnf(347,plain,
% 0.73/0.78 (~P4(a19,a14)),
% 0.73/0.78 inference(scs_inference,[],[331,36,335,9,167,172])).
% 0.73/0.78 cnf(349,plain,
% 0.73/0.78 (~P4(a14,a19)),
% 0.73/0.78 inference(scs_inference,[],[331,333,36,335,9,167,172,171])).
% 0.73/0.78 cnf(351,plain,
% 0.73/0.78 (P8(a37,a34)),
% 0.73/0.78 inference(scs_inference,[],[331,333,31,32,36,335,9,167,172,171,170])).
% 0.73/0.78 cnf(361,plain,
% 0.73/0.78 (~P4(a12,a19)),
% 0.73/0.78 inference(scs_inference,[],[349,35,171])).
% 0.73/0.78 cnf(365,plain,
% 0.73/0.78 (P8(a12,a37)),
% 0.73/0.78 inference(scs_inference,[],[347,349,33,34,35,171,172,170])).
% 0.73/0.78 cnf(371,plain,
% 0.73/0.78 (P4(a23,a22)),
% 0.73/0.78 inference(scs_inference,[],[187,40,171])).
% 0.73/0.78 cnf(373,plain,
% 0.73/0.78 (~P4(a21,a35)),
% 0.73/0.78 inference(scs_inference,[],[263,187,265,40,171,172])).
% 0.73/0.78 cnf(375,plain,
% 0.73/0.78 (P8(a27,a7)),
% 0.73/0.78 inference(scs_inference,[],[263,187,201,265,40,171,172,170])).
% 0.73/0.78 cnf(377,plain,
% 0.73/0.78 (~P4(a35,a21)),
% 0.73/0.78 inference(scs_inference,[],[263,187,201,265,40,171,172,170,166])).
% 0.73/0.78 cnf(385,plain,
% 0.73/0.78 (~P4(a21,a31)),
% 0.73/0.78 inference(scs_inference,[],[373,377,251,171,172])).
% 0.73/0.78 cnf(387,plain,
% 0.73/0.78 (P8(a35,a27)),
% 0.73/0.78 inference(scs_inference,[],[373,377,237,251,171,172,170])).
% 0.73/0.78 cnf(393,plain,
% 0.73/0.78 (~P4(a37,a19)),
% 0.73/0.78 inference(scs_inference,[],[361,365,171])).
% 0.73/0.78 cnf(397,plain,
% 0.73/0.78 (P8(a30,a22)),
% 0.73/0.78 inference(scs_inference,[],[361,371,281,323,365,171,172,170])).
% 0.73/0.78 cnf(407,plain,
% 0.73/0.78 (P8(a37,a30)),
% 0.73/0.78 inference(scs_inference,[],[393,337,351,171,170])).
% 0.73/0.78 cnf(419,plain,
% 0.73/0.78 (P8(a35,a7)),
% 0.73/0.78 inference(scs_inference,[],[373,375,387,40,171,172,170])).
% 0.73/0.78 cnf(442,plain,
% 0.73/0.78 (P8(a37,a22)),
% 0.73/0.78 inference(scs_inference,[],[393,397,407,171,170])).
% 0.73/0.78 cnf(458,plain,
% 0.73/0.78 (P4(a35,a22)),
% 0.73/0.78 inference(scs_inference,[],[373,419,40,172,171])).
% 0.73/0.78 cnf(460,plain,
% 0.73/0.78 (P8(a9,a7)),
% 0.73/0.78 inference(scs_inference,[],[373,419,265,40,172,171,170])).
% 0.73/0.78 cnf(479,plain,
% 0.73/0.78 (P8(a12,a22)),
% 0.73/0.78 inference(scs_inference,[],[458,442,365,172,170])).
% 0.73/0.78 cnf(483,plain,
% 0.73/0.78 (~P4(a19,a22)),
% 0.73/0.78 inference(scs_inference,[],[393,458,442,365,172,170,171,166])).
% 0.73/0.78 cnf(494,plain,
% 0.73/0.78 (P8(a11,a7)),
% 0.73/0.78 inference(scs_inference,[],[181,460,479,20,40,171,172,170])).
% 0.73/0.78 cnf(498,plain,
% 0.73/0.78 (P8(a13,a7)),
% 0.73/0.78 inference(scs_inference,[],[494,21,170])).
% 0.73/0.78 cnf(510,plain,
% 0.73/0.78 (P8(a15,a7)),
% 0.73/0.78 inference(scs_inference,[],[385,498,15,22,172,170])).
% 0.73/0.78 cnf(522,plain,
% 0.73/0.78 (P8(a17,a7)),
% 0.73/0.78 inference(scs_inference,[],[373,510,17,23,40,171,172,170])).
% 0.73/0.78 cnf(533,plain,
% 0.73/0.78 (P8(a19,a7)),
% 0.73/0.78 inference(scs_inference,[],[522,24,170])).
% 0.73/0.78 cnf(547,plain,
% 0.73/0.78 ($false),
% 0.73/0.78 inference(scs_inference,[],[483,277,533,11,26,201,40,172,170,171]),
% 0.73/0.78 ['proof']).
% 0.73/0.78 % SZS output end Proof
% 0.73/0.78 % Total time :0.140000s
%------------------------------------------------------------------------------