fCube Prover

% 6,333 inferences, 0.001 CPU in 0.001 seconds (100% CPU, 5101202 Lips)

This is Fcube
Copyright (C) 2012
Mauro Ferrari,      email: [email protected],
Camillo Fiorentini, email: [email protected]
Guido Fiorino,      email: [email protected]
This program comes with ABSOLUTELY NO WARRANTY.
This is free software, and you are welcome to redistribute it
under  conditions  GNU  Public License, see <http://www.gnu.org/licenses/> for details.
Input Formula:
F (((p&(q => r)) => s) <=> ((~p | (q | s))&(~p | (~r | s))))

Sign Permanence tried,input formula equivalent to: 
   F (((p&(q => r)) => s) <=> ((~p | (q | s))&(~p | (~r | s))));
Left branch of F equiv,Main SWFF: F (((~p | (q | s))&(~p | (s | ~r))) <=> ((p&(q => r)) => s))

      F (((~p | (q | s))&(~p | (s | ~r))) => ((p&(q => r)) => s));
 
F->,Main SWFF: F (((~p | (q | s))&(~p | (s | ~r))) => ((p&(q => r)) => s))

         T ((~p | (q | s))&(~p | (s | ~r)));
         F ((p&(q => r)) => s);
 
Main SWFF: T ((~p | (q | s))&(~p | (s | ~r)))

            T (~p | (q | s));
            T (~p | (s | ~r));
            F ((p&(q => r)) => s);
 
Branch of T or,Disjunct: ~p of Main SWFF: T (~p | (q | s))

               T p;
               T r;
               FC q;
               FC s;
               T 0;
               F ~p;
 
Branch of T or,Disjunct: q of Main SWFF: T (~p | (q | s))

               T q;
               T (~p | (s | ~r));
               F ((p&r) => s);
 
Branch of T or,Disjunct: ~p of Main SWFF: T (~p | (s | ~r))

                  T p;
                  T r;
                  FC s;
                  T 0;
                  F ~p;
                  T q;
 
Branch of T or,Disjunct: s of Main SWFF: T (~p | (s | ~r))

                  T s;
                  F 1;
                  T q;
 
Branch of T or,Disjunct: ~r of Main SWFF: T (~p | (s | ~r))

                  T r;
                  T p;
                  FC s;
                  T 0;
                  F ~r;
                  T q;
 
Branch of T or,Disjunct: s of Main SWFF: T (~p | (q | s))

               T s;
               F 1;
 
Right branch of F equiv,Main SWFF: F (((~p | (q | s))&(~p | (s | ~r))) <=> ((p&(q => r)) => s))

      F (((p&(q => r)) => s) => ((~p | (q | s))&(~p | (s | ~r))));
 
F->,Main SWFF: F (((p&(q => r)) => s) => ((~p | (q | s))&(~p | (s | ~r))))

         T ((p&(q => r)) => s);
         F ((~p | s)&(~p | (s | ~r)));
         F q;
 
Main SWFF: T ((p&(q => r)) => s)

            T (p => ((q => r) => s));
            F ((~p | s)&(~p | (s | ~r)));
            F q;
 
Left branch of F and,Main SWFF: F ((~p | s)&(~p | (s | ~r)))

               FC r;
               F (~p | s);
               F q;
               T (p => (~q => s));
 
Main SWFF: F (~p | s)

                  F ~p;
                  F s;
                  F q;
                  T (p => (~q => s));
                  FC r;
 
F non,Main SWFF: F ~p

                     T q;
                     T s;
                     T p;
 
 
1 search result = unprovable (fCube-4.1)
*** The Counter Model (see also the prolog term ) ***
-- root --
-- end world -- 
      F s;
      F q;
      FC r;
-- end world -- 
         T q;
         T s;
         T p;
-- end world --
*** Prolog term of the countermodel ***
[[swff(f,s),swff(f,q),swff(fc,r),[swff(t,q),swff(t,s),swff(t,p)]]]
true.