%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : SYN587-1 : TPTP v3.4.2. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : faust %s
% Computer : art04.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 18:16:22 EDT 2009
% Result : Unsatisfiable 0.3s
% Output : Refutation 0.3s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 7
% Syntax : Number of formulae : 22 ( 12 unt; 0 def)
% Number of atoms : 41 ( 0 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 40 ( 21 ~; 19 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 6 con; 0-2 aty)
% Number of variables : 34 ( 0 sgn 12 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Faust---1.0 format not known, defaulting to TPTP
fof(p15_17,plain,
! [A,B,C,D] :
( p15(A,B)
| ~ p2(C,A)
| ~ p2(D,B)
| ~ p15(C,D) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN587-1.tptp',unknown),
[] ).
cnf(164636344,plain,
( p15(A,B)
| ~ p2(C,A)
| ~ p2(D,B)
| ~ p15(C,D) ),
inference(rewrite,[status(thm)],[p15_17]),
[] ).
fof(p2_4,plain,
! [A] : p2(A,A),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN587-1.tptp',unknown),
[] ).
cnf(164525576,plain,
p2(A,A),
inference(rewrite,[status(thm)],[p2_4]),
[] ).
cnf(238946376,plain,
( p15(A,B)
| ~ p2(C,A)
| ~ p15(C,B) ),
inference(resolution,[status(thm)],[164636344,164525576]),
[] ).
fof(p15_18,plain,
p15(f4(f6(f10(c16),f6(f7(f8(f9(c17))),c18)),c19),c20),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN587-1.tptp',unknown),
[] ).
cnf(164507440,plain,
p15(f4(f6(f10(c16),f6(f7(f8(f9(c17))),c18)),c19),c20),
inference(rewrite,[status(thm)],[p15_18]),
[] ).
cnf(239394928,plain,
( p15(A,c20)
| ~ p2(f4(f6(f10(c16),f6(f7(f8(f9(c17))),c18)),c19),A) ),
inference(resolution,[status(thm)],[238946376,164507440]),
[] ).
fof(p2_16,plain,
! [A,B,C] :
( p2(A,B)
| ~ p2(C,A)
| ~ p2(C,B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN587-1.tptp',unknown),
[] ).
cnf(164622024,plain,
( p2(A,B)
| ~ p2(C,A)
| ~ p2(C,B) ),
inference(rewrite,[status(thm)],[p2_16]),
[] ).
cnf(238936704,plain,
( p2(A,B)
| ~ p2(B,A) ),
inference(resolution,[status(thm)],[164622024,164525576]),
[] ).
fof(p2_20,plain,
! [A,B,C,D] :
( p2(f4(A,B),f4(C,D))
| ~ p2(A,C)
| ~ p3(B,D) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN587-1.tptp',unknown),
[] ).
cnf(164662208,plain,
( p2(f4(A,B),f4(C,D))
| ~ p2(A,C)
| ~ p3(B,D) ),
inference(rewrite,[status(thm)],[p2_20]),
[] ).
fof(p3_5,plain,
p3(c21,c19),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN587-1.tptp',unknown),
[] ).
cnf(164534048,plain,
p3(c21,c19),
inference(rewrite,[status(thm)],[p3_5]),
[] ).
cnf(239134904,plain,
( p2(f4(A,c21),f4(B,c19))
| ~ p2(A,B) ),
inference(resolution,[status(thm)],[164662208,164534048]),
[] ).
cnf(239147168,plain,
p2(f4(A,c21),f4(A,c19)),
inference(resolution,[status(thm)],[239134904,164525576]),
[] ).
cnf(239274712,plain,
p2(f4(A,c19),f4(A,c21)),
inference(resolution,[status(thm)],[238936704,239147168]),
[] ).
cnf(239399432,plain,
p15(f4(f6(f10(c16),f6(f7(f8(f9(c17))),c18)),c21),c20),
inference(resolution,[status(thm)],[239394928,239274712]),
[] ).
fof(not_p15_19,plain,
~ p15(f4(f6(f10(c16),f6(f7(f8(f9(c17))),c18)),c21),c20),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN587-1.tptp',unknown),
[] ).
cnf(164654496,plain,
~ p15(f4(f6(f10(c16),f6(f7(f8(f9(c17))),c18)),c21),c20),
inference(rewrite,[status(thm)],[not_p15_19]),
[] ).
cnf(contradiction,plain,
$false,
inference(resolution,[status(thm)],[239399432,164654496]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 1 seconds
% START OF PROOF SEQUENCE
% fof(p15_17,plain,(p15(A,B)|~p2(C,A)|~p2(D,B)|~p15(C,D)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN587-1.tptp',unknown),[]).
%
% cnf(164636344,plain,(p15(A,B)|~p2(C,A)|~p2(D,B)|~p15(C,D)),inference(rewrite,[status(thm)],[p15_17]),[]).
%
% fof(p2_4,plain,(p2(A,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN587-1.tptp',unknown),[]).
%
% cnf(164525576,plain,(p2(A,A)),inference(rewrite,[status(thm)],[p2_4]),[]).
%
% cnf(238946376,plain,(p15(A,B)|~p2(C,A)|~p15(C,B)),inference(resolution,[status(thm)],[164636344,164525576]),[]).
%
% fof(p15_18,plain,(p15(f4(f6(f10(c16),f6(f7(f8(f9(c17))),c18)),c19),c20)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN587-1.tptp',unknown),[]).
%
% cnf(164507440,plain,(p15(f4(f6(f10(c16),f6(f7(f8(f9(c17))),c18)),c19),c20)),inference(rewrite,[status(thm)],[p15_18]),[]).
%
% cnf(239394928,plain,(p15(A,c20)|~p2(f4(f6(f10(c16),f6(f7(f8(f9(c17))),c18)),c19),A)),inference(resolution,[status(thm)],[238946376,164507440]),[]).
%
% fof(p2_16,plain,(p2(A,B)|~p2(C,A)|~p2(C,B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN587-1.tptp',unknown),[]).
%
% cnf(164622024,plain,(p2(A,B)|~p2(C,A)|~p2(C,B)),inference(rewrite,[status(thm)],[p2_16]),[]).
%
% cnf(238936704,plain,(p2(A,B)|~p2(B,A)),inference(resolution,[status(thm)],[164622024,164525576]),[]).
%
% fof(p2_20,plain,(p2(f4(A,B),f4(C,D))|~p2(A,C)|~p3(B,D)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN587-1.tptp',unknown),[]).
%
% cnf(164662208,plain,(p2(f4(A,B),f4(C,D))|~p2(A,C)|~p3(B,D)),inference(rewrite,[status(thm)],[p2_20]),[]).
%
% fof(p3_5,plain,(p3(c21,c19)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN587-1.tptp',unknown),[]).
%
% cnf(164534048,plain,(p3(c21,c19)),inference(rewrite,[status(thm)],[p3_5]),[]).
%
% cnf(239134904,plain,(p2(f4(A,c21),f4(B,c19))|~p2(A,B)),inference(resolution,[status(thm)],[164662208,164534048]),[]).
%
% cnf(239147168,plain,(p2(f4(A,c21),f4(A,c19))),inference(resolution,[status(thm)],[239134904,164525576]),[]).
%
% cnf(239274712,plain,(p2(f4(A,c19),f4(A,c21))),inference(resolution,[status(thm)],[238936704,239147168]),[]).
%
% cnf(239399432,plain,(p15(f4(f6(f10(c16),f6(f7(f8(f9(c17))),c18)),c21),c20)),inference(resolution,[status(thm)],[239394928,239274712]),[]).
%
% fof(not_p15_19,plain,(~p15(f4(f6(f10(c16),f6(f7(f8(f9(c17))),c18)),c21),c20)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN587-1.tptp',unknown),[]).
%
% cnf(164654496,plain,(~p15(f4(f6(f10(c16),f6(f7(f8(f9(c17))),c18)),c21),c20)),inference(rewrite,[status(thm)],[not_p15_19]),[]).
%
% cnf(contradiction,plain,$false,inference(resolution,[status(thm)],[239399432,164654496]),[]).
%
% END OF PROOF SEQUENCE
%
%------------------------------------------------------------------------------