The cat chases the mouse. The cat is rough. The cow eats the lion. The cow eats the mouse. The cow is not blue. The cow likes the cat. The cow likes the lion. The lion chases the cat. The lion chases the cow. The lion chases the mouse. The mouse eats the cow. The mouse eats the lion. If someone likes the lion and the lion is not nice then the lion eats the cat. If the lion likes the cow and the lion does not like the mouse then the mouse likes the cat. If someone eats the mouse then the mouse likes the cat. If someone is cold and they chase the cow then they chase the cat. If someone chases the lion and they eat the cow then the lion likes the cat. If someone chases the mouse then the mouse chases the lion. If the lion likes the cat then the cat is nice. If someone is nice and they do not chase the cat then they eat the cat.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cow eats the lion.
("cow" "eats" "lion" "+")
The cow eats the mouse.
("cow" "eats" "mouse" "+")
The cow is not blue.
("cow" "is" "blue" "-")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
If someone likes the lion and the lion is not nice then the lion eats the cat.
((("someone" "likes" "lion" "+") ("lion" "is" "nice" "~")) -> ("lion" "eats" "cat" "+"))
If the lion likes the cow and the lion does not like the mouse then the mouse likes the cat.
((("lion" "likes" "cow" "+") ("lion" "likes" "mouse" "~")) -> ("mouse" "likes" "cat" "+"))
If someone eats the mouse then the mouse likes the cat.
((("someone" "eats" "mouse" "+")) -> ("mouse" "likes" "cat" "+"))
If someone is cold and they chase the cow then they chase the cat.
((("someone" "is" "cold" "+") ("someone" "chases" "cow" "+")) -> ("someone" "chases" "cat" "+"))
If someone chases the lion and they eat the cow then the lion likes the cat.
((("someone" "chases" "lion" "+") ("someone" "eats" "cow" "+")) -> ("lion" "likes" "cat" "+"))
If someone chases the mouse then the mouse chases the lion.
((("someone" "chases" "mouse" "+")) -> ("mouse" "chases" "lion" "+"))
If the lion likes the cat then the cat is nice.
((("lion" "likes" "cat" "+")) -> ("cat" "is" "nice" "+"))
If someone is nice and they do not chase the cat then they eat the cat.
((("someone" "is" "nice" "+") ("someone" "chases" "cat" "~")) -> ("someone" "eats" "cat" "+"))
The mouse eats the lion.
True
1
proof
[(triple12)]
("mouse" "eats" "lion" "+")
triple12
The mouse does not eat the cow.
False
1
inv-proof
[(triple11)]
("mouse" "eats" "cow" "-")
triple11
The mouse likes the cat.
True
2
proof
[(((triple4) -> rule3))]
("mouse" "likes" "cat" "+")
((triple4) -> (rule3 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The mouse does not like the cat.
False
2
inv-proof
[(((triple4) -> rule3))]
("mouse" "likes" "cat" "-")
((triple4) -> (rule3 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The lion likes the cat.
True
4
proof
[(((((triple1) -> rule6) triple11) -> rule5) OR ((((triple10) -> rule6) triple11) -> rule5))]
("lion" "likes" "cat" "+")
((((triple1) -> (rule6 % int2)) triple11) -> (rule5 % int1))
The lion likes the cat.
("lion" "likes" "cat" "+")
int1
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int2
((((triple10) -> (rule6 % int2)) triple11) -> (rule5 % int1))
The lion likes the cat.
("lion" "likes" "cat" "+")
int1
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int2
The lion does not like the cat.
False
4
inv-proof
[(((((triple1) -> rule6) triple11) -> rule5) OR ((((triple10) -> rule6) triple11) -> rule5))]
("lion" "likes" "cat" "-")
((((triple1) -> (rule6 % int2)) triple11) -> (rule5 % int1))
The lion likes the cat.
("lion" "likes" "cat" "+")
int1
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int2
((((triple10) -> (rule6 % int2)) triple11) -> (rule5 % int1))
The lion likes the cat.
("lion" "likes" "cat" "+")
int1
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int2
The cat is nice.
True
5
proof
[(((((((triple1) -> rule6) triple11) -> rule5)) -> rule7) OR ((((((triple10) -> rule6) triple11) -> rule5)) -> rule7))]
("cat" "is" "nice" "+")
((((((triple1) -> (rule6 % int3)) triple11) -> (rule5 % int2))) -> (rule7 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
int2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int3
((((((triple10) -> (rule6 % int3)) triple11) -> (rule5 % int2))) -> (rule7 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
int2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int3
The cat is not nice.
False
5
inv-proof
[(((((((triple1) -> rule6) triple11) -> rule5)) -> rule7) OR ((((((triple10) -> rule6) triple11) -> rule5)) -> rule7))]
("cat" "is" "nice" "-")
((((((triple1) -> (rule6 % int3)) triple11) -> (rule5 % int2))) -> (rule7 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
int2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int3
((((((triple10) -> (rule6 % int3)) triple11) -> (rule5 % int2))) -> (rule7 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
int2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int3
The lion does not eat the cat.
Unknown
inv-rconc
[@1: The lion eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "eats" "cat" "-")
The mouse eats the cat.
Unknown
rconc
[@1: The mouse eats the cat.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "eats" "cat" "+")
The mouse does not chase the cat.
Unknown
inv-rconc
[@1: The mouse chases the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "chases" "cat" "-")
The cow chases the cat.
Unknown
rconc
[@1: The cow chases the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "chases" "cat" "+")
The lion is not blue.
Unknown
inv-random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
The cat does not eat the mouse.
Unknown
inv-random
[@0: The cat eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "mouse" "-")
The cat is cold.
Unknown
random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "+")
@0: The cat chases the mouse.[(triple1)] The cat is rough.[(triple2)] The cow eats the lion.[(triple3)] The cow eats the mouse.[(triple4)] The cow is not blue.[(triple5)] The cow likes the cat.[(triple6)] The cow likes the lion.[(triple7)] The lion chases the cat.[(triple8)] The lion chases the cow.[(triple9)] The lion chases the mouse.[(triple10)] The mouse eats the cow.[(triple11)] The mouse eats the lion.[(triple12)] @1: The mouse chases the lion.[(((triple1) -> rule6) OR ((triple10) -> rule6))] The mouse likes the cat.[(((triple4) -> rule3))] @2: The lion likes the cat.[(((((triple1) -> rule6) triple11) -> rule5) OR ((((triple10) -> rule6) triple11) -> rule5))] @3: The cat is nice.[(((((((triple1) -> rule6) triple11) -> rule5)) -> rule7) OR ((((((triple10) -> rule6) triple11) -> rule5)) -> rule7))]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
The cat is rough.
("cat" "is" "rough" "+")
triple2
The cow eats the lion.
("cow" "eats" "lion" "+")
triple3
The cow eats the mouse.
("cow" "eats" "mouse" "+")
triple4
The cow is not blue.
("cow" "is" "blue" "-")
triple5
The cow likes the cat.
("cow" "likes" "cat" "+")
triple6
The cow likes the lion.
("cow" "likes" "lion" "+")
triple7
The lion chases the cat.
("lion" "chases" "cat" "+")
triple8
The lion chases the cow.
("lion" "chases" "cow" "+")
triple9
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple10
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple11
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple12
The mouse chases the lion.
("mouse" "chases" "lion" "+")
((triple1) -> (rule6 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
((triple10) -> (rule6 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The mouse likes the cat.
("mouse" "likes" "cat" "+")
((triple4) -> (rule3 % int1))
The mouse likes the cat.
("mouse" "likes" "cat" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
((((triple1) -> (rule6 % int2)) triple11) -> (rule5 % int1))
The lion likes the cat.
("lion" "likes" "cat" "+")
int1
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int2
((((triple10) -> (rule6 % int2)) triple11) -> (rule5 % int1))
The lion likes the cat.
("lion" "likes" "cat" "+")
int1
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
((((((triple1) -> (rule6 % int3)) triple11) -> (rule5 % int2))) -> (rule7 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
int2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int3
((((((triple10) -> (rule6 % int3)) triple11) -> (rule5 % int2))) -> (rule7 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
int2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int3