%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : SET012-4 : TPTP v3.4.2. Bugfixed v1.2.1.
% 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 15:23:20 EDT 2009
% Result : Unsatisfiable 0.4s
% Output : Refutation 0.4s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 9
% Syntax : Number of formulae : 31 ( 12 unt; 0 def)
% Number of atoms : 58 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 52 ( 25 ~; 27 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 29 ( 1 sgn 12 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Faust---1.0 format not known, defaulting to TPTP
fof(extensionality1,plain,
! [A,B] :
( little_set(f1(A,B))
| $equal(B,A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SET/SET012-4.tptp',unknown),
[] ).
cnf(157060288,plain,
( little_set(f1(A,B))
| $equal(B,A) ),
inference(rewrite,[status(thm)],[extensionality1]),
[] ).
fof(prove_a_equals_c,plain,
~ $equal(cs,as),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SET/SET012-4.tptp',unknown),
[] ).
cnf(157120520,plain,
~ $equal(cs,as),
inference(rewrite,[status(thm)],[prove_a_equals_c]),
[] ).
cnf(164981920,plain,
little_set(f1(as,cs)),
inference(resolution,[status(thm)],[157060288,157120520]),
[] ).
fof(a2,plain,
! [A,B] :
( ~ member(A,B)
| little_set(A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SET/SET012-4.tptp',unknown),
[] ).
cnf(157050360,plain,
( ~ member(A,B)
| little_set(A) ),
inference(rewrite,[status(thm)],[a2]),
[] ).
fof(complement2,plain,
! [A,B] :
( member(A,complement(B))
| ~ little_set(A)
| member(A,B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SET/SET012-4.tptp',unknown),
[] ).
cnf(157093312,plain,
( member(A,complement(B))
| ~ little_set(A)
| member(A,B) ),
inference(rewrite,[status(thm)],[complement2]),
[] ).
fof(complement_of_a_is_b,plain,
$equal(complement(as),bs),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SET/SET012-4.tptp',unknown),
[] ).
cnf(157111744,plain,
$equal(complement(as),bs),
inference(rewrite,[status(thm)],[complement_of_a_is_b]),
[] ).
cnf(165718680,plain,
( member(A,bs)
| ~ little_set(A)
| member(A,as) ),
inference(paramodulation,[status(thm)],[157093312,157111744,theory(equality)]),
[] ).
fof(complement1,plain,
! [A,B] :
( ~ member(A,complement(B))
| ~ member(A,B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SET/SET012-4.tptp',unknown),
[] ).
cnf(157085832,plain,
( ~ member(A,complement(B))
| ~ member(A,B) ),
inference(rewrite,[status(thm)],[complement1]),
[] ).
fof(complement_of_b_is_c,plain,
$equal(complement(bs),cs),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SET/SET012-4.tptp',unknown),
[] ).
cnf(157046104,plain,
$equal(complement(bs),cs),
inference(rewrite,[status(thm)],[complement_of_b_is_c]),
[] ).
cnf(165442096,plain,
( ~ member(A,cs)
| ~ member(A,bs) ),
inference(paramodulation,[status(thm)],[157085832,157046104,theory(equality)]),
[] ).
cnf(169940712,plain,
( member(A,as)
| ~ member(A,cs) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[157050360,165718680,165442096]),
[] ).
fof(extensionality2,plain,
! [A,B] :
( member(f1(A,B),A)
| member(f1(A,B),B)
| $equal(B,A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SET/SET012-4.tptp',unknown),
[] ).
cnf(157068664,plain,
( member(f1(A,B),A)
| member(f1(A,B),B)
| $equal(B,A) ),
inference(rewrite,[status(thm)],[extensionality2]),
[] ).
cnf(165052880,plain,
( member(f1(as,cs),as)
| member(f1(as,cs),cs) ),
inference(resolution,[status(thm)],[157120520,157068664]),
[] ).
cnf(170544824,plain,
member(f1(as,cs),as),
inference(resolution,[status(thm)],[169940712,165052880]),
[] ).
cnf(170642888,plain,
~ member(f1(as,cs),complement(as)),
inference(resolution,[status(thm)],[170544824,157085832]),
[] ).
cnf(165426712,plain,
( ~ member(A,bs)
| ~ member(A,as) ),
inference(paramodulation,[status(thm)],[157085832,157111744,theory(equality)]),
[] ).
cnf(170651272,plain,
~ member(f1(as,cs),bs),
inference(resolution,[status(thm)],[170544824,165426712]),
[] ).
cnf(165726600,plain,
( member(A,cs)
| ~ little_set(A)
| member(A,bs) ),
inference(paramodulation,[status(thm)],[157093312,157046104,theory(equality)]),
[] ).
cnf(170715888,plain,
member(f1(as,cs),cs),
inference(forward_subsumption_resolution__resolution,[status(thm)],[164981920,170651272,165726600]),
[] ).
fof(extensionality3,plain,
! [A,B] :
( ~ member(f1(A,B),A)
| ~ member(f1(A,B),B)
| $equal(B,A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SET/SET012-4.tptp',unknown),
[] ).
cnf(157076256,plain,
( ~ member(f1(A,B),A)
| ~ member(f1(A,B),B)
| $equal(B,A) ),
inference(rewrite,[status(thm)],[extensionality3]),
[] ).
cnf(165008888,plain,
( ~ member(f1(as,cs),as)
| ~ member(f1(as,cs),cs) ),
inference(resolution,[status(thm)],[157076256,157120520]),
[] ).
cnf(contradiction,plain,
$false,
inference(forward_subsumption_resolution__resolution,[status(thm)],[164981920,170642888,170715888,157093312,165008888]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 0 seconds
% START OF PROOF SEQUENCE
% fof(extensionality1,plain,(little_set(f1(A,B))|$equal(B,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SET/SET012-4.tptp',unknown),[]).
%
% cnf(157060288,plain,(little_set(f1(A,B))|$equal(B,A)),inference(rewrite,[status(thm)],[extensionality1]),[]).
%
% fof(prove_a_equals_c,plain,(~$equal(cs,as)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SET/SET012-4.tptp',unknown),[]).
%
% cnf(157120520,plain,(~$equal(cs,as)),inference(rewrite,[status(thm)],[prove_a_equals_c]),[]).
%
% cnf(164981920,plain,(little_set(f1(as,cs))),inference(resolution,[status(thm)],[157060288,157120520]),[]).
%
% fof(a2,plain,(~member(A,B)|little_set(A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SET/SET012-4.tptp',unknown),[]).
%
% cnf(157050360,plain,(~member(A,B)|little_set(A)),inference(rewrite,[status(thm)],[a2]),[]).
%
% fof(complement2,plain,(member(A,complement(B))|~little_set(A)|member(A,B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SET/SET012-4.tptp',unknown),[]).
%
% cnf(157093312,plain,(member(A,complement(B))|~little_set(A)|member(A,B)),inference(rewrite,[status(thm)],[complement2]),[]).
%
% fof(complement_of_a_is_b,plain,($equal(complement(as),bs)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SET/SET012-4.tptp',unknown),[]).
%
% cnf(157111744,plain,($equal(complement(as),bs)),inference(rewrite,[status(thm)],[complement_of_a_is_b]),[]).
%
% cnf(165718680,plain,(member(A,bs)|~little_set(A)|member(A,as)),inference(paramodulation,[status(thm)],[157093312,157111744,theory(equality)]),[]).
%
% fof(complement1,plain,(~member(A,complement(B))|~member(A,B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SET/SET012-4.tptp',unknown),[]).
%
% cnf(157085832,plain,(~member(A,complement(B))|~member(A,B)),inference(rewrite,[status(thm)],[complement1]),[]).
%
% fof(complement_of_b_is_c,plain,($equal(complement(bs),cs)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SET/SET012-4.tptp',unknown),[]).
%
% cnf(157046104,plain,($equal(complement(bs),cs)),inference(rewrite,[status(thm)],[complement_of_b_is_c]),[]).
%
% cnf(165442096,plain,(~member(A,cs)|~member(A,bs)),inference(paramodulation,[status(thm)],[157085832,157046104,theory(equality)]),[]).
%
% cnf(169940712,plain,(member(A,as)|~member(A,cs)),inference(forward_subsumption_resolution__resolution,[status(thm)],[157050360,165718680,165442096]),[]).
%
% fof(extensionality2,plain,(member(f1(A,B),A)|member(f1(A,B),B)|$equal(B,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SET/SET012-4.tptp',unknown),[]).
%
% cnf(157068664,plain,(member(f1(A,B),A)|member(f1(A,B),B)|$equal(B,A)),inference(rewrite,[status(thm)],[extensionality2]),[]).
%
% cnf(165052880,plain,(member(f1(as,cs),as)|member(f1(as,cs),cs)),inference(resolution,[status(thm)],[157120520,157068664]),[]).
%
% cnf(170544824,plain,(member(f1(as,cs),as)),inference(resolution,[status(thm)],[169940712,165052880]),[]).
%
% cnf(170642888,plain,(~member(f1(as,cs),complement(as))),inference(resolution,[status(thm)],[170544824,157085832]),[]).
%
% cnf(165426712,plain,(~member(A,bs)|~member(A,as)),inference(paramodulation,[status(thm)],[157085832,157111744,theory(equality)]),[]).
%
% cnf(170651272,plain,(~member(f1(as,cs),bs)),inference(resolution,[status(thm)],[170544824,165426712]),[]).
%
% cnf(165726600,plain,(member(A,cs)|~little_set(A)|member(A,bs)),inference(paramodulation,[status(thm)],[157093312,157046104,theory(equality)]),[]).
%
% cnf(170715888,plain,(member(f1(as,cs),cs)),inference(forward_subsumption_resolution__resolution,[status(thm)],[164981920,170651272,165726600]),[]).
%
% fof(extensionality3,plain,(~member(f1(A,B),A)|~member(f1(A,B),B)|$equal(B,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SET/SET012-4.tptp',unknown),[]).
%
% cnf(157076256,plain,(~member(f1(A,B),A)|~member(f1(A,B),B)|$equal(B,A)),inference(rewrite,[status(thm)],[extensionality3]),[]).
%
% cnf(165008888,plain,(~member(f1(as,cs),as)|~member(f1(as,cs),cs)),inference(resolution,[status(thm)],[157076256,157120520]),[]).
%
% cnf(contradiction,plain,$false,inference(forward_subsumption_resolution__resolution,[status(thm)],[164981920,170642888,170715888,157093312,165008888]),[]).
%
% END OF PROOF SEQUENCE
%
%------------------------------------------------------------------------------