The mouse is big. The mouse is blue. The mouse is rough. The mouse is round. The mouse is young. If someone is big then they are blue. All blue, rough people are big. If the mouse is rough and the mouse is blue then the mouse is big. All blue, rough people are round. All big, rough people are blue. If the mouse is young then the mouse is rough. Rough people are big. If someone is young then they are blue.
The mouse is big.
("mouse" "is" "big" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse is young.
("mouse" "is" "young" "+")
If someone is big then they are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
All blue, rough people are big.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
If the mouse is rough and the mouse is blue then the mouse is big.
((("mouse" "is" "rough" "+") ("mouse" "is" "blue" "+")) -> ("mouse" "is" "big" "+"))
All blue, rough people are round.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
All big, rough people are blue.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
If the mouse is young then the mouse is rough.
((("mouse" "is" "young" "+")) -> ("mouse" "is" "rough" "+"))
Rough people are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
If someone is young then they are blue.
((("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
The mouse is big.
True
1
proof
[(triple1 OR ((triple3) -> rule7) OR ((triple2 triple3) -> rule2) OR ((triple3 triple2) -> rule3) OR ((((triple5) -> rule6)) -> rule7) OR ((triple2 ((triple5) -> rule6)) -> rule2) OR ((triple3 ((triple5) -> rule8)) -> rule3) OR ((((triple5) -> rule6) triple2) -> rule3) OR ((((triple5) -> rule8) triple3) -> rule2) OR ((((triple5) -> rule6) ((triple5) -> rule8)) -> rule3) OR ((((triple5) -> rule8) ((triple5) -> rule6)) -> rule2))]
("mouse" "is" "big" "+")
triple1
((triple3) -> (rule7 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
((triple2 triple3) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
((triple3 triple2) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
((((triple5) -> (rule6 % int2))) -> (rule7 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
((triple2 ((triple5) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
((triple3 ((triple5) -> (rule8 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
((((triple5) -> (rule6 % int2)) triple2) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
((((triple5) -> (rule8 % int2)) triple3) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
((((triple5) -> (rule6 % int3)) ((triple5) -> (rule8 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
((((triple5) -> (rule8 % int3)) ((triple5) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The mouse is not young.
False
1
inv-proof
[(triple5)]
("mouse" "is" "young" "-")
triple5
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
@0: The mouse is big.[(triple1 OR ((triple3) -> rule7) OR ((triple2 triple3) -> rule2) OR ((triple3 triple2) -> rule3) OR ((((triple5) -> rule6)) -> rule7) OR ((triple2 ((triple5) -> rule6)) -> rule2) OR ((triple3 ((triple5) -> rule8)) -> rule3) OR ((((triple5) -> rule6) triple2) -> rule3) OR ((((triple5) -> rule8) triple3) -> rule2) OR ((((triple5) -> rule6) ((triple5) -> rule8)) -> rule3) OR ((((triple5) -> rule8) ((triple5) -> rule6)) -> rule2))] The mouse is blue.[(triple2 OR ((triple1) -> rule1) OR ((triple5) -> rule8) OR ((triple1 triple3) -> rule5) OR ((((triple3) -> rule7)) -> rule1) OR ((triple1 ((triple5) -> rule6)) -> rule5) OR ((((triple3) -> rule7) triple3) -> rule5) OR ((((triple3) -> rule7) ((triple5) -> rule6)) -> rule5) OR ((((((triple5) -> rule6)) -> rule7)) -> rule1) OR ((((((triple5) -> rule6)) -> rule7) triple3) -> rule5) OR ((((((triple5) -> rule6)) -> rule7) ((triple5) -> rule6)) -> rule5))] The mouse is rough.[(triple3 OR ((triple5) -> rule6))] The mouse is round.[(triple4 OR ((triple2 triple3) -> rule4) OR ((triple2 ((triple5) -> rule6)) -> rule4) OR ((((triple1) -> rule1) triple3) -> rule4) OR ((((triple5) -> rule8) triple3) -> rule4) OR ((((triple1 triple3) -> rule5) triple3) -> rule4) OR ((((triple1) -> rule1) ((triple5) -> rule6)) -> rule4) OR ((((triple5) -> rule8) ((triple5) -> rule6)) -> rule4) OR ((((triple1 triple3) -> rule5) ((triple5) -> rule6)) -> rule4) OR ((((((triple3) -> rule7)) -> rule1) triple3) -> rule4) OR ((((triple1 ((triple5) -> rule6)) -> rule5) triple3) -> rule4) OR ((((((triple3) -> rule7) triple3) -> rule5) triple3) -> rule4) OR ((((((triple3) -> rule7)) -> rule1) ((triple5) -> rule6)) -> rule4) OR ((((triple1 ((triple5) -> rule6)) -> rule5) ((triple5) -> rule6)) -> rule4) OR ((((((triple3) -> rule7) triple3) -> rule5) ((triple5) -> rule6)) -> rule4) OR ((((((triple3) -> rule7) ((triple5) -> rule6)) -> rule5) triple3) -> rule4) OR ((((((triple3) -> rule7) ((triple5) -> rule6)) -> rule5) ((triple5) -> rule6)) -> rule4) OR ((((((((triple5) -> rule6)) -> rule7)) -> rule1) triple3) -> rule4) OR ((((((((triple5) -> rule6)) -> rule7) triple3) -> rule5) triple3) -> rule4) OR ((((((((triple5) -> rule6)) -> rule7)) -> rule1) ((triple5) -> rule6)) -> rule4) OR ((((((((triple5) -> rule6)) -> rule7) triple3) -> rule5) ((triple5) -> rule6)) -> rule4) OR ((((((((triple5) -> rule6)) -> rule7) ((triple5) -> rule6)) -> rule5) triple3) -> rule4) OR ((((((((triple5) -> rule6)) -> rule7) ((triple5) -> rule6)) -> rule5) ((triple5) -> rule6)) -> rule4))] The mouse is young.[(triple5)]
The mouse is big.
("mouse" "is" "big" "+")
triple1
((triple3) -> (rule7 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
((triple2 triple3) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
((triple3 triple2) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
((((triple5) -> (rule6 % int2))) -> (rule7 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
((triple2 ((triple5) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
((triple3 ((triple5) -> (rule8 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
((((triple5) -> (rule6 % int2)) triple2) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
((((triple5) -> (rule8 % int2)) triple3) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
((((triple5) -> (rule6 % int3)) ((triple5) -> (rule8 % int2))) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
((((triple5) -> (rule8 % int3)) ((triple5) -> (rule6 % int2))) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The mouse is blue.
("mouse" "is" "blue" "+")
triple2
((triple1) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((triple5) -> (rule8 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((triple1 triple3) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
((triple1 ((triple5) -> (rule6 % int2))) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
((((triple3) -> (rule7 % int2)) triple3) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
((((triple3) -> (rule7 % int3)) ((triple5) -> (rule6 % int2))) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
int3
((((((triple5) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
((((((triple5) -> (rule6 % int3))) -> (rule7 % int2)) triple3) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
((((((triple5) -> (rule6 % int3))) -> (rule7 % int2)) ((triple5) -> (rule6 % int3))) -> (rule5 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
triple3
((triple5) -> (rule6 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
triple4
((triple2 triple3) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
((triple2 ((triple5) -> (rule6 % int2))) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
((((triple1) -> (rule1 % int2)) triple3) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
((((triple5) -> (rule8 % int2)) triple3) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
((((triple1 triple3) -> (rule5 % int2)) triple3) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
((((triple1) -> (rule1 % int3)) ((triple5) -> (rule6 % int2))) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
((((triple5) -> (rule8 % int3)) ((triple5) -> (rule6 % int2))) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
((((triple1 triple3) -> (rule5 % int3)) ((triple5) -> (rule6 % int2))) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
((((((triple3) -> (rule7 % int3))) -> (rule1 % int2)) triple3) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
int3
((((triple1 ((triple5) -> (rule6 % int3))) -> (rule5 % int2)) triple3) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
((((((triple3) -> (rule7 % int3)) triple3) -> (rule5 % int2)) triple3) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
int3
((((((triple3) -> (rule7 % int4))) -> (rule1 % int3)) ((triple5) -> (rule6 % int2))) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The mouse is big.
("mouse" "is" "big" "+")
int4
((((triple1 ((triple5) -> (rule6 % int3))) -> (rule5 % int2)) ((triple5) -> (rule6 % int3))) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
((((((triple3) -> (rule7 % int4)) triple3) -> (rule5 % int3)) ((triple5) -> (rule6 % int2))) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The mouse is big.
("mouse" "is" "big" "+")
int4
((((((triple3) -> (rule7 % int4)) ((triple5) -> (rule6 % int3))) -> (rule5 % int2)) triple3) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The mouse is big.
("mouse" "is" "big" "+")
int4
((((((triple3) -> (rule7 % int4)) ((triple5) -> (rule6 % int3))) -> (rule5 % int2)) ((triple5) -> (rule6 % int3))) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The mouse is big.
("mouse" "is" "big" "+")
int4
((((((((triple5) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule1 % int2)) triple3) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
int4
((((((((triple5) -> (rule6 % int4))) -> (rule7 % int3)) triple3) -> (rule5 % int2)) triple3) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
int4
((((((((triple5) -> (rule6 % int4))) -> (rule7 % int3))) -> (rule1 % int2)) ((triple5) -> (rule6 % int4))) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
int4
((((((((triple5) -> (rule6 % int4))) -> (rule7 % int3)) triple3) -> (rule5 % int2)) ((triple5) -> (rule6 % int4))) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
int4
((((((((triple5) -> (rule6 % int4))) -> (rule7 % int3)) ((triple5) -> (rule6 % int4))) -> (rule5 % int2)) triple3) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
int4
((((((((triple5) -> (rule6 % int4))) -> (rule7 % int3)) ((triple5) -> (rule6 % int4))) -> (rule5 % int2)) ((triple5) -> (rule6 % int4))) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse is big.
("mouse" "is" "big" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
int4
The mouse is young.
("mouse" "is" "young" "+")
triple5