The lion does not eat the mouse. The lion is cold. The lion is round. The lion likes the mouse. The lion sees the mouse. The mouse eats the lion. The mouse is cold. The mouse is not kind. The mouse is nice. The mouse is round. The mouse likes the lion. The mouse does not see the lion. If someone is round then they do not see the lion. If someone eats the mouse then they are not nice. If someone likes the mouse then the mouse likes the lion. If someone likes the lion and the lion likes the mouse then the lion sees the mouse. If the lion eats the mouse and the lion is not round then the lion sees the mouse. If someone is round and they do not see the lion then they are not big. If someone likes the mouse then they like the lion. If someone is big then they like the lion.
The lion does not eat the mouse.
("lion" "eats" "mouse" "-")
The lion is cold.
("lion" "is" "cold" "+")
The lion is round.
("lion" "is" "round" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is not kind.
("mouse" "is" "kind" "-")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
The mouse does not see the lion.
("mouse" "sees" "lion" "-")
If someone is round then they do not see the lion.
((("someone" "is" "round" "+")) -> ("someone" "sees" "lion" "-"))
If someone eats the mouse then they are not nice.
((("someone" "eats" "mouse" "+")) -> ("someone" "is" "nice" "-"))
If someone likes the mouse then the mouse likes the lion.
((("someone" "likes" "mouse" "+")) -> ("mouse" "likes" "lion" "+"))
If someone likes the lion and the lion likes the mouse then the lion sees the mouse.
((("someone" "likes" "lion" "+") ("lion" "likes" "mouse" "+")) -> ("lion" "sees" "mouse" "+"))
If the lion eats the mouse and the lion is not round then the lion sees the mouse.
((("lion" "eats" "mouse" "+") ("lion" "is" "round" "~")) -> ("lion" "sees" "mouse" "+"))
If someone is round and they do not see the lion then they are not big.
((("someone" "is" "round" "+") ("someone" "sees" "lion" "~")) -> ("someone" "is" "big" "-"))
If someone likes the mouse then they like the lion.
((("someone" "likes" "mouse" "+")) -> ("someone" "likes" "lion" "+"))
If someone is big then they like the lion.
((("someone" "is" "big" "+")) -> ("someone" "likes" "lion" "+"))
The mouse is round.
True
1
proof
[(triple10)]
("mouse" "is" "round" "+")
triple10
The mouse does not eat the lion.
False
1
inv-proof
[(triple6)]
("mouse" "eats" "lion" "-")
triple6
The mouse is not big.
True
3
proof
[(((triple10 triple12) -> rule6) OR ((triple10 ((triple10) -> rule1)) -> rule6))]
("mouse" "is" "big" "-")
((triple10 triple12) -> (rule6 % int1))
The mouse is not big.
("mouse" "is" "big" "-")
int1
((triple10 ((triple10) -> (rule1 % int2))) -> (rule6 % int1))
The mouse is not big.
("mouse" "is" "big" "-")
int1
The mouse does not see the lion.
("mouse" "sees" "lion" "-")
int2
The lion does not like the lion.
False
2
inv-proof
[(((triple4) -> rule7))]
("lion" "likes" "lion" "-")
((triple4) -> (rule7 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion is not big.
True
4
proof
[(((triple3 ((triple3) -> rule1)) -> rule6))]
("lion" "is" "big" "-")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The lion is not big.
("lion" "is" "big" "-")
int1
The lion does not see the lion.
("lion" "sees" "lion" "-")
int2
The lion is big.
False
4
inv-proof
[(((triple3 ((triple3) -> rule1)) -> rule6))]
("lion" "is" "big" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The lion is not big.
("lion" "is" "big" "-")
int1
The lion does not see the lion.
("lion" "sees" "lion" "-")
int2
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
The lion is not nice.
Unknown
inv-random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
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 lion is kind.
Unknown
random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "+")
@0: The lion does not eat the mouse.[(triple1)] The lion is cold.[(triple2)] The lion is round.[(triple3)] The lion likes the mouse.[(triple4)] The lion sees the mouse.[(triple5 OR ((triple11 triple4) -> rule4) OR ((((triple4) -> rule3) triple4) -> rule4) OR ((((triple4) -> rule7) triple4) -> rule4))] The mouse does not see the lion.[(triple12 OR ((triple10) -> rule1))] The mouse eats the lion.[(triple6)] The mouse is cold.[(triple7)] The mouse is nice.[(triple9)] The mouse is not kind.[(triple8)] The mouse is round.[(triple10)] The mouse likes the lion.[(triple11 OR ((triple4) -> rule3))] @1: The lion does not see the lion.[(((triple3) -> rule1))] The lion likes the lion.[(((triple4) -> rule7))] The mouse is not big.[(((triple10 triple12) -> rule6) OR ((triple10 ((triple10) -> rule1)) -> rule6))] @2: The lion is not big.[(((triple3 ((triple3) -> rule1)) -> rule6))]
The lion does not eat the mouse.
("lion" "eats" "mouse" "-")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The lion is round.
("lion" "is" "round" "+")
triple3
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple4
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple5
((triple11 triple4) -> (rule4 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
((((triple4) -> (rule3 % int2)) triple4) -> (rule4 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int2
((((triple4) -> (rule7 % int2)) triple4) -> (rule4 % int1))
The lion sees the mouse.
("lion" "sees" "mouse" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The mouse does not see the lion.
("mouse" "sees" "lion" "-")
triple12
((triple10) -> (rule1 % int1))
The mouse does not see the lion.
("mouse" "sees" "lion" "-")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple6
The mouse is cold.
("mouse" "is" "cold" "+")
triple7
The mouse is nice.
("mouse" "is" "nice" "+")
triple9
The mouse is not kind.
("mouse" "is" "kind" "-")
triple8
The mouse is round.
("mouse" "is" "round" "+")
triple10
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple11
((triple4) -> (rule3 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The lion does not see the lion.
("lion" "sees" "lion" "-")
((triple3) -> (rule1 % int1))
The lion does not see the lion.
("lion" "sees" "lion" "-")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
((triple4) -> (rule7 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The mouse is not big.
("mouse" "is" "big" "-")
((triple10 triple12) -> (rule6 % int1))
The mouse is not big.
("mouse" "is" "big" "-")
int1
((triple10 ((triple10) -> (rule1 % int2))) -> (rule6 % int1))
The mouse is not big.
("mouse" "is" "big" "-")
int1
The mouse does not see the lion.
("mouse" "sees" "lion" "-")
int2
The lion is not big.
("lion" "is" "big" "-")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The lion is not big.
("lion" "is" "big" "-")
int1
The lion does not see the lion.
("lion" "sees" "lion" "-")
int2