%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : SYN037-1 : TPTP v3.4.2. Released v1.0.0.
% Transfm : none
% Format : tptp
% Command : faust %s
% Computer : art05.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 1003MB
% OS : Linux 2.6.17-1.2142_FC4
% CPULimit : 600s
% DateTime : Wed May 6 16:38:30 EDT 2009
% Result : Unsatisfiable 2.8s
% Output : Refutation 2.8s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 35
% Syntax : Number of formulae : 208 ( 15 unt; 0 def)
% Number of atoms : 587 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 588 ( 209 ~; 379 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 13 ( 12 usr; 9 prp; 0-1 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-1 aty)
% Number of variables : 95 ( 62 sgn 18 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Faust---1.0 format not known, defaulting to TPTP
fof(clause_9,plain,
( ~ q(s8)
| n8 ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144705520,plain,
( ~ q(s8)
| n8 ),
inference(rewrite,[status(thm)],[clause_9]),
[] ).
fof(clause_11,plain,
! [A] :
( ~ p(A)
| n7 ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144719240,plain,
( ~ p(A)
| n7 ),
inference(rewrite,[status(thm)],[clause_11]),
[] ).
fof(clause_26,plain,
! [A] :
( p(A)
| p(s1(A))
| n1(A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144846552,plain,
( p(A)
| p(s1(A))
| n1(A) ),
inference(rewrite,[status(thm)],[clause_26]),
[] ).
cnf(245970128,plain,
( n7
| p(A)
| n1(A) ),
inference(resolution,[status(thm)],[144719240,144846552]),
[] ).
cnf(246483144,plain,
( n7
| n1(A) ),
inference(resolution,[status(thm)],[245970128,144719240]),
[] ).
fof(clause_23,plain,
! [A] :
( ~ n1(A)
| n2 ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144821208,plain,
( ~ n1(A)
| n2 ),
inference(rewrite,[status(thm)],[clause_23]),
[] ).
cnf(246499888,plain,
( n7
| n2 ),
inference(resolution,[status(thm)],[246483144,144821208]),
[] ).
fof(clause_35,plain,
( ~ n7
| n8
| ~ n10 ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144917680,plain,
( ~ n7
| n8
| ~ n10 ),
inference(rewrite,[status(thm)],[clause_35]),
[] ).
cnf(246540064,plain,
( n2
| n8
| ~ n10 ),
inference(resolution,[status(thm)],[246499888,144917680]),
[] ).
fof(clause_4,plain,
( n2
| n9
| n6
| n10 ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144665376,plain,
( n2
| n9
| n6
| n10 ),
inference(rewrite,[status(thm)],[clause_4]),
[] ).
cnf(246577584,plain,
( n2
| n8
| n9
| n6 ),
inference(resolution,[status(thm)],[246540064,144665376]),
[] ).
fof(clause_6,plain,
( ~ n2
| n9
| n6
| ~ n10 ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144680312,plain,
( ~ n2
| n9
| n6
| ~ n10 ),
inference(rewrite,[status(thm)],[clause_6]),
[] ).
fof(clause_34,plain,
( n7
| n8
| n10 ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144907208,plain,
( n7
| n8
| n10 ),
inference(rewrite,[status(thm)],[clause_34]),
[] ).
cnf(247819696,plain,
( n9
| n6
| n7
| n8 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[246577584,144680312,144907208]),
[] ).
fof(clause_21,plain,
! [A] :
( ~ q(A)
| n3 ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144803456,plain,
( ~ q(A)
| n3 ),
inference(rewrite,[status(thm)],[clause_21]),
[] ).
fof(clause_16,plain,
! [A] :
( q(s5(A))
| q(A)
| n5(A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144764208,plain,
( q(s5(A))
| q(A)
| n5(A) ),
inference(rewrite,[status(thm)],[clause_16]),
[] ).
cnf(246086056,plain,
( n3
| q(A)
| n5(A) ),
inference(resolution,[status(thm)],[144803456,144764208]),
[] ).
cnf(246818264,plain,
( n3
| n5(A) ),
inference(resolution,[status(thm)],[246086056,144803456]),
[] ).
fof(clause_13,plain,
! [A] :
( ~ n5(A)
| n6 ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144736800,plain,
( ~ n5(A)
| n6 ),
inference(rewrite,[status(thm)],[clause_13]),
[] ).
cnf(246851912,plain,
( n3
| n6 ),
inference(resolution,[status(thm)],[246818264,144736800]),
[] ).
fof(clause_31,plain,
( ~ n3
| n4
| ~ n9 ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144885128,plain,
( ~ n3
| n4
| ~ n9 ),
inference(rewrite,[status(thm)],[clause_31]),
[] ).
cnf(246903312,plain,
( n6
| n4
| ~ n9 ),
inference(resolution,[status(thm)],[246851912,144885128]),
[] ).
fof(clause_20,plain,
! [A] :
( ~ n4
| p(A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144797672,plain,
( ~ n4
| p(A) ),
inference(rewrite,[status(thm)],[clause_20]),
[] ).
cnf(246052960,plain,
( ~ n4
| n7 ),
inference(resolution,[status(thm)],[144797672,144719240]),
[] ).
cnf(246945064,plain,
( n6
| ~ n9
| n7 ),
inference(resolution,[status(thm)],[246903312,246052960]),
[] ).
cnf(247953960,plain,
( n6
| n7
| n8 ),
inference(resolution,[status(thm)],[247819696,246945064]),
[] ).
fof(clause_10,plain,
! [A] :
( ~ n8
| q(A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144629720,plain,
( ~ n8
| q(A) ),
inference(rewrite,[status(thm)],[clause_10]),
[] ).
cnf(247973272,plain,
( n6
| n7
| q(A) ),
inference(resolution,[status(thm)],[247953960,144629720]),
[] ).
fof(clause_17,plain,
! [A,B] :
( ~ n5(A)
| ~ q(B)
| q(A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144774640,plain,
( ~ n5(A)
| ~ q(B)
| q(A) ),
inference(rewrite,[status(thm)],[clause_17]),
[] ).
fof(clause_14,plain,
( ~ n6
| n5(s6) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144743752,plain,
( ~ n6
| n5(s6) ),
inference(rewrite,[status(thm)],[clause_14]),
[] ).
cnf(257592000,plain,
( ~ q(A)
| q(s6)
| ~ n6 ),
inference(resolution,[status(thm)],[144774640,144743752]),
[] ).
fof(clause_22,plain,
( ~ n3
| q(s3) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144810440,plain,
( ~ n3
| q(s3) ),
inference(rewrite,[status(thm)],[clause_22]),
[] ).
fof(clause_5,plain,
( ~ n2
| n9
| ~ n6
| n10 ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144673752,plain,
( ~ n2
| n9
| ~ n6
| n10 ),
inference(rewrite,[status(thm)],[clause_5]),
[] ).
fof(clause_30,plain,
( n3
| n4
| n9 ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144874384,plain,
( n3
| n4
| n9 ),
inference(rewrite,[status(thm)],[clause_30]),
[] ).
cnf(246070008,plain,
( n7
| n3
| n9 ),
inference(resolution,[status(thm)],[246052960,144874384]),
[] ).
cnf(246378704,plain,
( n8
| ~ n10
| n3
| n9 ),
inference(resolution,[status(thm)],[144917680,246070008]),
[] ).
cnf(246078416,plain,
( n3
| ~ n8 ),
inference(resolution,[status(thm)],[144803456,144629720]),
[] ).
cnf(247355672,plain,
( ~ n10
| n3
| n9 ),
inference(resolution,[status(thm)],[246378704,246078416]),
[] ).
cnf(247673024,plain,
( ~ n2
| n9
| n3 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[246851912,144673752,247355672]),
[] ).
fof(clause_1,plain,
( ~ n2
| ~ n9
| ~ n6
| ~ n10 ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144637152,plain,
( ~ n2
| ~ n9
| ~ n6
| ~ n10 ),
inference(rewrite,[status(thm)],[clause_1]),
[] ).
cnf(246103224,plain,
( n3
| n7
| n10 ),
inference(resolution,[status(thm)],[246078416,144907208]),
[] ).
cnf(253392288,plain,
( n3
| n7 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[247673024,246499888,246851912,144637152,246103224]),
[] ).
cnf(253398080,plain,
( q(s3)
| n7 ),
inference(resolution,[status(thm)],[144810440,253392288]),
[] ).
cnf(257865096,plain,
( q(s6)
| n7 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[247973272,257592000,253398080]),
[] ).
fof(clause_18,plain,
! [A,B] :
( ~ n5(A)
| q(B)
| ~ q(A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144629200,plain,
( ~ n5(A)
| q(B)
| ~ q(A) ),
inference(rewrite,[status(thm)],[clause_18]),
[] ).
cnf(257602680,plain,
( q(A)
| ~ q(s6)
| ~ n6 ),
inference(resolution,[status(thm)],[144629200,144743752]),
[] ).
fof(clause_15,plain,
! [A] :
( ~ q(s5(A))
| ~ q(A)
| n5(A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144751320,plain,
( ~ q(s5(A))
| ~ q(A)
| n5(A) ),
inference(rewrite,[status(thm)],[clause_15]),
[] ).
cnf(257632640,plain,
( ~ q(s5(A))
| ~ q(A)
| n6 ),
inference(resolution,[status(thm)],[144751320,144736800]),
[] ).
cnf(257872128,plain,
( n6
| n7 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[247973272,257632640,253398080]),
[] ).
cnf(257927712,plain,
( q(A)
| n7 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[257865096,257602680,257872128]),
[] ).
cnf(258088312,plain,
( n8
| n7 ),
inference(resolution,[status(thm)],[144705520,257927712]),
[] ).
cnf(246244768,plain,
( ~ n3
| ~ n9
| n7 ),
inference(resolution,[status(thm)],[144885128,246052960]),
[] ).
cnf(247160232,plain,
( ~ n9
| n7
| n10 ),
inference(resolution,[status(thm)],[246244768,246103224]),
[] ).
cnf(247667112,plain,
( ~ n6
| n10
| n7 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[246499888,144673752,247160232]),
[] ).
cnf(258349328,plain,
( n7
| n10 ),
inference(resolution,[status(thm)],[257872128,247667112]),
[] ).
fof(clause_36,plain,
( n7
| ~ n8
| ~ n10 ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144924336,plain,
( n7
| ~ n8
| ~ n10 ),
inference(rewrite,[status(thm)],[clause_36]),
[] ).
cnf(258889824,plain,
n7,
inference(forward_subsumption_resolution__resolution,[status(thm)],[258088312,258349328,144924336]),
[] ).
cnf(247887840,plain,
( n6
| ~ n10
| n7 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[246499888,144680312,246945064]),
[] ).
cnf(257638152,plain,
( n6
| ~ n8 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[144629720,257632640,144629720]),
[] ).
cnf(257967368,plain,
( ~ n10
| n6 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[247887840,144917680,257638152]),
[] ).
fof(clause_7,plain,
( n2
| ~ n9
| ~ n6
| n10 ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144688496,plain,
( n2
| ~ n9
| ~ n6
| n10 ),
inference(rewrite,[status(thm)],[clause_7]),
[] ).
cnf(246568944,plain,
( n2
| ~ n10
| n3 ),
inference(resolution,[status(thm)],[246540064,246078416]),
[] ).
cnf(248289376,plain,
( n2
| ~ n9
| n3 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[246851912,144688496,246568944]),
[] ).
cnf(248341792,plain,
( n2
| n3
| n4 ),
inference(resolution,[status(thm)],[248289376,144874384]),
[] ).
cnf(257972536,plain,
( n2
| n9
| n6 ),
inference(resolution,[status(thm)],[246577584,257638152]),
[] ).
cnf(258213952,plain,
( ~ q(A)
| q(s6)
| n2
| n9 ),
inference(resolution,[status(thm)],[257592000,257972536]),
[] ).
cnf(258226496,plain,
( q(s6)
| n2
| n9
| ~ n3 ),
inference(resolution,[status(thm)],[258213952,144810440]),
[] ).
cnf(258397304,plain,
( n2
| n6
| n4 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[248341792,257972536,144885128]),
[] ).
cnf(258655408,plain,
( q(A)
| ~ q(s6)
| n2
| n4 ),
inference(resolution,[status(thm)],[257602680,258397304]),
[] ).
fof(clause_29,plain,
( ~ n3
| ~ n4
| n9 ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144865736,plain,
( ~ n3
| ~ n4
| n9 ),
inference(rewrite,[status(thm)],[clause_29]),
[] ).
cnf(258731792,plain,
( q(A)
| n2
| ~ n3
| n9 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[258226496,258655408,144865736]),
[] ).
cnf(264764176,plain,
( q(A)
| n2
| n4 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[248341792,258731792,144885128]),
[] ).
cnf(268728680,plain,
( n2
| n4
| n8 ),
inference(resolution,[status(thm)],[264764176,144705520]),
[] ).
cnf(248379544,plain,
( n2
| ~ n9
| n4 ),
inference(resolution,[status(thm)],[248289376,144885128]),
[] ).
cnf(248455048,plain,
( n2
| ~ n9
| p(A) ),
inference(resolution,[status(thm)],[248379544,144797672]),
[] ).
fof(clause_3,plain,
( n2
| n9
| ~ n6
| ~ n10 ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144654632,plain,
( n2
| n9
| ~ n6
| ~ n10 ),
inference(rewrite,[status(thm)],[clause_3]),
[] ).
cnf(250405872,plain,
( n2
| p(A)
| ~ n6
| ~ n10 ),
inference(resolution,[status(thm)],[248455048,144654632]),
[] ).
cnf(262653336,plain,
( n2
| p(A)
| ~ n10 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[246540064,250405872,257638152]),
[] ).
fof(clause_33,plain,
( ~ n7
| ~ n8
| n10 ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144898216,plain,
( ~ n7
| ~ n8
| n10 ),
inference(rewrite,[status(thm)],[clause_33]),
[] ).
cnf(246532440,plain,
( n2
| ~ n8
| n10 ),
inference(resolution,[status(thm)],[246499888,144898216]),
[] ).
cnf(262694584,plain,
( n2
| p(A)
| ~ n8 ),
inference(resolution,[status(thm)],[262653336,246532440]),
[] ).
fof(clause_19,plain,
( ~ p(s4)
| n4 ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144786520,plain,
( ~ p(s4)
| n4 ),
inference(rewrite,[status(thm)],[clause_19]),
[] ).
cnf(262714384,plain,
( n2
| ~ n8
| n4 ),
inference(resolution,[status(thm)],[262694584,144786520]),
[] ).
cnf(268851440,plain,
( n2
| n4 ),
inference(resolution,[status(thm)],[268728680,262714384]),
[] ).
fof(clause_24,plain,
( ~ n2
| n1(s2) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144826680,plain,
( ~ n2
| n1(s2) ),
inference(rewrite,[status(thm)],[clause_24]),
[] ).
cnf(268880344,plain,
( n4
| n1(s2) ),
inference(resolution,[status(thm)],[268851440,144826680]),
[] ).
fof(clause_27,plain,
! [A,B] :
( ~ n1(A)
| ~ p(A)
| p(B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144852928,plain,
( ~ n1(A)
| ~ p(A)
| p(B) ),
inference(rewrite,[status(thm)],[clause_27]),
[] ).
cnf(259230960,plain,
( ~ n1(A)
| ~ p(A)
| n4 ),
inference(resolution,[status(thm)],[144852928,144786520]),
[] ).
cnf(268875136,plain,
( n2
| p(A) ),
inference(resolution,[status(thm)],[268851440,144797672]),
[] ).
fof(clause_28,plain,
! [A,B] :
( ~ n1(A)
| p(A)
| ~ p(B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144859784,plain,
( ~ n1(A)
| p(A)
| ~ p(B) ),
inference(rewrite,[status(thm)],[clause_28]),
[] ).
fof(clause_12,plain,
( ~ n7
| p(s7) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144730248,plain,
( ~ n7
| p(s7) ),
inference(rewrite,[status(thm)],[clause_12]),
[] ).
cnf(269872776,plain,
( ~ n1(A)
| p(A) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[258889824,144859784,144730248]),
[] ).
cnf(269891392,plain,
p(s2),
inference(forward_subsumption_resolution__resolution,[status(thm)],[268875136,269872776,144826680]),
[] ).
cnf(269907912,plain,
n4,
inference(forward_subsumption_resolution__resolution,[status(thm)],[268880344,259230960,269891392]),
[] ).
cnf(269001712,plain,
( p(A)
| n1(s2) ),
inference(resolution,[status(thm)],[268875136,144826680]),
[] ).
cnf(269898672,plain,
p(A),
inference(forward_subsumption_resolution__resolution,[status(thm)],[269001712,144852928,269891392]),
[] ).
fof(clause_25,plain,
! [A] :
( ~ p(A)
| ~ p(s1(A))
| n1(A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144833568,plain,
( ~ p(A)
| ~ p(s1(A))
| n1(A) ),
inference(rewrite,[status(thm)],[clause_25]),
[] ).
cnf(270455032,plain,
n1(s7),
inference(forward_subsumption_resolution__resolution,[status(thm)],[246483144,269898672,144833568,144730248]),
[] ).
cnf(270767352,plain,
n2,
inference(resolution,[status(thm)],[270455032,144821208]),
[] ).
cnf(270841712,plain,
( n9
| n3 ),
inference(resolution,[status(thm)],[270767352,247673024]),
[] ).
cnf(270853448,plain,
n9,
inference(forward_subsumption_resolution__resolution,[status(thm)],[269907912,270841712,144865736]),
[] ).
cnf(274518512,plain,
~ n10,
inference(forward_subsumption_resolution__resolution,[status(thm)],[257967368,270853448,144637152,270767352]),
[] ).
cnf(274529520,plain,
~ n8,
inference(forward_subsumption_resolution__resolution,[status(thm)],[258889824,274518512,144898216]),
[] ).
cnf(260627704,plain,
( ~ p(s2)
| p(A)
| ~ n2 ),
inference(resolution,[status(thm)],[144852928,144826680]),
[] ).
cnf(260644552,plain,
( ~ p(s2)
| p(A)
| n9
| n6
| n10 ),
inference(resolution,[status(thm)],[260627704,144665376]),
[] ).
cnf(260796632,plain,
( ~ p(s2)
| p(A)
| n6
| n10
| n4 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[246851912,260644552,144885128]),
[] ).
cnf(260894344,plain,
( ~ p(s2)
| p(A)
| n10
| n4
| n5(s6) ),
inference(resolution,[status(thm)],[260796632,144743752]),
[] ).
cnf(261063624,plain,
( ~ p(s2)
| n10
| n4
| n5(s6) ),
inference(resolution,[status(thm)],[260894344,144786520]),
[] ).
cnf(259002656,plain,
( n8
| ~ n10 ),
inference(resolution,[status(thm)],[144917680,258889824]),
[] ).
cnf(261076776,plain,
( ~ p(s2)
| n4
| n5(s6)
| n8 ),
inference(resolution,[status(thm)],[261063624,259002656]),
[] ).
cnf(246891632,plain,
( n6
| ~ n4
| n9 ),
inference(resolution,[status(thm)],[246851912,144865736]),
[] ).
cnf(261139440,plain,
( ~ p(s2)
| n5(s6)
| n8
| n6
| n9 ),
inference(resolution,[status(thm)],[261076776,246891632]),
[] ).
cnf(260636088,plain,
( p(s2)
| ~ p(A)
| ~ n2 ),
inference(resolution,[status(thm)],[144859784,144826680]),
[] ).
cnf(260783312,plain,
( p(s2)
| ~ p(A)
| n8
| n9
| n6 ),
inference(resolution,[status(thm)],[260636088,246577584]),
[] ).
cnf(260884264,plain,
( p(s2)
| ~ p(A)
| n8
| n6
| n4 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[246851912,260783312,144885128]),
[] ).
cnf(260974432,plain,
( p(s2)
| ~ p(A)
| n8
| n4
| n5(s6) ),
inference(resolution,[status(thm)],[260884264,144743752]),
[] ).
cnf(261202456,plain,
( ~ p(A)
| n8
| n5(s6)
| n6
| n9 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[261139440,260974432,246891632]),
[] ).
cnf(246390352,plain,
( ~ n7
| ~ n10
| n3 ),
inference(resolution,[status(thm)],[144917680,246078416]),
[] ).
cnf(253413072,plain,
( ~ n10
| n3 ),
inference(resolution,[status(thm)],[246390352,253392288]),
[] ).
cnf(247834360,plain,
( ~ n2
| n9
| ~ n10
| n5(s6) ),
inference(resolution,[status(thm)],[144680312,144743752]),
[] ).
cnf(255114048,plain,
( ~ n2
| ~ n10
| n5(s6)
| n4 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[253413072,247834360,144885128]),
[] ).
cnf(255136136,plain,
( ~ n2
| ~ n10
| n5(s6)
| p(A) ),
inference(resolution,[status(thm)],[255114048,144797672]),
[] ).
cnf(255490736,plain,
( ~ n2
| n5(s6)
| p(A)
| ~ n7
| ~ n8 ),
inference(resolution,[status(thm)],[255136136,144898216]),
[] ).
cnf(255876016,plain,
( ~ n2
| n5(s6)
| p(A)
| ~ n8
| ~ p(B) ),
inference(resolution,[status(thm)],[255490736,144719240]),
[] ).
cnf(263237272,plain,
( n5(s6)
| p(A)
| ~ p(B)
| n9
| n6 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[261202456,255876016,257972536]),
[] ).
cnf(263263152,plain,
( p(A)
| ~ p(B)
| n9
| n6 ),
inference(resolution,[status(thm)],[263237272,144736800]),
[] ).
cnf(263286256,plain,
( p(A)
| ~ p(B)
| n6
| n4 ),
inference(resolution,[status(thm)],[263263152,246903312]),
[] ).
cnf(263307832,plain,
( p(A)
| ~ p(B)
| n4
| n5(s6) ),
inference(resolution,[status(thm)],[263286256,144743752]),
[] ).
cnf(263358200,plain,
( ~ p(A)
| n4
| n5(s6) ),
inference(resolution,[status(thm)],[263307832,144786520]),
[] ).
cnf(258104904,plain,
( p(s7)
| q(A) ),
inference(resolution,[status(thm)],[144730248,257927712]),
[] ).
cnf(246453024,plain,
( n7
| ~ n10
| ~ q(s8) ),
inference(resolution,[status(thm)],[144924336,144705520]),
[] ).
cnf(251949824,plain,
( ~ n10
| ~ q(s8)
| p(s7) ),
inference(resolution,[status(thm)],[246453024,144730248]),
[] ).
cnf(258360760,plain,
( p(s7)
| n10 ),
inference(resolution,[status(thm)],[144730248,258349328]),
[] ).
cnf(258946096,plain,
p(s7),
inference(forward_subsumption_resolution__resolution,[status(thm)],[258104904,251949824,258360760]),
[] ).
cnf(264028432,plain,
( n4
| n5(s6) ),
inference(resolution,[status(thm)],[263358200,258946096]),
[] ).
cnf(264091304,plain,
( n5(s6)
| n9 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[246818264,264028432,144865736]),
[] ).
cnf(264099592,plain,
( n9
| n6 ),
inference(resolution,[status(thm)],[264091304,144736800]),
[] ).
fof(clause_2,plain,
( ~ n2
| ~ n9
| n6
| n10 ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144644632,plain,
( ~ n2
| ~ n9
| n6
| n10 ),
inference(rewrite,[status(thm)],[clause_2]),
[] ).
cnf(271823776,plain,
( n6
| n10 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[264099592,144644632,270767352]),
[] ).
cnf(271834128,plain,
( n5(s6)
| n10 ),
inference(resolution,[status(thm)],[144743752,271823776]),
[] ).
cnf(271855560,plain,
( n5(s6)
| n8 ),
inference(resolution,[status(thm)],[271834128,259002656]),
[] ).
cnf(274616032,plain,
( ~ n5(A)
| ~ q(A)
| n8 ),
inference(resolution,[status(thm)],[144629200,144705520]),
[] ).
cnf(247188184,plain,
( n6
| n8
| ~ n10 ),
inference(resolution,[status(thm)],[247953960,144917680]),
[] ).
cnf(248138952,plain,
( n6
| ~ n10
| q(A) ),
inference(resolution,[status(thm)],[247188184,144629720]),
[] ).
cnf(250192568,plain,
( n6
| q(A)
| ~ n2
| ~ n9 ),
inference(resolution,[status(thm)],[248138952,144644632]),
[] ).
cnf(245946360,plain,
( q(A)
| n7
| n10 ),
inference(resolution,[status(thm)],[144629720,144907208]),
[] ).
cnf(253505952,plain,
( ~ n9
| q(A)
| n7 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[250192568,246499888,144637152,245946360]),
[] ).
cnf(248405696,plain,
( n3
| n4
| n1(s2) ),
inference(resolution,[status(thm)],[248341792,144826680]),
[] ).
cnf(261353304,plain,
( ~ p(s2)
| p(A)
| n3
| n4 ),
inference(resolution,[status(thm)],[144852928,248405696]),
[] ).
cnf(261416472,plain,
( ~ p(s2)
| n3
| n4 ),
inference(resolution,[status(thm)],[261353304,144786520]),
[] ).
fof(clause_32,plain,
( n3
| ~ n4
| ~ n9 ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),
[] ).
cnf(144891688,plain,
( n3
| ~ n4
| ~ n9 ),
inference(rewrite,[status(thm)],[clause_32]),
[] ).
cnf(261444104,plain,
( ~ p(s2)
| n3
| ~ n9 ),
inference(resolution,[status(thm)],[261416472,144891688]),
[] ).
cnf(261360936,plain,
( p(s2)
| ~ p(A)
| n3
| n4 ),
inference(resolution,[status(thm)],[144859784,248405696]),
[] ).
cnf(261456928,plain,
( ~ p(A)
| n3
| ~ n9 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[261444104,261360936,144891688]),
[] ).
cnf(265721296,plain,
( ~ p(A)
| ~ n9
| q(s3) ),
inference(resolution,[status(thm)],[261456928,144810440]),
[] ).
cnf(265781072,plain,
( ~ n9
| q(s3) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[253505952,265721296,144730248]),
[] ).
cnf(266229344,plain,
( ~ n9
| n3 ),
inference(resolution,[status(thm)],[265781072,144803456]),
[] ).
cnf(266241160,plain,
( n3
| n4 ),
inference(resolution,[status(thm)],[266229344,144874384]),
[] ).
cnf(270893024,plain,
n3,
inference(forward_subsumption_resolution__resolution,[status(thm)],[266241160,270853448,144891688]),
[] ).
cnf(257654528,plain,
( ~ n5(A)
| q(A)
| ~ n3 ),
inference(resolution,[status(thm)],[144774640,144810440]),
[] ).
cnf(264122288,plain,
( n5(s6)
| ~ n2
| n6
| n10 ),
inference(resolution,[status(thm)],[264091304,144644632]),
[] ).
cnf(264196944,plain,
( n5(s6)
| ~ n2
| n6 ),
inference(resolution,[status(thm)],[264122288,257967368]),
[] ).
cnf(264226856,plain,
( ~ n2
| n6 ),
inference(resolution,[status(thm)],[264196944,144736800]),
[] ).
cnf(258134520,plain,
( n5(A)
| n7 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[257927712,144751320,257927712]),
[] ).
cnf(257581248,plain,
( n5(A)
| ~ n8 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[144629720,144751320,144629720]),
[] ).
cnf(263605848,plain,
( n5(A)
| ~ n10 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[258134520,257581248,144917680]),
[] ).
cnf(268587752,plain,
( n5(A)
| ~ n2
| n9 ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[264226856,263605848,144673752]),
[] ).
cnf(261992424,plain,
( n6
| ~ n2
| ~ n9 ),
inference(resolution,[status(thm)],[257967368,144644632]),
[] ).
cnf(270471032,plain,
( ~ n2
| n5(s6) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[268587752,261992424,144743752]),
[] ).
cnf(271903920,plain,
n5(s6),
inference(resolution,[status(thm)],[270471032,270767352]),
[] ).
cnf(274727688,plain,
q(s6),
inference(forward_subsumption_resolution__resolution,[status(thm)],[270893024,257654528,271903920]),
[] ).
cnf(274760352,plain,
n8,
inference(forward_subsumption_resolution__resolution,[status(thm)],[271855560,274616032,274727688]),
[] ).
cnf(contradiction,plain,
$false,
inference(resolution,[status(thm)],[274529520,274760352]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 3 seconds
% START OF PROOF SEQUENCE
% fof(clause_9,plain,(~q(s8)|n8),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144705520,plain,(~q(s8)|n8),inference(rewrite,[status(thm)],[clause_9]),[]).
%
% fof(clause_11,plain,(~p(A)|n7),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144719240,plain,(~p(A)|n7),inference(rewrite,[status(thm)],[clause_11]),[]).
%
% fof(clause_26,plain,(p(A)|p(s1(A))|n1(A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144846552,plain,(p(A)|p(s1(A))|n1(A)),inference(rewrite,[status(thm)],[clause_26]),[]).
%
% cnf(245970128,plain,(n7|p(A)|n1(A)),inference(resolution,[status(thm)],[144719240,144846552]),[]).
%
% cnf(246483144,plain,(n7|n1(A)),inference(resolution,[status(thm)],[245970128,144719240]),[]).
%
% fof(clause_23,plain,(~n1(A)|n2),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144821208,plain,(~n1(A)|n2),inference(rewrite,[status(thm)],[clause_23]),[]).
%
% cnf(246499888,plain,(n7|n2),inference(resolution,[status(thm)],[246483144,144821208]),[]).
%
% fof(clause_35,plain,(~n7|n8|~n10),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144917680,plain,(~n7|n8|~n10),inference(rewrite,[status(thm)],[clause_35]),[]).
%
% cnf(246540064,plain,(n2|n8|~n10),inference(resolution,[status(thm)],[246499888,144917680]),[]).
%
% fof(clause_4,plain,(n2|n9|n6|n10),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144665376,plain,(n2|n9|n6|n10),inference(rewrite,[status(thm)],[clause_4]),[]).
%
% cnf(246577584,plain,(n2|n8|n9|n6),inference(resolution,[status(thm)],[246540064,144665376]),[]).
%
% fof(clause_6,plain,(~n2|n9|n6|~n10),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144680312,plain,(~n2|n9|n6|~n10),inference(rewrite,[status(thm)],[clause_6]),[]).
%
% fof(clause_34,plain,(n7|n8|n10),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144907208,plain,(n7|n8|n10),inference(rewrite,[status(thm)],[clause_34]),[]).
%
% cnf(247819696,plain,(n9|n6|n7|n8),inference(forward_subsumption_resolution__resolution,[status(thm)],[246577584,144680312,144907208]),[]).
%
% fof(clause_21,plain,(~q(A)|n3),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144803456,plain,(~q(A)|n3),inference(rewrite,[status(thm)],[clause_21]),[]).
%
% fof(clause_16,plain,(q(s5(A))|q(A)|n5(A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144764208,plain,(q(s5(A))|q(A)|n5(A)),inference(rewrite,[status(thm)],[clause_16]),[]).
%
% cnf(246086056,plain,(n3|q(A)|n5(A)),inference(resolution,[status(thm)],[144803456,144764208]),[]).
%
% cnf(246818264,plain,(n3|n5(A)),inference(resolution,[status(thm)],[246086056,144803456]),[]).
%
% fof(clause_13,plain,(~n5(A)|n6),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144736800,plain,(~n5(A)|n6),inference(rewrite,[status(thm)],[clause_13]),[]).
%
% cnf(246851912,plain,(n3|n6),inference(resolution,[status(thm)],[246818264,144736800]),[]).
%
% fof(clause_31,plain,(~n3|n4|~n9),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144885128,plain,(~n3|n4|~n9),inference(rewrite,[status(thm)],[clause_31]),[]).
%
% cnf(246903312,plain,(n6|n4|~n9),inference(resolution,[status(thm)],[246851912,144885128]),[]).
%
% fof(clause_20,plain,(~n4|p(A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144797672,plain,(~n4|p(A)),inference(rewrite,[status(thm)],[clause_20]),[]).
%
% cnf(246052960,plain,(~n4|n7),inference(resolution,[status(thm)],[144797672,144719240]),[]).
%
% cnf(246945064,plain,(n6|~n9|n7),inference(resolution,[status(thm)],[246903312,246052960]),[]).
%
% cnf(247953960,plain,(n6|n7|n8),inference(resolution,[status(thm)],[247819696,246945064]),[]).
%
% fof(clause_10,plain,(~n8|q(A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144629720,plain,(~n8|q(A)),inference(rewrite,[status(thm)],[clause_10]),[]).
%
% cnf(247973272,plain,(n6|n7|q(A)),inference(resolution,[status(thm)],[247953960,144629720]),[]).
%
% fof(clause_17,plain,(~n5(A)|~q(B)|q(A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144774640,plain,(~n5(A)|~q(B)|q(A)),inference(rewrite,[status(thm)],[clause_17]),[]).
%
% fof(clause_14,plain,(~n6|n5(s6)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144743752,plain,(~n6|n5(s6)),inference(rewrite,[status(thm)],[clause_14]),[]).
%
% cnf(257592000,plain,(~q(A)|q(s6)|~n6),inference(resolution,[status(thm)],[144774640,144743752]),[]).
%
% fof(clause_22,plain,(~n3|q(s3)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144810440,plain,(~n3|q(s3)),inference(rewrite,[status(thm)],[clause_22]),[]).
%
% fof(clause_5,plain,(~n2|n9|~n6|n10),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144673752,plain,(~n2|n9|~n6|n10),inference(rewrite,[status(thm)],[clause_5]),[]).
%
% fof(clause_30,plain,(n3|n4|n9),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144874384,plain,(n3|n4|n9),inference(rewrite,[status(thm)],[clause_30]),[]).
%
% cnf(246070008,plain,(n7|n3|n9),inference(resolution,[status(thm)],[246052960,144874384]),[]).
%
% cnf(246378704,plain,(n8|~n10|n3|n9),inference(resolution,[status(thm)],[144917680,246070008]),[]).
%
% cnf(246078416,plain,(n3|~n8),inference(resolution,[status(thm)],[144803456,144629720]),[]).
%
% cnf(247355672,plain,(~n10|n3|n9),inference(resolution,[status(thm)],[246378704,246078416]),[]).
%
% cnf(247673024,plain,(~n2|n9|n3),inference(forward_subsumption_resolution__resolution,[status(thm)],[246851912,144673752,247355672]),[]).
%
% fof(clause_1,plain,(~n2|~n9|~n6|~n10),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144637152,plain,(~n2|~n9|~n6|~n10),inference(rewrite,[status(thm)],[clause_1]),[]).
%
% cnf(246103224,plain,(n3|n7|n10),inference(resolution,[status(thm)],[246078416,144907208]),[]).
%
% cnf(253392288,plain,(n3|n7),inference(forward_subsumption_resolution__resolution,[status(thm)],[247673024,246499888,246851912,144637152,246103224]),[]).
%
% cnf(253398080,plain,(q(s3)|n7),inference(resolution,[status(thm)],[144810440,253392288]),[]).
%
% cnf(257865096,plain,(q(s6)|n7),inference(forward_subsumption_resolution__resolution,[status(thm)],[247973272,257592000,253398080]),[]).
%
% fof(clause_18,plain,(~n5(A)|q(B)|~q(A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144629200,plain,(~n5(A)|q(B)|~q(A)),inference(rewrite,[status(thm)],[clause_18]),[]).
%
% cnf(257602680,plain,(q(A)|~q(s6)|~n6),inference(resolution,[status(thm)],[144629200,144743752]),[]).
%
% fof(clause_15,plain,(~q(s5(A))|~q(A)|n5(A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144751320,plain,(~q(s5(A))|~q(A)|n5(A)),inference(rewrite,[status(thm)],[clause_15]),[]).
%
% cnf(257632640,plain,(~q(s5(A))|~q(A)|n6),inference(resolution,[status(thm)],[144751320,144736800]),[]).
%
% cnf(257872128,plain,(n6|n7),inference(forward_subsumption_resolution__resolution,[status(thm)],[247973272,257632640,253398080]),[]).
%
% cnf(257927712,plain,(q(A)|n7),inference(forward_subsumption_resolution__resolution,[status(thm)],[257865096,257602680,257872128]),[]).
%
% cnf(258088312,plain,(n8|n7),inference(resolution,[status(thm)],[144705520,257927712]),[]).
%
% cnf(246244768,plain,(~n3|~n9|n7),inference(resolution,[status(thm)],[144885128,246052960]),[]).
%
% cnf(247160232,plain,(~n9|n7|n10),inference(resolution,[status(thm)],[246244768,246103224]),[]).
%
% cnf(247667112,plain,(~n6|n10|n7),inference(forward_subsumption_resolution__resolution,[status(thm)],[246499888,144673752,247160232]),[]).
%
% cnf(258349328,plain,(n7|n10),inference(resolution,[status(thm)],[257872128,247667112]),[]).
%
% fof(clause_36,plain,(n7|~n8|~n10),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144924336,plain,(n7|~n8|~n10),inference(rewrite,[status(thm)],[clause_36]),[]).
%
% cnf(258889824,plain,(n7),inference(forward_subsumption_resolution__resolution,[status(thm)],[258088312,258349328,144924336]),[]).
%
% cnf(247887840,plain,(n6|~n10|n7),inference(forward_subsumption_resolution__resolution,[status(thm)],[246499888,144680312,246945064]),[]).
%
% cnf(257638152,plain,(n6|~n8),inference(forward_subsumption_resolution__resolution,[status(thm)],[144629720,257632640,144629720]),[]).
%
% cnf(257967368,plain,(~n10|n6),inference(forward_subsumption_resolution__resolution,[status(thm)],[247887840,144917680,257638152]),[]).
%
% fof(clause_7,plain,(n2|~n9|~n6|n10),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144688496,plain,(n2|~n9|~n6|n10),inference(rewrite,[status(thm)],[clause_7]),[]).
%
% cnf(246568944,plain,(n2|~n10|n3),inference(resolution,[status(thm)],[246540064,246078416]),[]).
%
% cnf(248289376,plain,(n2|~n9|n3),inference(forward_subsumption_resolution__resolution,[status(thm)],[246851912,144688496,246568944]),[]).
%
% cnf(248341792,plain,(n2|n3|n4),inference(resolution,[status(thm)],[248289376,144874384]),[]).
%
% cnf(257972536,plain,(n2|n9|n6),inference(resolution,[status(thm)],[246577584,257638152]),[]).
%
% cnf(258213952,plain,(~q(A)|q(s6)|n2|n9),inference(resolution,[status(thm)],[257592000,257972536]),[]).
%
% cnf(258226496,plain,(q(s6)|n2|n9|~n3),inference(resolution,[status(thm)],[258213952,144810440]),[]).
%
% cnf(258397304,plain,(n2|n6|n4),inference(forward_subsumption_resolution__resolution,[status(thm)],[248341792,257972536,144885128]),[]).
%
% cnf(258655408,plain,(q(A)|~q(s6)|n2|n4),inference(resolution,[status(thm)],[257602680,258397304]),[]).
%
% fof(clause_29,plain,(~n3|~n4|n9),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144865736,plain,(~n3|~n4|n9),inference(rewrite,[status(thm)],[clause_29]),[]).
%
% cnf(258731792,plain,(q(A)|n2|~n3|n9),inference(forward_subsumption_resolution__resolution,[status(thm)],[258226496,258655408,144865736]),[]).
%
% cnf(264764176,plain,(q(A)|n2|n4),inference(forward_subsumption_resolution__resolution,[status(thm)],[248341792,258731792,144885128]),[]).
%
% cnf(268728680,plain,(n2|n4|n8),inference(resolution,[status(thm)],[264764176,144705520]),[]).
%
% cnf(248379544,plain,(n2|~n9|n4),inference(resolution,[status(thm)],[248289376,144885128]),[]).
%
% cnf(248455048,plain,(n2|~n9|p(A)),inference(resolution,[status(thm)],[248379544,144797672]),[]).
%
% fof(clause_3,plain,(n2|n9|~n6|~n10),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144654632,plain,(n2|n9|~n6|~n10),inference(rewrite,[status(thm)],[clause_3]),[]).
%
% cnf(250405872,plain,(n2|p(A)|~n6|~n10),inference(resolution,[status(thm)],[248455048,144654632]),[]).
%
% cnf(262653336,plain,(n2|p(A)|~n10),inference(forward_subsumption_resolution__resolution,[status(thm)],[246540064,250405872,257638152]),[]).
%
% fof(clause_33,plain,(~n7|~n8|n10),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144898216,plain,(~n7|~n8|n10),inference(rewrite,[status(thm)],[clause_33]),[]).
%
% cnf(246532440,plain,(n2|~n8|n10),inference(resolution,[status(thm)],[246499888,144898216]),[]).
%
% cnf(262694584,plain,(n2|p(A)|~n8),inference(resolution,[status(thm)],[262653336,246532440]),[]).
%
% fof(clause_19,plain,(~p(s4)|n4),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144786520,plain,(~p(s4)|n4),inference(rewrite,[status(thm)],[clause_19]),[]).
%
% cnf(262714384,plain,(n2|~n8|n4),inference(resolution,[status(thm)],[262694584,144786520]),[]).
%
% cnf(268851440,plain,(n2|n4),inference(resolution,[status(thm)],[268728680,262714384]),[]).
%
% fof(clause_24,plain,(~n2|n1(s2)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144826680,plain,(~n2|n1(s2)),inference(rewrite,[status(thm)],[clause_24]),[]).
%
% cnf(268880344,plain,(n4|n1(s2)),inference(resolution,[status(thm)],[268851440,144826680]),[]).
%
% fof(clause_27,plain,(~n1(A)|~p(A)|p(B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144852928,plain,(~n1(A)|~p(A)|p(B)),inference(rewrite,[status(thm)],[clause_27]),[]).
%
% cnf(259230960,plain,(~n1(A)|~p(A)|n4),inference(resolution,[status(thm)],[144852928,144786520]),[]).
%
% cnf(268875136,plain,(n2|p(A)),inference(resolution,[status(thm)],[268851440,144797672]),[]).
%
% fof(clause_28,plain,(~n1(A)|p(A)|~p(B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144859784,plain,(~n1(A)|p(A)|~p(B)),inference(rewrite,[status(thm)],[clause_28]),[]).
%
% fof(clause_12,plain,(~n7|p(s7)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144730248,plain,(~n7|p(s7)),inference(rewrite,[status(thm)],[clause_12]),[]).
%
% cnf(269872776,plain,(~n1(A)|p(A)),inference(forward_subsumption_resolution__resolution,[status(thm)],[258889824,144859784,144730248]),[]).
%
% cnf(269891392,plain,(p(s2)),inference(forward_subsumption_resolution__resolution,[status(thm)],[268875136,269872776,144826680]),[]).
%
% cnf(269907912,plain,(n4),inference(forward_subsumption_resolution__resolution,[status(thm)],[268880344,259230960,269891392]),[]).
%
% cnf(269001712,plain,(p(A)|n1(s2)),inference(resolution,[status(thm)],[268875136,144826680]),[]).
%
% cnf(269898672,plain,(p(A)),inference(forward_subsumption_resolution__resolution,[status(thm)],[269001712,144852928,269891392]),[]).
%
% fof(clause_25,plain,(~p(A)|~p(s1(A))|n1(A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144833568,plain,(~p(A)|~p(s1(A))|n1(A)),inference(rewrite,[status(thm)],[clause_25]),[]).
%
% cnf(270455032,plain,(n1(s7)),inference(forward_subsumption_resolution__resolution,[status(thm)],[246483144,269898672,144833568,144730248]),[]).
%
% cnf(270767352,plain,(n2),inference(resolution,[status(thm)],[270455032,144821208]),[]).
%
% cnf(270841712,plain,(n9|n3),inference(resolution,[status(thm)],[270767352,247673024]),[]).
%
% cnf(270853448,plain,(n9),inference(forward_subsumption_resolution__resolution,[status(thm)],[269907912,270841712,144865736]),[]).
%
% cnf(274518512,plain,(~n10),inference(forward_subsumption_resolution__resolution,[status(thm)],[257967368,270853448,144637152,270767352]),[]).
%
% cnf(274529520,plain,(~n8),inference(forward_subsumption_resolution__resolution,[status(thm)],[258889824,274518512,144898216]),[]).
%
% cnf(260627704,plain,(~p(s2)|p(A)|~n2),inference(resolution,[status(thm)],[144852928,144826680]),[]).
%
% cnf(260644552,plain,(~p(s2)|p(A)|n9|n6|n10),inference(resolution,[status(thm)],[260627704,144665376]),[]).
%
% cnf(260796632,plain,(~p(s2)|p(A)|n6|n10|n4),inference(forward_subsumption_resolution__resolution,[status(thm)],[246851912,260644552,144885128]),[]).
%
% cnf(260894344,plain,(~p(s2)|p(A)|n10|n4|n5(s6)),inference(resolution,[status(thm)],[260796632,144743752]),[]).
%
% cnf(261063624,plain,(~p(s2)|n10|n4|n5(s6)),inference(resolution,[status(thm)],[260894344,144786520]),[]).
%
% cnf(259002656,plain,(n8|~n10),inference(resolution,[status(thm)],[144917680,258889824]),[]).
%
% cnf(261076776,plain,(~p(s2)|n4|n5(s6)|n8),inference(resolution,[status(thm)],[261063624,259002656]),[]).
%
% cnf(246891632,plain,(n6|~n4|n9),inference(resolution,[status(thm)],[246851912,144865736]),[]).
%
% cnf(261139440,plain,(~p(s2)|n5(s6)|n8|n6|n9),inference(resolution,[status(thm)],[261076776,246891632]),[]).
%
% cnf(260636088,plain,(p(s2)|~p(A)|~n2),inference(resolution,[status(thm)],[144859784,144826680]),[]).
%
% cnf(260783312,plain,(p(s2)|~p(A)|n8|n9|n6),inference(resolution,[status(thm)],[260636088,246577584]),[]).
%
% cnf(260884264,plain,(p(s2)|~p(A)|n8|n6|n4),inference(forward_subsumption_resolution__resolution,[status(thm)],[246851912,260783312,144885128]),[]).
%
% cnf(260974432,plain,(p(s2)|~p(A)|n8|n4|n5(s6)),inference(resolution,[status(thm)],[260884264,144743752]),[]).
%
% cnf(261202456,plain,(~p(A)|n8|n5(s6)|n6|n9),inference(forward_subsumption_resolution__resolution,[status(thm)],[261139440,260974432,246891632]),[]).
%
% cnf(246390352,plain,(~n7|~n10|n3),inference(resolution,[status(thm)],[144917680,246078416]),[]).
%
% cnf(253413072,plain,(~n10|n3),inference(resolution,[status(thm)],[246390352,253392288]),[]).
%
% cnf(247834360,plain,(~n2|n9|~n10|n5(s6)),inference(resolution,[status(thm)],[144680312,144743752]),[]).
%
% cnf(255114048,plain,(~n2|~n10|n5(s6)|n4),inference(forward_subsumption_resolution__resolution,[status(thm)],[253413072,247834360,144885128]),[]).
%
% cnf(255136136,plain,(~n2|~n10|n5(s6)|p(A)),inference(resolution,[status(thm)],[255114048,144797672]),[]).
%
% cnf(255490736,plain,(~n2|n5(s6)|p(A)|~n7|~n8),inference(resolution,[status(thm)],[255136136,144898216]),[]).
%
% cnf(255876016,plain,(~n2|n5(s6)|p(A)|~n8|~p(B)),inference(resolution,[status(thm)],[255490736,144719240]),[]).
%
% cnf(263237272,plain,(n5(s6)|p(A)|~p(B)|n9|n6),inference(forward_subsumption_resolution__resolution,[status(thm)],[261202456,255876016,257972536]),[]).
%
% cnf(263263152,plain,(p(A)|~p(B)|n9|n6),inference(resolution,[status(thm)],[263237272,144736800]),[]).
%
% cnf(263286256,plain,(p(A)|~p(B)|n6|n4),inference(resolution,[status(thm)],[263263152,246903312]),[]).
%
% cnf(263307832,plain,(p(A)|~p(B)|n4|n5(s6)),inference(resolution,[status(thm)],[263286256,144743752]),[]).
%
% cnf(263358200,plain,(~p(A)|n4|n5(s6)),inference(resolution,[status(thm)],[263307832,144786520]),[]).
%
% cnf(258104904,plain,(p(s7)|q(A)),inference(resolution,[status(thm)],[144730248,257927712]),[]).
%
% cnf(246453024,plain,(n7|~n10|~q(s8)),inference(resolution,[status(thm)],[144924336,144705520]),[]).
%
% cnf(251949824,plain,(~n10|~q(s8)|p(s7)),inference(resolution,[status(thm)],[246453024,144730248]),[]).
%
% cnf(258360760,plain,(p(s7)|n10),inference(resolution,[status(thm)],[144730248,258349328]),[]).
%
% cnf(258946096,plain,(p(s7)),inference(forward_subsumption_resolution__resolution,[status(thm)],[258104904,251949824,258360760]),[]).
%
% cnf(264028432,plain,(n4|n5(s6)),inference(resolution,[status(thm)],[263358200,258946096]),[]).
%
% cnf(264091304,plain,(n5(s6)|n9),inference(forward_subsumption_resolution__resolution,[status(thm)],[246818264,264028432,144865736]),[]).
%
% cnf(264099592,plain,(n9|n6),inference(resolution,[status(thm)],[264091304,144736800]),[]).
%
% fof(clause_2,plain,(~n2|~n9|n6|n10),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144644632,plain,(~n2|~n9|n6|n10),inference(rewrite,[status(thm)],[clause_2]),[]).
%
% cnf(271823776,plain,(n6|n10),inference(forward_subsumption_resolution__resolution,[status(thm)],[264099592,144644632,270767352]),[]).
%
% cnf(271834128,plain,(n5(s6)|n10),inference(resolution,[status(thm)],[144743752,271823776]),[]).
%
% cnf(271855560,plain,(n5(s6)|n8),inference(resolution,[status(thm)],[271834128,259002656]),[]).
%
% cnf(274616032,plain,(~n5(A)|~q(A)|n8),inference(resolution,[status(thm)],[144629200,144705520]),[]).
%
% cnf(247188184,plain,(n6|n8|~n10),inference(resolution,[status(thm)],[247953960,144917680]),[]).
%
% cnf(248138952,plain,(n6|~n10|q(A)),inference(resolution,[status(thm)],[247188184,144629720]),[]).
%
% cnf(250192568,plain,(n6|q(A)|~n2|~n9),inference(resolution,[status(thm)],[248138952,144644632]),[]).
%
% cnf(245946360,plain,(q(A)|n7|n10),inference(resolution,[status(thm)],[144629720,144907208]),[]).
%
% cnf(253505952,plain,(~n9|q(A)|n7),inference(forward_subsumption_resolution__resolution,[status(thm)],[250192568,246499888,144637152,245946360]),[]).
%
% cnf(248405696,plain,(n3|n4|n1(s2)),inference(resolution,[status(thm)],[248341792,144826680]),[]).
%
% cnf(261353304,plain,(~p(s2)|p(A)|n3|n4),inference(resolution,[status(thm)],[144852928,248405696]),[]).
%
% cnf(261416472,plain,(~p(s2)|n3|n4),inference(resolution,[status(thm)],[261353304,144786520]),[]).
%
% fof(clause_32,plain,(n3|~n4|~n9),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN037-1.tptp',unknown),[]).
%
% cnf(144891688,plain,(n3|~n4|~n9),inference(rewrite,[status(thm)],[clause_32]),[]).
%
% cnf(261444104,plain,(~p(s2)|n3|~n9),inference(resolution,[status(thm)],[261416472,144891688]),[]).
%
% cnf(261360936,plain,(p(s2)|~p(A)|n3|n4),inference(resolution,[status(thm)],[144859784,248405696]),[]).
%
% cnf(261456928,plain,(~p(A)|n3|~n9),inference(forward_subsumption_resolution__resolution,[status(thm)],[261444104,261360936,144891688]),[]).
%
% cnf(265721296,plain,(~p(A)|~n9|q(s3)),inference(resolution,[status(thm)],[261456928,144810440]),[]).
%
% cnf(265781072,plain,(~n9|q(s3)),inference(forward_subsumption_resolution__resolution,[status(thm)],[253505952,265721296,144730248]),[]).
%
% cnf(266229344,plain,(~n9|n3),inference(resolution,[status(thm)],[265781072,144803456]),[]).
%
% cnf(266241160,plain,(n3|n4),inference(resolution,[status(thm)],[266229344,144874384]),[]).
%
% cnf(270893024,plain,(n3),inference(forward_subsumption_resolution__resolution,[status(thm)],[266241160,270853448,144891688]),[]).
%
% cnf(257654528,plain,(~n5(A)|q(A)|~n3),inference(resolution,[status(thm)],[144774640,144810440]),[]).
%
% cnf(264122288,plain,(n5(s6)|~n2|n6|n10),inference(resolution,[status(thm)],[264091304,144644632]),[]).
%
% cnf(264196944,plain,(n5(s6)|~n2|n6),inference(resolution,[status(thm)],[264122288,257967368]),[]).
%
% cnf(264226856,plain,(~n2|n6),inference(resolution,[status(thm)],[264196944,144736800]),[]).
%
% cnf(258134520,plain,(n5(A)|n7),inference(forward_subsumption_resolution__resolution,[status(thm)],[257927712,144751320,257927712]),[]).
%
% cnf(257581248,plain,(n5(A)|~n8),inference(forward_subsumption_resolution__resolution,[status(thm)],[144629720,144751320,144629720]),[]).
%
% cnf(263605848,plain,(n5(A)|~n10),inference(forward_subsumption_resolution__resolution,[status(thm)],[258134520,257581248,144917680]),[]).
%
% cnf(268587752,plain,(n5(A)|~n2|n9),inference(forward_subsumption_resolution__resolution,[status(thm)],[264226856,263605848,144673752]),[]).
%
% cnf(261992424,plain,(n6|~n2|~n9),inference(resolution,[status(thm)],[257967368,144644632]),[]).
%
% cnf(270471032,plain,(~n2|n5(s6)),inference(forward_subsumption_resolution__resolution,[status(thm)],[268587752,261992424,144743752]),[]).
%
% cnf(271903920,plain,(n5(s6)),inference(resolution,[status(thm)],[270471032,270767352]),[]).
%
% cnf(274727688,plain,(q(s6)),inference(forward_subsumption_resolution__resolution,[status(thm)],[270893024,257654528,271903920]),[]).
%
% cnf(274760352,plain,(n8),inference(forward_subsumption_resolution__resolution,[status(thm)],[271855560,274616032,274727688]),[]).
%
% cnf(contradiction,plain,$false,inference(resolution,[status(thm)],[274529520,274760352]),[]).
%
% END OF PROOF SEQUENCE
%
%------------------------------------------------------------------------------