%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : CSR061+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 : 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:52 EDT 2024
% Result : Theorem 0.51s 0.57s
% Output : CNFRefutation 0.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.08 % Problem : CSR061+1 : TPTP v8.2.0. Released v3.4.0.
% 0.02/0.08 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.08/0.28 % Computer : n019.cluster.edu
% 0.08/0.28 % Model : x86_64 x86_64
% 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.28 % Memory : 8042.1875MB
% 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.28 % CPULimit : 300
% 0.08/0.28 % WCLimit : 300
% 0.08/0.28 % DateTime : Wed Jun 19 23:07:53 EDT 2024
% 0.08/0.28 % CPUTime :
% 0.13/0.49 start to proof:theBenchmark
% 0.13/0.55 %-------------------------------------------
% 0.13/0.55 % File :CSE---1.7
% 0.13/0.55 % Problem :theBenchmark
% 0.13/0.55 % Transform :cnf
% 0.13/0.55 % Format :tptp:raw
% 0.13/0.55 % Command :java -jar mcs_scs.jar %d %s
% 0.13/0.55
% 0.13/0.55 % Result :Theorem 0.020000s
% 0.13/0.55 % Output :CNFRefutation 0.020000s
% 0.13/0.55 %-------------------------------------------
% 0.13/0.55 %------------------------------------------------------------------------------
% 0.13/0.55 % File : CSR061+1 : TPTP v8.2.0. Released v3.4.0.
% 0.13/0.55 % Domain : Common Sense Reasoning
% 0.13/0.55 % Problem : Autogenerated Cyc Problem CSR061+1
% 0.13/0.55 % Version : Especial.
% 0.13/0.55 % English :
% 0.13/0.55
% 0.13/0.55 % Refs : [RS+] Reagan Smith et al., The Cyc TPTP Challenge Problem
% 0.13/0.55 % Source : [RS+]
% 0.13/0.55 % Names :
% 0.13/0.55
% 0.13/0.55 % Status : Theorem
% 0.13/0.55 % 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.1, 0.05 v3.7.0, 0.00 v3.4.0
% 0.13/0.55 % Syntax : Number of formulae : 119 ( 23 unt; 0 def)
% 0.13/0.55 % Number of atoms : 228 ( 0 equ)
% 0.13/0.55 % Maximal formula atoms : 3 ( 1 avg)
% 0.13/0.55 % Number of connectives : 111 ( 2 ~; 0 |; 15 &)
% 0.13/0.55 % ( 0 <=>; 94 =>; 0 <=; 0 <~>)
% 0.13/0.55 % Maximal formula depth : 7 ( 3 avg)
% 0.13/0.55 % Maximal term depth : 1 ( 1 avg)
% 0.13/0.55 % Number of predicates : 31 ( 31 usr; 0 prp; 1-2 aty)
% 0.13/0.55 % Number of functors : 24 ( 24 usr; 24 con; 0-0 aty)
% 0.13/0.55 % Number of variables : 141 ( 141 !; 0 ?)
% 0.13/0.55 % SPC : FOF_THM_EPR_NEQ
% 0.13/0.55
% 0.13/0.55 % Comments : Autogenerated from the OpenCyc KB. Documentation can be found at
% 0.13/0.55 % http://opencyc.org/doc/#TPTP_Challenge_Problem_Set
% 0.13/0.55 % : Cyc(R) Knowledge Base Copyright(C) 1995-2007 Cycorp, Inc., Austin,
% 0.13/0.55 % TX, USA. All rights reserved.
% 0.13/0.55 % : OpenCyc Knowledge Base Copyright(C) 2001-2007 Cycorp, Inc.,
% 0.13/0.55 % Austin, TX, USA. All rights reserved.
% 0.13/0.55 %------------------------------------------------------------------------------
% 0.13/0.55 %$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.13/0.55 %$static(cyc_scaling_1,include('Axioms/CSR002+0.ax'))
% 0.13/0.55 %----Empty file include('Axioms/CSR002+0.ax').
% 0.13/0.55 %------------------------------------------------------------------------------
% 0.13/0.55 % Cyc Assertion #1322220:
% 0.13/0.55 fof(just1,axiom,
% 0.13/0.55 transitivebinarypredicate(c_genlmt) ).
% 0.13/0.55
% 0.13/0.55 % Cyc Assertion #1462275:
% 0.13/0.55 fof(just2,axiom,
% 0.13/0.55 genlmt(c_generictemporalmt,c_basekb) ).
% 0.13/0.55
% 0.13/0.55 % Cyc Assertion #1473451:
% 0.13/0.55 fof(just3,axiom,
% 0.13/0.55 genlmt(c_timehasnoendmt,c_generictemporalmt) ).
% 0.13/0.55
% 0.13/0.55 % Cyc Assertion #1650755:
% 0.13/0.55 fof(just4,axiom,
% 0.13/0.55 genlmt(c_basekb,c_universalvocabularymt) ).
% 0.13/0.55
% 0.13/0.55 % Cyc Assertion #2088991:
% 0.13/0.55 fof(just5,axiom,
% 0.13/0.55 genls(c_tptpcol_4_106497,c_tptpcol_3_98305) ).
% 0.13/0.55
% 0.13/0.55 fof(just6,axiom,
% 0.13/0.55 ! [OBJ] :
% 0.13/0.55 ( tptpcol_4_106497(OBJ)
% 0.13/0.55 => tptpcol_3_98305(OBJ) ) ).
% 0.13/0.55
% 0.13/0.55 % Cyc Assertion #2099230:
% 0.13/0.55 fof(just7,axiom,
% 0.13/0.55 genls(c_tptpcol_5_110593,c_tptpcol_4_106497) ).
% 0.13/0.55
% 0.13/0.55 fof(just8,axiom,
% 0.13/0.55 ! [OBJ] :
% 0.13/0.55 ( tptpcol_5_110593(OBJ)
% 0.13/0.55 => tptpcol_4_106497(OBJ) ) ).
% 0.13/0.55
% 0.13/0.55 % Cyc Assertion #2104349:
% 0.13/0.55 fof(just9,axiom,
% 0.13/0.55 genls(c_tptpcol_6_112641,c_tptpcol_5_110593) ).
% 0.13/0.55
% 0.13/0.55 fof(just10,axiom,
% 0.13/0.55 ! [OBJ] :
% 0.13/0.55 ( tptpcol_6_112641(OBJ)
% 0.13/0.55 => tptpcol_5_110593(OBJ) ) ).
% 0.13/0.55
% 0.13/0.55 % Cyc Assertion #2106908:
% 0.13/0.55 fof(just11,axiom,
% 0.13/0.55 genls(c_tptpcol_7_113665,c_tptpcol_6_112641) ).
% 0.13/0.55
% 0.13/0.55 fof(just12,axiom,
% 0.13/0.55 ! [OBJ] :
% 0.13/0.55 ( tptpcol_7_113665(OBJ)
% 0.13/0.55 => tptpcol_6_112641(OBJ) ) ).
% 0.13/0.55
% 0.13/0.55 % Cyc Assertion #2108187:
% 0.13/0.55 fof(just13,axiom,
% 0.13/0.55 genls(c_tptpcol_8_114177,c_tptpcol_7_113665) ).
% 0.13/0.55
% 0.13/0.55 fof(just14,axiom,
% 0.13/0.55 ! [OBJ] :
% 0.13/0.55 ( tptpcol_8_114177(OBJ)
% 0.13/0.55 => tptpcol_7_113665(OBJ) ) ).
% 0.13/0.55
% 0.13/0.55 % Cyc Assertion #2109471:
% 0.13/0.55 fof(just15,axiom,
% 0.13/0.55 genls(c_tptpcol_4_114689,c_tptpcol_3_114688) ).
% 0.13/0.55
% 0.13/0.55 fof(just16,axiom,
% 0.13/0.55 ! [OBJ] :
% 0.13/0.55 ( tptpcol_4_114689(OBJ)
% 0.13/0.55 => tptpcol_3_114688(OBJ) ) ).
% 0.13/0.55
% 0.13/0.55 % Cyc Assertion #2109473:
% 0.13/0.55 fof(just17,axiom,
% 0.13/0.55 genls(c_tptpcol_5_114690,c_tptpcol_4_114689) ).
% 0.13/0.55
% 0.13/0.55 fof(just18,axiom,
% 0.13/0.55 ! [OBJ] :
% 0.13/0.55 ( tptpcol_5_114690(OBJ)
% 0.13/0.55 => tptpcol_4_114689(OBJ) ) ).
% 0.13/0.55
% 0.13/0.55 % Cyc Assertion #2114592:
% 0.13/0.55 fof(just19,axiom,
% 0.13/0.55 genls(c_tptpcol_6_116738,c_tptpcol_5_114690) ).
% 0.13/0.55
% 0.13/0.55 fof(just20,axiom,
% 0.13/0.55 ! [OBJ] :
% 0.13/0.55 ( tptpcol_6_116738(OBJ)
% 0.13/0.55 => tptpcol_5_114690(OBJ) ) ).
% 0.13/0.55
% 0.13/0.55 % Cyc Assertion #2117151:
% 0.13/0.55 fof(just21,axiom,
% 0.13/0.55 genls(c_tptpcol_7_117762,c_tptpcol_6_116738) ).
% 0.13/0.55
% 0.13/0.55 fof(just22,axiom,
% 0.13/0.55 ! [OBJ] :
% 0.13/0.55 ( tptpcol_7_117762(OBJ)
% 0.13/0.55 => tptpcol_6_116738(OBJ) ) ).
% 0.13/0.55
% 0.13/0.55 % Cyc Assertion #2117153:
% 0.13/0.55 fof(just23,axiom,
% 0.13/0.55 genls(c_tptpcol_8_117763,c_tptpcol_7_117762) ).
% 0.13/0.55
% 0.13/0.55 fof(just24,axiom,
% 0.13/0.55 ! [OBJ] :
% 0.13/0.55 ( tptpcol_8_117763(OBJ)
% 0.13/0.55 => tptpcol_7_117762(OBJ) ) ).
% 0.13/0.55
% 0.13/0.55 % Cyc Assertion #2117792:
% 0.13/0.55 fof(just25,axiom,
% 0.13/0.55 genls(c_tptpcol_9_118019,c_tptpcol_8_117763) ).
% 0.13/0.55
% 0.13/0.55 fof(just26,axiom,
% 0.13/0.55 ! [OBJ] :
% 0.13/0.55 ( tptpcol_9_118019(OBJ)
% 0.13/0.55 => tptpcol_8_117763(OBJ) ) ).
% 0.13/0.55
% 0.13/0.55 % Cyc Assertion #2117794:
% 0.13/0.55 fof(just27,axiom,
% 0.13/0.55 genls(c_tptpcol_10_118020,c_tptpcol_9_118019) ).
% 0.13/0.55
% 0.13/0.55 fof(just28,axiom,
% 0.13/0.55 ! [OBJ] :
% 0.13/0.55 ( tptpcol_10_118020(OBJ)
% 0.13/0.55 => tptpcol_9_118019(OBJ) ) ).
% 0.13/0.55
% 0.13/0.55 % Cyc Assertion #2117953:
% 0.13/0.55 fof(just29,axiom,
% 0.13/0.55 genls(c_tptpcol_11_118084,c_tptpcol_10_118020) ).
% 0.13/0.55
% 0.13/0.55 fof(just30,axiom,
% 0.13/0.55 ! [OBJ] :
% 0.13/0.55 ( tptpcol_11_118084(OBJ)
% 0.13/0.55 => tptpcol_10_118020(OBJ) ) ).
% 0.13/0.55
% 0.13/0.55 % Cyc Assertion #2118032:
% 0.13/0.55 fof(just31,axiom,
% 0.13/0.55 genls(c_tptpcol_12_118116,c_tptpcol_11_118084) ).
% 0.13/0.55
% 0.13/0.55 fof(just32,axiom,
% 0.13/0.55 ! [OBJ] :
% 0.13/0.55 ( tptpcol_12_118116(OBJ)
% 0.13/0.55 => tptpcol_11_118084(OBJ) ) ).
% 0.13/0.55
% 0.13/0.55 % Cyc Assertion #2118034:
% 0.13/0.55 fof(just33,axiom,
% 0.13/0.55 genls(c_tptpcol_13_118117,c_tptpcol_12_118116) ).
% 0.13/0.55
% 0.13/0.55 fof(just34,axiom,
% 0.13/0.55 ! [OBJ] :
% 0.13/0.55 ( tptpcol_13_118117(OBJ)
% 0.13/0.55 => tptpcol_12_118116(OBJ) ) ).
% 0.13/0.55
% 0.13/0.55 % Cyc Assertion #2118036:
% 0.13/0.55 fof(just35,axiom,
% 0.13/0.55 genls(c_tptpcol_14_118118,c_tptpcol_13_118117) ).
% 0.13/0.55
% 0.13/0.55 fof(just36,axiom,
% 0.13/0.55 ! [OBJ] :
% 0.13/0.55 ( tptpcol_14_118118(OBJ)
% 0.13/0.55 => tptpcol_13_118117(OBJ) ) ).
% 0.13/0.55
% 0.13/0.55 % Cyc Assertion #2150425:
% 0.13/0.55 fof(just37,axiom,
% 0.13/0.55 disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688) ).
% 0.13/0.55
% 0.13/0.55 fof(just38,axiom,
% 0.13/0.55 ! [OBJ] :
% 0.13/0.55 ~ ( tptpcol_3_98305(OBJ)
% 0.13/0.55 & tptpcol_3_114688(OBJ) ) ).
% 0.13/0.55
% 0.13/0.55 % Cyc Assertion #398814:
% 0.13/0.55 fof(just39,axiom,
% 0.13/0.55 ! [OBJ,COL1,COL2] :
% 0.13/0.55 ~ ( isa(OBJ,COL1)
% 0.13/0.55 & isa(OBJ,COL2)
% 0.13/0.55 & disjointwith(COL1,COL2) ) ).
% 0.13/0.55
% 0.13/0.55 % Cyc Assertion #831913:
% 0.13/0.55 fof(just40,axiom,
% 0.13/0.55 ! [SPECPRED,PRED,GENLPRED] :
% 0.13/0.55 ( ( genlinverse(SPECPRED,PRED)
% 0.13/0.55 & genlinverse(PRED,GENLPRED) )
% 0.13/0.55 => genlpreds(SPECPRED,GENLPRED) ) ).
% 0.13/0.55
% 0.13/0.55 % Cyc Constant #40273:
% 0.13/0.55 fof(just41,axiom,
% 0.13/0.55 ! [ARG1,INS] :
% 0.13/0.55 ( genlpreds(ARG1,INS)
% 0.13/0.55 => predicate(INS) ) ).
% 0.13/0.55
% 0.13/0.55 fof(just42,axiom,
% 0.13/0.55 ! [ARG1,INS] :
% 0.13/0.55 ( genlpreds(ARG1,INS)
% 0.13/0.55 => predicate(INS) ) ).
% 0.13/0.55
% 0.13/0.55 fof(just43,axiom,
% 0.13/0.55 ! [INS,ARG2] :
% 0.13/0.55 ( genlpreds(INS,ARG2)
% 0.13/0.55 => predicate(INS) ) ).
% 0.13/0.55
% 0.13/0.55 fof(just44,axiom,
% 0.13/0.55 ! [INS,ARG2] :
% 0.13/0.56 ( genlpreds(INS,ARG2)
% 0.13/0.56 => predicate(INS) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just45,axiom,
% 0.13/0.56 ! [X,Y,Z] :
% 0.13/0.56 ( ( genlpreds(X,Y)
% 0.13/0.56 & genlpreds(Y,Z) )
% 0.13/0.56 => genlpreds(X,Z) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just46,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( predicate(X)
% 0.13/0.56 => genlpreds(X,X) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just47,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( predicate(X)
% 0.13/0.56 => genlpreds(X,X) ) ).
% 0.13/0.56
% 0.13/0.56 % Cyc Constant #45259:
% 0.13/0.56 fof(just48,axiom,
% 0.13/0.56 ! [ARG1,INS] :
% 0.13/0.56 ( genlinverse(ARG1,INS)
% 0.13/0.56 => binarypredicate(INS) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just49,axiom,
% 0.13/0.56 ! [INS,ARG2] :
% 0.13/0.56 ( genlinverse(INS,ARG2)
% 0.13/0.56 => binarypredicate(INS) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just50,axiom,
% 0.13/0.56 ! [OLD,ARG2,NEW] :
% 0.13/0.56 ( ( genlinverse(OLD,ARG2)
% 0.13/0.56 & genlpreds(NEW,OLD) )
% 0.13/0.56 => genlinverse(NEW,ARG2) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just51,axiom,
% 0.13/0.56 ! [ARG1,OLD,NEW] :
% 0.13/0.56 ( ( genlinverse(ARG1,OLD)
% 0.13/0.56 & genlpreds(OLD,NEW) )
% 0.13/0.56 => genlinverse(ARG1,NEW) ) ).
% 0.13/0.56
% 0.13/0.56 % Cyc Constant #78648:
% 0.13/0.56 fof(just52,axiom,
% 0.13/0.56 ! [ARG1,INS] :
% 0.13/0.56 ( disjointwith(ARG1,INS)
% 0.13/0.56 => collection(INS) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just53,axiom,
% 0.13/0.56 ! [INS,ARG2] :
% 0.13/0.56 ( disjointwith(INS,ARG2)
% 0.13/0.56 => collection(INS) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just54,axiom,
% 0.13/0.56 ! [X,Y] :
% 0.13/0.56 ( disjointwith(X,Y)
% 0.13/0.56 => disjointwith(Y,X) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just55,axiom,
% 0.13/0.56 ! [ARG1,OLD,NEW] :
% 0.13/0.56 ( ( disjointwith(ARG1,OLD)
% 0.13/0.56 & genls(NEW,OLD) )
% 0.13/0.56 => disjointwith(ARG1,NEW) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just56,axiom,
% 0.13/0.56 ! [OLD,ARG2,NEW] :
% 0.13/0.56 ( ( disjointwith(OLD,ARG2)
% 0.13/0.56 & genls(NEW,OLD) )
% 0.13/0.56 => disjointwith(NEW,ARG2) ) ).
% 0.13/0.56
% 0.13/0.56 % Cyc Constant #247715:
% 0.13/0.56 fof(just57,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( isa(X,c_tptpcol_14_118118)
% 0.13/0.56 => tptpcol_14_118118(X) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just58,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( tptpcol_14_118118(X)
% 0.13/0.56 => isa(X,c_tptpcol_14_118118) ) ).
% 0.13/0.56
% 0.13/0.56 % Cyc Constant #247714:
% 0.13/0.56 fof(just59,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( isa(X,c_tptpcol_13_118117)
% 0.13/0.56 => tptpcol_13_118117(X) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just60,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( tptpcol_13_118117(X)
% 0.13/0.56 => isa(X,c_tptpcol_13_118117) ) ).
% 0.13/0.56
% 0.13/0.56 % Cyc Constant #247713:
% 0.13/0.56 fof(just61,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( isa(X,c_tptpcol_12_118116)
% 0.13/0.56 => tptpcol_12_118116(X) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just62,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( tptpcol_12_118116(X)
% 0.13/0.56 => isa(X,c_tptpcol_12_118116) ) ).
% 0.13/0.56
% 0.13/0.56 % Cyc Constant #247681:
% 0.13/0.56 fof(just63,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( isa(X,c_tptpcol_11_118084)
% 0.13/0.56 => tptpcol_11_118084(X) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just64,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( tptpcol_11_118084(X)
% 0.13/0.56 => isa(X,c_tptpcol_11_118084) ) ).
% 0.13/0.56
% 0.13/0.56 % Cyc Constant #247617:
% 0.13/0.56 fof(just65,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( isa(X,c_tptpcol_10_118020)
% 0.13/0.56 => tptpcol_10_118020(X) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just66,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( tptpcol_10_118020(X)
% 0.13/0.56 => isa(X,c_tptpcol_10_118020) ) ).
% 0.13/0.56
% 0.13/0.56 % Cyc Constant #247616:
% 0.13/0.56 fof(just67,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( isa(X,c_tptpcol_9_118019)
% 0.13/0.56 => tptpcol_9_118019(X) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just68,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( tptpcol_9_118019(X)
% 0.13/0.56 => isa(X,c_tptpcol_9_118019) ) ).
% 0.13/0.56
% 0.13/0.56 % Cyc Constant #247360:
% 0.13/0.56 fof(just69,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( isa(X,c_tptpcol_8_117763)
% 0.13/0.56 => tptpcol_8_117763(X) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just70,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( tptpcol_8_117763(X)
% 0.13/0.56 => isa(X,c_tptpcol_8_117763) ) ).
% 0.13/0.56
% 0.13/0.56 % Cyc Constant #247359:
% 0.13/0.56 fof(just71,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( isa(X,c_tptpcol_7_117762)
% 0.13/0.56 => tptpcol_7_117762(X) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just72,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( tptpcol_7_117762(X)
% 0.13/0.56 => isa(X,c_tptpcol_7_117762) ) ).
% 0.13/0.56
% 0.13/0.56 % Cyc Constant #246335:
% 0.13/0.56 fof(just73,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( isa(X,c_tptpcol_6_116738)
% 0.13/0.56 => tptpcol_6_116738(X) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just74,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( tptpcol_6_116738(X)
% 0.13/0.56 => isa(X,c_tptpcol_6_116738) ) ).
% 0.13/0.56
% 0.13/0.56 % Cyc Constant #244287:
% 0.13/0.56 fof(just75,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( isa(X,c_tptpcol_5_114690)
% 0.13/0.56 => tptpcol_5_114690(X) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just76,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( tptpcol_5_114690(X)
% 0.13/0.56 => isa(X,c_tptpcol_5_114690) ) ).
% 0.13/0.56
% 0.13/0.56 % Cyc Constant #244285:
% 0.13/0.56 fof(just77,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( isa(X,c_tptpcol_3_114688)
% 0.13/0.56 => tptpcol_3_114688(X) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just78,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( tptpcol_3_114688(X)
% 0.13/0.56 => isa(X,c_tptpcol_3_114688) ) ).
% 0.13/0.56
% 0.13/0.56 % Cyc Constant #244286:
% 0.13/0.56 fof(just79,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( isa(X,c_tptpcol_4_114689)
% 0.13/0.56 => tptpcol_4_114689(X) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just80,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( tptpcol_4_114689(X)
% 0.13/0.56 => isa(X,c_tptpcol_4_114689) ) ).
% 0.13/0.56
% 0.13/0.56 % Cyc Constant #243774:
% 0.13/0.56 fof(just81,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( isa(X,c_tptpcol_8_114177)
% 0.13/0.56 => tptpcol_8_114177(X) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just82,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( tptpcol_8_114177(X)
% 0.13/0.56 => isa(X,c_tptpcol_8_114177) ) ).
% 0.13/0.56
% 0.13/0.56 % Cyc Constant #243262:
% 0.13/0.56 fof(just83,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( isa(X,c_tptpcol_7_113665)
% 0.13/0.56 => tptpcol_7_113665(X) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just84,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( tptpcol_7_113665(X)
% 0.13/0.56 => isa(X,c_tptpcol_7_113665) ) ).
% 0.13/0.56
% 0.13/0.56 % Cyc Constant #242238:
% 0.13/0.56 fof(just85,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( isa(X,c_tptpcol_6_112641)
% 0.13/0.56 => tptpcol_6_112641(X) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just86,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( tptpcol_6_112641(X)
% 0.13/0.56 => isa(X,c_tptpcol_6_112641) ) ).
% 0.13/0.56
% 0.13/0.56 % Cyc Constant #240190:
% 0.13/0.56 fof(just87,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( isa(X,c_tptpcol_5_110593)
% 0.13/0.56 => tptpcol_5_110593(X) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just88,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( tptpcol_5_110593(X)
% 0.13/0.56 => isa(X,c_tptpcol_5_110593) ) ).
% 0.13/0.56
% 0.13/0.56 % Cyc Constant #227902:
% 0.13/0.56 fof(just89,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( isa(X,c_tptpcol_3_98305)
% 0.13/0.56 => tptpcol_3_98305(X) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just90,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( tptpcol_3_98305(X)
% 0.13/0.56 => isa(X,c_tptpcol_3_98305) ) ).
% 0.13/0.56
% 0.13/0.56 % Cyc Constant #236094:
% 0.13/0.56 fof(just91,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( isa(X,c_tptpcol_4_106497)
% 0.13/0.56 => tptpcol_4_106497(X) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just92,axiom,
% 0.13/0.56 ! [X] :
% 0.13/0.56 ( tptpcol_4_106497(X)
% 0.13/0.56 => isa(X,c_tptpcol_4_106497) ) ).
% 0.13/0.56
% 0.13/0.56 % Cyc Constant #0:
% 0.13/0.56 fof(just93,axiom,
% 0.13/0.56 ! [ARG1,INS] :
% 0.13/0.56 ( genls(ARG1,INS)
% 0.13/0.56 => collection(INS) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just94,axiom,
% 0.13/0.56 ! [ARG1,INS] :
% 0.13/0.56 ( genls(ARG1,INS)
% 0.13/0.56 => collection(INS) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just95,axiom,
% 0.13/0.56 ! [INS,ARG2] :
% 0.13/0.56 ( genls(INS,ARG2)
% 0.13/0.56 => collection(INS) ) ).
% 0.13/0.56
% 0.13/0.56 fof(just96,axiom,
% 0.13/0.56 ! [INS,ARG2] :
% 0.13/0.56 ( genls(INS,ARG2)
% 0.13/0.56 => collection(INS) ) ).
% 0.51/0.56
% 0.51/0.56 fof(just97,axiom,
% 0.51/0.56 ! [X,Y,Z] :
% 0.51/0.56 ( ( genls(X,Y)
% 0.51/0.56 & genls(Y,Z) )
% 0.51/0.56 => genls(X,Z) ) ).
% 0.51/0.56
% 0.51/0.56 fof(just98,axiom,
% 0.51/0.56 ! [X] :
% 0.51/0.56 ( collection(X)
% 0.51/0.56 => genls(X,X) ) ).
% 0.51/0.56
% 0.51/0.56 fof(just99,axiom,
% 0.51/0.56 ! [X] :
% 0.51/0.56 ( collection(X)
% 0.51/0.56 => genls(X,X) ) ).
% 0.51/0.56
% 0.51/0.56 fof(just100,axiom,
% 0.51/0.56 ! [OLD,ARG2,NEW] :
% 0.51/0.56 ( ( genls(OLD,ARG2)
% 0.51/0.56 & genls(NEW,OLD) )
% 0.51/0.56 => genls(NEW,ARG2) ) ).
% 0.51/0.56
% 0.51/0.56 fof(just101,axiom,
% 0.51/0.56 ! [ARG1,OLD,NEW] :
% 0.51/0.56 ( ( genls(ARG1,OLD)
% 0.51/0.56 & genls(OLD,NEW) )
% 0.51/0.56 => genls(ARG1,NEW) ) ).
% 0.51/0.56
% 0.51/0.56 % Cyc Constant #27757:
% 0.51/0.56 fof(just102,axiom,
% 0.51/0.56 mtvisible(c_basekb) ).
% 0.51/0.56
% 0.51/0.56 % Cyc Constant #127156:
% 0.51/0.56 fof(just103,axiom,
% 0.51/0.56 ! [X] :
% 0.51/0.56 ( isa(X,c_transitivebinarypredicate)
% 0.51/0.56 => transitivebinarypredicate(X) ) ).
% 0.51/0.56
% 0.51/0.56 fof(just104,axiom,
% 0.51/0.56 ! [X] :
% 0.51/0.56 ( transitivebinarypredicate(X)
% 0.51/0.56 => isa(X,c_transitivebinarypredicate) ) ).
% 0.51/0.56
% 0.51/0.56 % Cyc Constant #19550:
% 0.51/0.56 fof(just105,axiom,
% 0.51/0.56 ! [SPECMT,GENLMT] :
% 0.51/0.56 ( ( mtvisible(SPECMT)
% 0.51/0.56 & genlmt(SPECMT,GENLMT) )
% 0.51/0.56 => mtvisible(GENLMT) ) ).
% 0.51/0.56
% 0.51/0.56 fof(just106,axiom,
% 0.51/0.56 ! [ARG1,INS] :
% 0.51/0.56 ( genlmt(ARG1,INS)
% 0.51/0.56 => microtheory(INS) ) ).
% 0.51/0.56
% 0.51/0.56 fof(just107,axiom,
% 0.51/0.56 ! [ARG1,INS] :
% 0.51/0.57 ( genlmt(ARG1,INS)
% 0.51/0.57 => microtheory(INS) ) ).
% 0.51/0.57
% 0.51/0.57 fof(just108,axiom,
% 0.51/0.57 ! [INS,ARG2] :
% 0.51/0.57 ( genlmt(INS,ARG2)
% 0.51/0.57 => microtheory(INS) ) ).
% 0.51/0.57
% 0.51/0.57 fof(just109,axiom,
% 0.51/0.57 ! [INS,ARG2] :
% 0.51/0.57 ( genlmt(INS,ARG2)
% 0.51/0.57 => microtheory(INS) ) ).
% 0.51/0.57
% 0.51/0.57 fof(just110,axiom,
% 0.51/0.57 ! [X,Y,Z] :
% 0.51/0.57 ( ( genlmt(X,Y)
% 0.51/0.57 & genlmt(Y,Z) )
% 0.51/0.57 => genlmt(X,Z) ) ).
% 0.51/0.57
% 0.51/0.57 fof(just111,axiom,
% 0.51/0.57 ! [X] :
% 0.51/0.57 ( microtheory(X)
% 0.51/0.57 => genlmt(X,X) ) ).
% 0.51/0.57
% 0.51/0.57 fof(just112,axiom,
% 0.51/0.57 ! [X] :
% 0.51/0.57 ( microtheory(X)
% 0.51/0.57 => genlmt(X,X) ) ).
% 0.51/0.57
% 0.51/0.57 % Cyc Constant #72115:
% 0.51/0.57 fof(just113,axiom,
% 0.51/0.57 ! [ARG1,INS] :
% 0.51/0.57 ( isa(ARG1,INS)
% 0.51/0.57 => collection(INS) ) ).
% 0.51/0.57
% 0.51/0.57 fof(just114,axiom,
% 0.51/0.57 ! [ARG1,INS] :
% 0.51/0.57 ( isa(ARG1,INS)
% 0.51/0.57 => collection(INS) ) ).
% 0.51/0.57
% 0.51/0.57 fof(just115,axiom,
% 0.51/0.57 ! [INS,ARG2] :
% 0.51/0.57 ( isa(INS,ARG2)
% 0.51/0.57 => thing(INS) ) ).
% 0.51/0.57
% 0.51/0.57 fof(just116,axiom,
% 0.51/0.57 ! [INS,ARG2] :
% 0.51/0.57 ( isa(INS,ARG2)
% 0.51/0.57 => thing(INS) ) ).
% 0.51/0.57
% 0.51/0.57 fof(just117,axiom,
% 0.51/0.57 ! [ARG1,OLD,NEW] :
% 0.51/0.57 ( ( isa(ARG1,OLD)
% 0.51/0.57 & genls(OLD,NEW) )
% 0.51/0.57 => isa(ARG1,NEW) ) ).
% 0.51/0.57
% 0.51/0.57 % Cyc Constant #95028:
% 0.51/0.57 fof(just118,axiom,
% 0.51/0.57 mtvisible(c_universalvocabularymt) ).
% 0.51/0.57
% 0.51/0.57 fof(query61,conjecture,
% 0.51/0.57 ( mtvisible(c_timehasnoendmt)
% 0.51/0.57 => disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) ) ).
% 0.51/0.57
% 0.51/0.57 %------------------------------------------------------------------------------
% 0.51/0.57 %-------------------------------------------
% 0.51/0.57 % Proof found
% 0.51/0.57 % SZS status Theorem for theBenchmark
% 0.51/0.57 % SZS output start Proof
% 0.51/0.57 %ClaNum:120(EqnAxiom:0)
% 0.51/0.57 %VarNum:223(SingletonVarNum:116)
% 0.51/0.57 %MaxLitNum:3
% 0.51/0.57 %MaxfuncDepth:0
% 0.51/0.57 %SharedTerms:49
% 0.51/0.57 %goalClause: 3 25
% 0.51/0.57 %singleGoalClaCount:2
% 0.51/0.57 [1]P1(a1)
% 0.51/0.57 [2]P2(a2)
% 0.51/0.57 [3]P2(a4)
% 0.51/0.57 [4]P2(a5)
% 0.51/0.57 [5]P3(a3,a2)
% 0.51/0.57 [6]P3(a2,a5)
% 0.51/0.57 [7]P3(a4,a3)
% 0.51/0.57 [8]P8(a6,a7)
% 0.51/0.57 [9]P8(a14,a6)
% 0.51/0.57 [10]P8(a16,a14)
% 0.51/0.57 [11]P8(a18,a16)
% 0.51/0.57 [12]P8(a20,a18)
% 0.51/0.57 [13]P8(a15,a8)
% 0.51/0.57 [14]P8(a17,a15)
% 0.51/0.57 [15]P8(a19,a17)
% 0.51/0.57 [16]P8(a21,a19)
% 0.51/0.57 [17]P8(a22,a21)
% 0.51/0.57 [18]P8(a23,a22)
% 0.51/0.57 [19]P8(a9,a23)
% 0.51/0.57 [20]P8(a10,a9)
% 0.51/0.57 [21]P8(a11,a10)
% 0.51/0.57 [22]P8(a12,a11)
% 0.51/0.57 [23]P8(a13,a12)
% 0.51/0.57 [24]P4(a7,a8)
% 0.51/0.57 [25]~P4(a20,a13)
% 0.51/0.57 [26]~P22(x261)+P12(x261)
% 0.51/0.57 [27]~P12(x271)+P13(x271)
% 0.51/0.57 [28]~P24(x281)+P22(x281)
% 0.51/0.57 [29]~P26(x291)+P24(x291)
% 0.51/0.57 [30]~P28(x301)+P26(x301)
% 0.51/0.57 [31]~P25(x311)+P23(x311)
% 0.51/0.57 [32]~P23(x321)+P14(x321)
% 0.51/0.57 [33]~P27(x331)+P25(x331)
% 0.51/0.57 [34]~P29(x341)+P27(x341)
% 0.51/0.57 [35]~P30(x351)+P29(x351)
% 0.51/0.57 [36]~P31(x361)+P30(x361)
% 0.51/0.57 [37]~P15(x371)+P31(x371)
% 0.51/0.57 [38]~P18(x381)+P15(x381)
% 0.51/0.57 [39]~P19(x391)+P18(x391)
% 0.51/0.57 [40]~P20(x401)+P19(x401)
% 0.51/0.57 [41]~P21(x411)+P20(x411)
% 0.51/0.57 [42]~P14(x421)+~P13(x421)
% 0.51/0.57 [43]~P12(x431)+P10(x431,a6)
% 0.51/0.57 [44]~P13(x441)+P10(x441,a7)
% 0.51/0.57 [45]~P22(x451)+P10(x451,a14)
% 0.51/0.57 [46]~P24(x461)+P10(x461,a16)
% 0.51/0.57 [47]~P26(x471)+P10(x471,a18)
% 0.51/0.57 [48]~P28(x481)+P10(x481,a20)
% 0.51/0.57 [49]~P23(x491)+P10(x491,a15)
% 0.51/0.57 [50]~P14(x501)+P10(x501,a8)
% 0.51/0.57 [51]~P25(x511)+P10(x511,a17)
% 0.51/0.57 [52]~P27(x521)+P10(x521,a19)
% 0.51/0.57 [53]~P29(x531)+P10(x531,a21)
% 0.51/0.57 [54]~P30(x541)+P10(x541,a22)
% 0.51/0.57 [55]~P31(x551)+P10(x551,a23)
% 0.51/0.57 [56]~P15(x561)+P10(x561,a9)
% 0.51/0.57 [57]~P18(x571)+P10(x571,a10)
% 0.51/0.57 [58]~P19(x581)+P10(x581,a11)
% 0.51/0.57 [59]~P20(x591)+P10(x591,a12)
% 0.51/0.57 [60]~P21(x601)+P10(x601,a13)
% 0.51/0.57 [61]~P1(x611)+P10(x611,a24)
% 0.51/0.57 [63]~P11(x631)+P3(x631,x631)
% 0.51/0.57 [65]~P5(x651)+P8(x651,x651)
% 0.51/0.57 [67]~P16(x671)+P9(x671,x671)
% 0.51/0.57 [68]P1(x681)+~P10(x681,a24)
% 0.51/0.57 [69]P12(x691)+~P10(x691,a6)
% 0.51/0.57 [70]P13(x701)+~P10(x701,a7)
% 0.51/0.57 [71]P22(x711)+~P10(x711,a14)
% 0.51/0.57 [72]P24(x721)+~P10(x721,a16)
% 0.51/0.57 [73]P26(x731)+~P10(x731,a18)
% 0.51/0.57 [74]P28(x741)+~P10(x741,a20)
% 0.51/0.57 [75]P23(x751)+~P10(x751,a15)
% 0.51/0.57 [76]P14(x761)+~P10(x761,a8)
% 0.51/0.57 [77]P25(x771)+~P10(x771,a17)
% 0.51/0.57 [78]P27(x781)+~P10(x781,a19)
% 0.51/0.57 [79]P29(x791)+~P10(x791,a21)
% 0.51/0.57 [80]P30(x801)+~P10(x801,a22)
% 0.51/0.57 [81]P31(x811)+~P10(x811,a23)
% 0.51/0.57 [82]P15(x821)+~P10(x821,a9)
% 0.51/0.57 [83]P18(x831)+~P10(x831,a10)
% 0.51/0.57 [84]P19(x841)+~P10(x841,a11)
% 0.51/0.57 [85]P20(x851)+~P10(x851,a12)
% 0.51/0.57 [86]P21(x861)+~P10(x861,a13)
% 0.51/0.57 [88]P16(x881)+~P9(x882,x881)
% 0.51/0.57 [90]P16(x901)+~P9(x901,x902)
% 0.51/0.57 [91]P6(x911)+~P7(x912,x911)
% 0.51/0.57 [92]P6(x921)+~P7(x921,x922)
% 0.51/0.57 [94]P5(x941)+~P8(x942,x941)
% 0.51/0.57 [95]P5(x951)+~P4(x952,x951)
% 0.51/0.57 [97]P5(x971)+~P10(x972,x971)
% 0.51/0.57 [99]P5(x991)+~P8(x991,x992)
% 0.51/0.57 [100]P5(x1001)+~P4(x1001,x1002)
% 0.51/0.57 [102]P11(x1021)+~P3(x1022,x1021)
% 0.51/0.57 [104]P11(x1041)+~P3(x1041,x1042)
% 0.51/0.57 [106]P17(x1061)+~P10(x1061,x1062)
% 0.51/0.57 [108]~P4(x1082,x1081)+P4(x1081,x1082)
% 0.51/0.57 [107]~P3(x1072,x1071)+P2(x1071)+~P2(x1072)
% 0.51/0.57 [109]~P3(x1091,x1093)+P3(x1091,x1092)+~P3(x1093,x1092)
% 0.51/0.57 [112]~P8(x1121,x1123)+P8(x1121,x1122)+~P8(x1123,x1122)
% 0.51/0.57 [113]~P4(x1133,x1132)+P4(x1131,x1132)+~P8(x1131,x1133)
% 0.51/0.57 [114]~P4(x1141,x1143)+P4(x1141,x1142)+~P8(x1142,x1143)
% 0.51/0.57 [115]~P10(x1151,x1153)+P10(x1151,x1152)+~P8(x1153,x1152)
% 0.51/0.57 [116]~P9(x1161,x1163)+P7(x1161,x1162)+~P7(x1163,x1162)
% 0.51/0.57 [117]~P9(x1173,x1172)+P7(x1171,x1172)+~P7(x1171,x1173)
% 0.51/0.57 [118]~P7(x1181,x1183)+P9(x1181,x1182)+~P7(x1183,x1182)
% 0.51/0.57 [119]~P9(x1191,x1193)+P9(x1191,x1192)+~P9(x1193,x1192)
% 0.51/0.57 [120]~P10(x1203,x1201)+~P4(x1201,x1202)+~P10(x1203,x1202)
% 0.51/0.57 %EqnAxiom
% 0.51/0.57
% 0.51/0.57 %-------------------------------------------
% 0.51/0.57 cnf(121,plain,
% 0.51/0.57 (~P4(a13,a20)),
% 0.51/0.57 inference(scs_inference,[],[25,108])).
% 0.51/0.57 cnf(123,plain,
% 0.51/0.57 (P4(a6,a8)),
% 0.51/0.57 inference(scs_inference,[],[25,8,24,108,113])).
% 0.51/0.57 cnf(125,plain,
% 0.51/0.57 (~P4(a13,a18)),
% 0.51/0.57 inference(scs_inference,[],[25,8,12,24,108,113,114])).
% 0.51/0.57 cnf(129,plain,
% 0.51/0.57 (P8(a14,a7)),
% 0.51/0.57 inference(scs_inference,[],[25,5,7,8,9,12,24,108,113,114,109,112])).
% 0.51/0.57 cnf(139,plain,
% 0.51/0.57 (P8(a18,a14)),
% 0.51/0.57 inference(scs_inference,[],[125,10,11,108,114,112])).
% 0.51/0.57 cnf(143,plain,
% 0.51/0.57 (P3(a3,a5)),
% 0.51/0.57 inference(scs_inference,[],[125,5,6,10,11,108,114,112,113,109])).
% 0.51/0.57 cnf(153,plain,
% 0.51/0.57 (P8(a17,a8)),
% 0.51/0.57 inference(scs_inference,[],[13,14,112])).
% 0.51/0.57 cnf(159,plain,
% 0.51/0.57 (~P4(a12,a20)),
% 0.51/0.57 inference(scs_inference,[],[121,123,13,14,23,143,7,112,114,109,113])).
% 0.51/0.57 cnf(161,plain,
% 0.51/0.57 (~P4(a20,a12)),
% 0.51/0.57 inference(scs_inference,[],[121,123,13,14,23,143,7,112,114,109,113,108])).
% 0.51/0.57 cnf(187,plain,
% 0.51/0.57 (~P4(a20,a11)),
% 0.51/0.57 inference(scs_inference,[],[161,22,114])).
% 0.51/0.57 cnf(189,plain,
% 0.51/0.57 (P8(a21,a17)),
% 0.51/0.57 inference(scs_inference,[],[161,15,16,22,114,112])).
% 0.51/0.57 cnf(191,plain,
% 0.51/0.57 (~P4(a11,a20)),
% 0.51/0.57 inference(scs_inference,[],[159,161,15,16,22,114,112,113])).
% 0.51/0.57 cnf(197,plain,
% 0.51/0.57 (P8(a23,a21)),
% 0.51/0.57 inference(scs_inference,[],[17,18,112])).
% 0.51/0.57 cnf(199,plain,
% 0.51/0.57 (~P4(a10,a20)),
% 0.51/0.57 inference(scs_inference,[],[191,17,18,21,112,113])).
% 0.51/0.57 cnf(201,plain,
% 0.51/0.57 (~P4(a20,a10)),
% 0.51/0.57 inference(scs_inference,[],[187,191,17,18,21,112,113,114])).
% 0.51/0.57 cnf(214,plain,
% 0.51/0.57 (P8(a10,a23)),
% 0.51/0.57 inference(scs_inference,[],[199,201,19,20,114,113,112])).
% 0.51/0.57 cnf(220,plain,
% 0.51/0.57 (P8(a18,a7)),
% 0.51/0.57 inference(scs_inference,[],[129,139,112])).
% 0.51/0.57 cnf(222,plain,
% 0.51/0.57 (P4(a14,a8)),
% 0.51/0.57 inference(scs_inference,[],[129,139,24,112,113])).
% 0.51/0.57 cnf(243,plain,
% 0.51/0.57 (~P4(a23,a20)),
% 0.51/0.57 inference(scs_inference,[],[199,222,153,214,114,113])).
% 0.51/0.57 cnf(245,plain,
% 0.51/0.57 (P8(a21,a8)),
% 0.51/0.57 inference(scs_inference,[],[199,222,153,189,214,114,113,112])).
% 0.51/0.57 cnf(254,plain,
% 0.51/0.57 (~P4(a21,a20)),
% 0.51/0.57 inference(scs_inference,[],[243,197,113])).
% 0.51/0.57 cnf(256,plain,
% 0.51/0.57 (P8(a10,a21)),
% 0.51/0.57 inference(scs_inference,[],[243,197,214,113,112])).
% 0.51/0.58 cnf(267,plain,
% 0.51/0.58 (P8(a20,a7)),
% 0.51/0.58 inference(scs_inference,[],[125,220,12,114,112])).
% 0.51/0.58 cnf(269,plain,
% 0.51/0.58 (P4(a18,a8)),
% 0.51/0.58 inference(scs_inference,[],[125,220,12,24,114,112,113])).
% 0.51/0.58 cnf(277,plain,
% 0.51/0.58 (P8(a10,a8)),
% 0.51/0.58 inference(scs_inference,[],[245,256,112])).
% 0.51/0.58 cnf(283,plain,
% 0.51/0.58 (~P4(a20,a8)),
% 0.51/0.58 inference(scs_inference,[],[254,269,245,256,112,113,114,108])).
% 0.51/0.58 cnf(296,plain,
% 0.51/0.58 ($false),
% 0.51/0.58 inference(scs_inference,[],[283,123,267,277,24,114,113]),
% 0.51/0.58 ['proof']).
% 0.51/0.58 % SZS output end Proof
% 0.51/0.58 % Total time :0.020000s
%------------------------------------------------------------------------------