%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : CSR062+5 : TPTP v5.0.0. Bugfixed v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art01.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Sat Dec 25 06:35:57 EST 2010
% Result : Theorem 129.81s
% Output : CNFRefutation 134.37s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/CSR/CSR062+5.p
% --creating new selector for [CSR002+4.ax]
% -running prover on /tmp/tmp8RpZtn/sel_CSR062+5.p_1 with time limit 29
% -prover status CounterSatisfiable
% -running prover on /tmp/tmp8RpZtn/sel_CSR062+5.p_2 with time limit 60
% -prover status CounterSatisfiable
% --creating new selector for [CSR002+4.ax]
% -running prover on /tmp/tmp8RpZtn/sel_CSR062+5.p_3 with time limit 81
% -prover status Theorem
% Problem CSR062+5.p solved in phase 2.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/CSR/CSR062+5.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/CSR/CSR062+5.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:![X2]:(tptptypes_8_390(X1,X2)=>tptptypes_7_389(X1,X2)),file('/tmp/tmp8RpZtn/sel_CSR062+5.p_3', ax4_272404)).
% fof(5, axiom,genlmt(c_tptp_spindleheadmt,c_cyclistsmt),file('/tmp/tmp8RpZtn/sel_CSR062+5.p_3', ax4_176570)).
% fof(8, axiom,![X1]:![X2]:(tptptypes_6_388(X1,X2)=>tptptypes_5_387(X1,X2)),file('/tmp/tmp8RpZtn/sel_CSR062+5.p_3', ax4_56790)).
% fof(11, axiom,![X1]:![X2]:(tptptypes_7_389(X1,X2)=>tptptypes_6_388(X2,X1)),file('/tmp/tmp8RpZtn/sel_CSR062+5.p_3', ax4_69557)).
% fof(19, axiom,genlmt(c_tptp_member3205_mt,c_tptp_spindleheadmt),file('/tmp/tmp8RpZtn/sel_CSR062+5.p_3', ax4_308987)).
% fof(27, axiom,(mtvisible(c_cyclistsmt)=>tptptypes_8_390(c_pushingwithfingers,c_tptpcol_15_4027)),file('/tmp/tmp8RpZtn/sel_CSR062+5.p_3', ax4_271207)).
% fof(37, axiom,![X7]:![X8]:((mtvisible(X7)&genlmt(X7,X8))=>mtvisible(X8)),file('/tmp/tmp8RpZtn/sel_CSR062+5.p_3', ax4_540220)).
% fof(40, conjecture,?[X1]:(mtvisible(c_tptp_member3205_mt)=>tptptypes_5_387(X1,c_pushingwithfingers)),file('/tmp/tmp8RpZtn/sel_CSR062+5.p_3', query262)).
% fof(41, negated_conjecture,~(?[X1]:(mtvisible(c_tptp_member3205_mt)=>tptptypes_5_387(X1,c_pushingwithfingers))),inference(assume_negation,[status(cth)],[40])).
% fof(42, plain,![X1]:![X2]:(~(tptptypes_8_390(X1,X2))|tptptypes_7_389(X1,X2)),inference(fof_nnf,[status(thm)],[1])).
% fof(43, plain,![X3]:![X4]:(~(tptptypes_8_390(X3,X4))|tptptypes_7_389(X3,X4)),inference(variable_rename,[status(thm)],[42])).
% cnf(44,plain,(tptptypes_7_389(X1,X2)|~tptptypes_8_390(X1,X2)),inference(split_conjunct,[status(thm)],[43])).
% cnf(52,plain,(genlmt(c_tptp_spindleheadmt,c_cyclistsmt)),inference(split_conjunct,[status(thm)],[5])).
% fof(57, plain,![X1]:![X2]:(~(tptptypes_6_388(X1,X2))|tptptypes_5_387(X1,X2)),inference(fof_nnf,[status(thm)],[8])).
% fof(58, plain,![X3]:![X4]:(~(tptptypes_6_388(X3,X4))|tptptypes_5_387(X3,X4)),inference(variable_rename,[status(thm)],[57])).
% cnf(59,plain,(tptptypes_5_387(X1,X2)|~tptptypes_6_388(X1,X2)),inference(split_conjunct,[status(thm)],[58])).
% fof(64, plain,![X1]:![X2]:(~(tptptypes_7_389(X1,X2))|tptptypes_6_388(X2,X1)),inference(fof_nnf,[status(thm)],[11])).
% fof(65, plain,![X3]:![X4]:(~(tptptypes_7_389(X3,X4))|tptptypes_6_388(X4,X3)),inference(variable_rename,[status(thm)],[64])).
% cnf(66,plain,(tptptypes_6_388(X1,X2)|~tptptypes_7_389(X2,X1)),inference(split_conjunct,[status(thm)],[65])).
% cnf(84,plain,(genlmt(c_tptp_member3205_mt,c_tptp_spindleheadmt)),inference(split_conjunct,[status(thm)],[19])).
% fof(100, plain,(~(mtvisible(c_cyclistsmt))|tptptypes_8_390(c_pushingwithfingers,c_tptpcol_15_4027)),inference(fof_nnf,[status(thm)],[27])).
% cnf(101,plain,(tptptypes_8_390(c_pushingwithfingers,c_tptpcol_15_4027)|~mtvisible(c_cyclistsmt)),inference(split_conjunct,[status(thm)],[100])).
% fof(128, plain,![X7]:![X8]:((~(mtvisible(X7))|~(genlmt(X7,X8)))|mtvisible(X8)),inference(fof_nnf,[status(thm)],[37])).
% fof(129, plain,![X9]:![X10]:((~(mtvisible(X9))|~(genlmt(X9,X10)))|mtvisible(X10)),inference(variable_rename,[status(thm)],[128])).
% cnf(130,plain,(mtvisible(X1)|~genlmt(X2,X1)|~mtvisible(X2)),inference(split_conjunct,[status(thm)],[129])).
% fof(137, negated_conjecture,![X1]:(mtvisible(c_tptp_member3205_mt)&~(tptptypes_5_387(X1,c_pushingwithfingers))),inference(fof_nnf,[status(thm)],[41])).
% fof(138, negated_conjecture,![X2]:(mtvisible(c_tptp_member3205_mt)&~(tptptypes_5_387(X2,c_pushingwithfingers))),inference(variable_rename,[status(thm)],[137])).
% cnf(139,negated_conjecture,(~tptptypes_5_387(X1,c_pushingwithfingers)),inference(split_conjunct,[status(thm)],[138])).
% cnf(140,negated_conjecture,(mtvisible(c_tptp_member3205_mt)),inference(split_conjunct,[status(thm)],[138])).
% cnf(147,plain,(mtvisible(c_tptp_spindleheadmt)|~mtvisible(c_tptp_member3205_mt)),inference(spm,[status(thm)],[130,84,theory(equality)])).
% cnf(149,plain,(mtvisible(c_cyclistsmt)|~mtvisible(c_tptp_spindleheadmt)),inference(spm,[status(thm)],[130,52,theory(equality)])).
% cnf(155,plain,(mtvisible(c_tptp_spi
% ndleheadmt)|$false),inference(rw,[status(thm)],[147,140,theory(equality)])).
% cnf(156,plain,(mtvisible(c_tptp_spindleheadmt)),inference(cn,[status(thm)],[155,theory(equality)])).
% cnf(162,plain,(tptptypes_5_387(X1,X2)|~tptptypes_7_389(X2,X1)),inference(spm,[status(thm)],[59,66,theory(equality)])).
% cnf(174,plain,(mtvisible(c_cyclistsmt)|$false),inference(rw,[status(thm)],[149,156,theory(equality)])).
% cnf(175,plain,(mtvisible(c_cyclistsmt)),inference(cn,[status(thm)],[174,theory(equality)])).
% cnf(176,plain,(tptptypes_8_390(c_pushingwithfingers,c_tptpcol_15_4027)|$false),inference(rw,[status(thm)],[101,175,theory(equality)])).
% cnf(177,plain,(tptptypes_8_390(c_pushingwithfingers,c_tptpcol_15_4027)),inference(cn,[status(thm)],[176,theory(equality)])).
% cnf(178,negated_conjecture,(~tptptypes_7_389(c_pushingwithfingers,X1)),inference(spm,[status(thm)],[139,162,theory(equality)])).
% cnf(183,negated_conjecture,(~tptptypes_8_390(c_pushingwithfingers,X1)),inference(spm,[status(thm)],[178,44,theory(equality)])).
% cnf(184,plain,($false),inference(sr,[status(thm)],[177,183,theory(equality)])).
% cnf(185,plain,($false),184,['proof']).
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------