%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : SYN142-1 : TPTP v3.4.2. Released v1.1.0.
% Transfm : none
% Format : tptp
% Command : faust %s
% Computer : art07.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:55:38 EDT 2009
% Result : Unsatisfiable 586.2s
% Output : Refutation 586.2s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 29
% Syntax : Number of formulae : 84 ( 37 unt; 0 def)
% Number of atoms : 165 ( 0 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 170 ( 89 ~; 81 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 21 ( 20 usr; 1 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% Number of variables : 112 ( 25 sgn 47 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Faust---1.0 format not known, defaulting to TPTP
fof(axiom_32,plain,
k0(b),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(171168264,plain,
k0(b),
inference(rewrite,[status(thm)],[axiom_32]),
[] ).
fof(rule_068,plain,
! [A] :
( p1(A,A,A)
| ~ k0(A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(171960416,plain,
( p1(A,A,A)
| ~ k0(A) ),
inference(rewrite,[status(thm)],[rule_068]),
[] ).
fof(axiom_20,plain,
l0(a),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(171107808,plain,
l0(a),
inference(rewrite,[status(thm)],[axiom_20]),
[] ).
fof(rule_050,plain,
! [A,B] :
( n1(A,B,A)
| ~ s0(b)
| ~ l0(A)
| ~ p0(b,B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
fof(axiom_14,plain,
! [A] : p0(b,A),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(171080680,plain,
p0(b,A),
inference(rewrite,[status(thm)],[axiom_14]),
[] ).
fof(axiom_5,plain,
s0(b),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(171032880,plain,
s0(b),
inference(rewrite,[status(thm)],[axiom_5]),
[] ).
cnf(171729144,plain,
( n1(A,B,A)
| ~ l0(A) ),
inference(rewrite__forward_subsumption_resolution,[status(thm)],[rule_050,171080680,171032880]),
[] ).
cnf(183993952,plain,
n1(a,A,a),
inference(resolution,[status(thm)],[171729144,171107808]),
[] ).
fof(rule_054,plain,
! [A,B,C] :
( n1(A,B,B)
| ~ l0(C)
| ~ l1(C,A)
| ~ n1(A,B,A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(171794296,plain,
( n1(A,B,B)
| ~ l0(C)
| ~ l1(C,A)
| ~ n1(A,B,A) ),
inference(rewrite,[status(thm)],[rule_054]),
[] ).
fof(rule_002,plain,
! [A,B] :
( l1(A,A)
| ~ n0(B,A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(171214400,plain,
( l1(A,A)
| ~ n0(B,A) ),
inference(rewrite,[status(thm)],[rule_002]),
[] ).
fof(axiom_37,plain,
n0(b,a),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(171186976,plain,
n0(b,a),
inference(rewrite,[status(thm)],[axiom_37]),
[] ).
cnf(185122328,plain,
l1(a,a),
inference(resolution,[status(thm)],[171214400,171186976]),
[] ).
cnf(186634736,plain,
n1(a,A,A),
inference(forward_subsumption_resolution__resolution,[status(thm)],[171107808,183993952,171794296,185122328]),
[] ).
fof(rule_182,plain,
! [A,B,C] :
( q2(A,B,A)
| ~ p1(A,A,C)
| ~ n1(B,A,C)
| ~ q2(B,C,A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(173291776,plain,
( q2(A,B,A)
| ~ p1(A,A,C)
| ~ n1(B,A,C)
| ~ q2(B,C,A) ),
inference(rewrite,[status(thm)],[rule_182]),
[] ).
fof(rule_177,plain,
! [A,B] :
( q2(A,B,B)
| ~ k0(B)
| ~ p1(A,A,A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(173221352,plain,
( q2(A,B,B)
| ~ k0(B)
| ~ p1(A,A,A) ),
inference(rewrite,[status(thm)],[rule_177]),
[] ).
fof(rule_075,plain,
( p1(a,a,a)
| ~ p0(b,a) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(172013328,plain,
p1(a,a,a),
inference(rewrite__forward_subsumption_resolution,[status(thm)],[rule_075,171080680]),
[] ).
cnf(200714584,plain,
( q2(a,A,A)
| ~ k0(A) ),
inference(resolution,[status(thm)],[173221352,172013328]),
[] ).
cnf(206325412,plain,
( q2(A,a,A)
| ~ k0(A) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[171960416,186634736,173291776,200714584]),
[] ).
fof(rule_273,plain,
! [A,B,C,D] :
( s3(A,B)
| ~ q2(C,A,C)
| ~ s2(A)
| ~ m0(C,D,B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(174574416,plain,
( s3(A,B)
| ~ q2(C,A,C)
| ~ s2(A)
| ~ m0(C,D,B) ),
inference(rewrite,[status(thm)],[rule_273]),
[] ).
fof(axiom_19,plain,
! [A,B] : m0(A,d,B),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(171103448,plain,
m0(A,d,B),
inference(rewrite,[status(thm)],[axiom_19]),
[] ).
cnf(761810552,plain,
( s3(A,B)
| ~ q2(C,A,C)
| ~ s2(A) ),
inference(resolution,[status(thm)],[174574416,171103448]),
[] ).
fof(rule_186,plain,
! [A,B] :
( q2(A,A,B)
| ~ l1(B,A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(173358184,plain,
( q2(A,A,B)
| ~ l1(B,A) ),
inference(rewrite,[status(thm)],[rule_186]),
[] ).
cnf(186559632,plain,
q2(a,a,a),
inference(resolution,[status(thm)],[173358184,185122328]),
[] ).
cnf(789039152,plain,
( s3(a,A)
| ~ s2(a) ),
inference(resolution,[status(thm)],[761810552,186559632]),
[] ).
fof(axiom_17,plain,
! [A] : q0(A,d),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(171095968,plain,
q0(A,d),
inference(rewrite,[status(thm)],[axiom_17]),
[] ).
fof(rule_126,plain,
! [A,B,C] :
( s1(A)
| ~ q0(A,B)
| ~ s1(C) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(172520056,plain,
( s1(A)
| ~ q0(A,B)
| ~ s1(C) ),
inference(rewrite,[status(thm)],[rule_126]),
[] ).
cnf(189180952,plain,
( s1(A)
| ~ s1(B) ),
inference(resolution,[status(thm)],[171095968,172520056]),
[] ).
fof(rule_125,plain,
! [A] :
( s1(A)
| ~ p0(A,A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(172507912,plain,
( s1(A)
| ~ p0(A,A) ),
inference(rewrite,[status(thm)],[rule_125]),
[] ).
cnf(185462072,plain,
s1(b),
inference(resolution,[status(thm)],[172507912,171080680]),
[] ).
cnf(189185360,plain,
s1(A),
inference(resolution,[status(thm)],[189180952,185462072]),
[] ).
fof(rule_133,plain,
! [A,B,C,D] :
( l2(A,A)
| ~ p0(B,B)
| ~ s1(C)
| ~ m0(D,C,A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(172629000,plain,
( l2(A,A)
| ~ p0(B,B)
| ~ s1(C)
| ~ m0(D,C,A) ),
inference(rewrite,[status(thm)],[rule_133]),
[] ).
cnf(185657088,plain,
( l2(A,A)
| ~ s1(B)
| ~ m0(C,B,A) ),
inference(resolution,[status(thm)],[172629000,171080680]),
[] ).
cnf(194791256,plain,
l2(A,A),
inference(forward_subsumption_resolution__resolution,[status(thm)],[189185360,185657088,171103448]),
[] ).
fof(axiom_34,plain,
n0(c,d),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(171175720,plain,
n0(c,d),
inference(rewrite,[status(thm)],[axiom_34]),
[] ).
cnf(188367664,plain,
l1(d,d),
inference(resolution,[status(thm)],[171175720,171214400]),
[] ).
fof(rule_299,plain,
! [A,B,C,D] :
( s4(A)
| ~ p3(B,C,D)
| ~ l1(A,C) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(174927960,plain,
( s4(A)
| ~ p3(B,C,D)
| ~ l1(A,C) ),
inference(rewrite,[status(thm)],[rule_299]),
[] ).
fof(rule_244,plain,
! [A] :
( p3(A,A,A)
| ~ n2(A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(174163728,plain,
( p3(A,A,A)
| ~ n2(A) ),
inference(rewrite,[status(thm)],[rule_244]),
[] ).
fof(rule_137,plain,
! [A,B,C] :
( n2(A)
| ~ p1(B,C,A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(172683632,plain,
( n2(A)
| ~ p1(B,C,A) ),
inference(rewrite,[status(thm)],[rule_137]),
[] ).
fof(rule_072,plain,
! [A,B] :
( p1(A,A,A)
| ~ s0(B)
| ~ s0(A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(172007240,plain,
( p1(A,A,A)
| ~ s0(B)
| ~ s0(A) ),
inference(rewrite,[status(thm)],[rule_072]),
[] ).
fof(axiom_1,plain,
s0(d),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(170992632,plain,
s0(d),
inference(rewrite,[status(thm)],[axiom_1]),
[] ).
cnf(183708792,plain,
p1(d,d,d),
inference(resolution,[status(thm)],[172007240,170992632]),
[] ).
cnf(187799560,plain,
n2(d),
inference(resolution,[status(thm)],[172683632,183708792]),
[] ).
cnf(187931000,plain,
p3(d,d,d),
inference(resolution,[status(thm)],[174163728,187799560]),
[] ).
cnf(193349296,plain,
( s4(A)
| ~ l1(A,d) ),
inference(resolution,[status(thm)],[174927960,187931000]),
[] ).
fof(rule_305,plain,
! [A] :
( m5(A,A)
| ~ s4(A)
| ~ m4(e,e) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(175018192,plain,
( m5(A,A)
| ~ s4(A)
| ~ m4(e,e) ),
inference(rewrite,[status(thm)],[rule_305]),
[] ).
fof(prove_this,plain,
! [A] : ~ m5(d,A),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(175376912,plain,
~ m5(d,A),
inference(rewrite,[status(thm)],[prove_this]),
[] ).
cnf(187759312,plain,
( ~ s4(d)
| ~ m4(e,e) ),
inference(resolution,[status(thm)],[175018192,175376912]),
[] ).
cnf(193817328,plain,
~ m4(e,e),
inference(forward_subsumption_resolution__resolution,[status(thm)],[188367664,193349296,187759312]),
[] ).
fof(rule_279,plain,
! [A,B,C] :
( m4(A,B)
| ~ l2(C,B)
| ~ s3(a,A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(174657032,plain,
( m4(A,B)
| ~ l2(C,B)
| ~ s3(a,A) ),
inference(rewrite,[status(thm)],[rule_279]),
[] ).
cnf(193877592,plain,
( ~ l2(A,e)
| ~ s3(a,e) ),
inference(resolution,[status(thm)],[193817328,174657032]),
[] ).
cnf(195293160,plain,
~ s3(a,e),
inference(resolution,[status(thm)],[194791256,193877592]),
[] ).
cnf(789096840,plain,
~ s2(a),
inference(resolution,[status(thm)],[789039152,195293160]),
[] ).
fof(rule_189,plain,
! [A] :
( s2(A)
| ~ q2(b,A,b)
| ~ s1(b) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),
[] ).
cnf(173402272,plain,
( s2(A)
| ~ q2(b,A,b)
| ~ s1(b) ),
inference(rewrite,[status(thm)],[rule_189]),
[] ).
cnf(185772960,plain,
( s2(A)
| ~ q2(b,A,b) ),
inference(resolution,[status(thm)],[173402272,185462072]),
[] ).
cnf(789125168,plain,
~ q2(b,a,b),
inference(resolution,[status(thm)],[789096840,185772960]),
[] ).
cnf(contradiction,plain,
$false,
inference(forward_subsumption_resolution__resolution,[status(thm)],[171168264,206325412,789125168]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 804 seconds
% START OF PROOF SEQUENCE
% fof(axiom_32,plain,(k0(b)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(171168264,plain,(k0(b)),inference(rewrite,[status(thm)],[axiom_32]),[]).
%
% fof(rule_068,plain,(p1(A,A,A)|~k0(A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(171960416,plain,(p1(A,A,A)|~k0(A)),inference(rewrite,[status(thm)],[rule_068]),[]).
%
% fof(axiom_20,plain,(l0(a)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(171107808,plain,(l0(a)),inference(rewrite,[status(thm)],[axiom_20]),[]).
%
% fof(rule_050,plain,(n1(A,B,A)|~s0(b)|~l0(A)|~p0(b,B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% fof(axiom_14,plain,(p0(b,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(171080680,plain,(p0(b,A)),inference(rewrite,[status(thm)],[axiom_14]),[]).
%
% fof(axiom_5,plain,(s0(b)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(171032880,plain,(s0(b)),inference(rewrite,[status(thm)],[axiom_5]),[]).
%
% cnf(171729144,plain,(n1(A,B,A)|~l0(A)),inference(rewrite__forward_subsumption_resolution,[status(thm)],[rule_050,171080680,171032880]),[]).
%
% cnf(183993952,plain,(n1(a,A,a)),inference(resolution,[status(thm)],[171729144,171107808]),[]).
%
% fof(rule_054,plain,(n1(A,B,B)|~l0(C)|~l1(C,A)|~n1(A,B,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(171794296,plain,(n1(A,B,B)|~l0(C)|~l1(C,A)|~n1(A,B,A)),inference(rewrite,[status(thm)],[rule_054]),[]).
%
% fof(rule_002,plain,(l1(A,A)|~n0(B,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(171214400,plain,(l1(A,A)|~n0(B,A)),inference(rewrite,[status(thm)],[rule_002]),[]).
%
% fof(axiom_37,plain,(n0(b,a)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(171186976,plain,(n0(b,a)),inference(rewrite,[status(thm)],[axiom_37]),[]).
%
% cnf(185122328,plain,(l1(a,a)),inference(resolution,[status(thm)],[171214400,171186976]),[]).
%
% cnf(186634736,plain,(n1(a,A,A)),inference(forward_subsumption_resolution__resolution,[status(thm)],[171107808,183993952,171794296,185122328]),[]).
%
% fof(rule_182,plain,(q2(A,B,A)|~p1(A,A,C)|~n1(B,A,C)|~q2(B,C,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(173291776,plain,(q2(A,B,A)|~p1(A,A,C)|~n1(B,A,C)|~q2(B,C,A)),inference(rewrite,[status(thm)],[rule_182]),[]).
%
% fof(rule_177,plain,(q2(A,B,B)|~k0(B)|~p1(A,A,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(173221352,plain,(q2(A,B,B)|~k0(B)|~p1(A,A,A)),inference(rewrite,[status(thm)],[rule_177]),[]).
%
% fof(rule_075,plain,(p1(a,a,a)|~p0(b,a)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(172013328,plain,(p1(a,a,a)),inference(rewrite__forward_subsumption_resolution,[status(thm)],[rule_075,171080680]),[]).
%
% cnf(200714584,plain,(q2(a,A,A)|~k0(A)),inference(resolution,[status(thm)],[173221352,172013328]),[]).
%
% cnf(206325412,plain,(q2(A,a,A)|~k0(A)),inference(forward_subsumption_resolution__resolution,[status(thm)],[171960416,186634736,173291776,200714584]),[]).
%
% fof(rule_273,plain,(s3(A,B)|~q2(C,A,C)|~s2(A)|~m0(C,D,B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(174574416,plain,(s3(A,B)|~q2(C,A,C)|~s2(A)|~m0(C,D,B)),inference(rewrite,[status(thm)],[rule_273]),[]).
%
% fof(axiom_19,plain,(m0(A,d,B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(171103448,plain,(m0(A,d,B)),inference(rewrite,[status(thm)],[axiom_19]),[]).
%
% cnf(761810552,plain,(s3(A,B)|~q2(C,A,C)|~s2(A)),inference(resolution,[status(thm)],[174574416,171103448]),[]).
%
% fof(rule_186,plain,(q2(A,A,B)|~l1(B,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(173358184,plain,(q2(A,A,B)|~l1(B,A)),inference(rewrite,[status(thm)],[rule_186]),[]).
%
% cnf(186559632,plain,(q2(a,a,a)),inference(resolution,[status(thm)],[173358184,185122328]),[]).
%
% cnf(789039152,plain,(s3(a,A)|~s2(a)),inference(resolution,[status(thm)],[761810552,186559632]),[]).
%
% fof(axiom_17,plain,(q0(A,d)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(171095968,plain,(q0(A,d)),inference(rewrite,[status(thm)],[axiom_17]),[]).
%
% fof(rule_126,plain,(s1(A)|~q0(A,B)|~s1(C)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(172520056,plain,(s1(A)|~q0(A,B)|~s1(C)),inference(rewrite,[status(thm)],[rule_126]),[]).
%
% cnf(189180952,plain,(s1(A)|~s1(B)),inference(resolution,[status(thm)],[171095968,172520056]),[]).
%
% fof(rule_125,plain,(s1(A)|~p0(A,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(172507912,plain,(s1(A)|~p0(A,A)),inference(rewrite,[status(thm)],[rule_125]),[]).
%
% cnf(185462072,plain,(s1(b)),inference(resolution,[status(thm)],[172507912,171080680]),[]).
%
% cnf(189185360,plain,(s1(A)),inference(resolution,[status(thm)],[189180952,185462072]),[]).
%
% fof(rule_133,plain,(l2(A,A)|~p0(B,B)|~s1(C)|~m0(D,C,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(172629000,plain,(l2(A,A)|~p0(B,B)|~s1(C)|~m0(D,C,A)),inference(rewrite,[status(thm)],[rule_133]),[]).
%
% cnf(185657088,plain,(l2(A,A)|~s1(B)|~m0(C,B,A)),inference(resolution,[status(thm)],[172629000,171080680]),[]).
%
% cnf(194791256,plain,(l2(A,A)),inference(forward_subsumption_resolution__resolution,[status(thm)],[189185360,185657088,171103448]),[]).
%
% fof(axiom_34,plain,(n0(c,d)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(171175720,plain,(n0(c,d)),inference(rewrite,[status(thm)],[axiom_34]),[]).
%
% cnf(188367664,plain,(l1(d,d)),inference(resolution,[status(thm)],[171175720,171214400]),[]).
%
% fof(rule_299,plain,(s4(A)|~p3(B,C,D)|~l1(A,C)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(174927960,plain,(s4(A)|~p3(B,C,D)|~l1(A,C)),inference(rewrite,[status(thm)],[rule_299]),[]).
%
% fof(rule_244,plain,(p3(A,A,A)|~n2(A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(174163728,plain,(p3(A,A,A)|~n2(A)),inference(rewrite,[status(thm)],[rule_244]),[]).
%
% fof(rule_137,plain,(n2(A)|~p1(B,C,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(172683632,plain,(n2(A)|~p1(B,C,A)),inference(rewrite,[status(thm)],[rule_137]),[]).
%
% fof(rule_072,plain,(p1(A,A,A)|~s0(B)|~s0(A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(172007240,plain,(p1(A,A,A)|~s0(B)|~s0(A)),inference(rewrite,[status(thm)],[rule_072]),[]).
%
% fof(axiom_1,plain,(s0(d)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(170992632,plain,(s0(d)),inference(rewrite,[status(thm)],[axiom_1]),[]).
%
% cnf(183708792,plain,(p1(d,d,d)),inference(resolution,[status(thm)],[172007240,170992632]),[]).
%
% cnf(187799560,plain,(n2(d)),inference(resolution,[status(thm)],[172683632,183708792]),[]).
%
% cnf(187931000,plain,(p3(d,d,d)),inference(resolution,[status(thm)],[174163728,187799560]),[]).
%
% cnf(193349296,plain,(s4(A)|~l1(A,d)),inference(resolution,[status(thm)],[174927960,187931000]),[]).
%
% fof(rule_305,plain,(m5(A,A)|~s4(A)|~m4(e,e)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(175018192,plain,(m5(A,A)|~s4(A)|~m4(e,e)),inference(rewrite,[status(thm)],[rule_305]),[]).
%
% fof(prove_this,plain,(~m5(d,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(175376912,plain,(~m5(d,A)),inference(rewrite,[status(thm)],[prove_this]),[]).
%
% cnf(187759312,plain,(~s4(d)|~m4(e,e)),inference(resolution,[status(thm)],[175018192,175376912]),[]).
%
% cnf(193817328,plain,(~m4(e,e)),inference(forward_subsumption_resolution__resolution,[status(thm)],[188367664,193349296,187759312]),[]).
%
% fof(rule_279,plain,(m4(A,B)|~l2(C,B)|~s3(a,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(174657032,plain,(m4(A,B)|~l2(C,B)|~s3(a,A)),inference(rewrite,[status(thm)],[rule_279]),[]).
%
% cnf(193877592,plain,(~l2(A,e)|~s3(a,e)),inference(resolution,[status(thm)],[193817328,174657032]),[]).
%
% cnf(195293160,plain,(~s3(a,e)),inference(resolution,[status(thm)],[194791256,193877592]),[]).
%
% cnf(789096840,plain,(~s2(a)),inference(resolution,[status(thm)],[789039152,195293160]),[]).
%
% fof(rule_189,plain,(s2(A)|~q2(b,A,b)|~s1(b)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN142-1.tptp',unknown),[]).
%
% cnf(173402272,plain,(s2(A)|~q2(b,A,b)|~s1(b)),inference(rewrite,[status(thm)],[rule_189]),[]).
%
% cnf(185772960,plain,(s2(A)|~q2(b,A,b)),inference(resolution,[status(thm)],[173402272,185462072]),[]).
%
% cnf(789125168,plain,(~q2(b,a,b)),inference(resolution,[status(thm)],[789096840,185772960]),[]).
%
% cnf(contradiction,plain,$false,inference(forward_subsumption_resolution__resolution,[status(thm)],[171168264,206325412,789125168]),[]).
%
% END OF PROOF SEQUENCE
%
%------------------------------------------------------------------------------