The cow eats the lion. The cow is rough. The cow likes the tiger. The lion is big. The lion likes the tiger. The tiger likes the lion. The tiger needs the cow. If someone eats the cow and they like the tiger then the cow likes the lion. If someone is kind then they eat the cow. If someone likes the lion then the lion needs the tiger. If someone eats the lion and the lion eats the cow then the lion eats the tiger. If someone eats the cow then the cow likes the lion. If the tiger needs the lion and the tiger eats the lion then the tiger is red. If someone is rough then they eat the lion. If someone eats the tiger and they like the tiger then they are cold.
The cow eats the lion.
("cow" "eats" "lion" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The lion is big.
("lion" "is" "big" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
If someone eats the cow and they like the tiger then the cow likes the lion.
((("someone" "eats" "cow" "+") ("someone" "likes" "tiger" "+")) -> ("cow" "likes" "lion" "+"))
If someone is kind then they eat the cow.
((("someone" "is" "kind" "+")) -> ("someone" "eats" "cow" "+"))
If someone likes the lion then the lion needs the tiger.
((("someone" "likes" "lion" "+")) -> ("lion" "needs" "tiger" "+"))
If someone eats the lion and the lion eats the cow then the lion eats the tiger.
((("someone" "eats" "lion" "+") ("lion" "eats" "cow" "+")) -> ("lion" "eats" "tiger" "+"))
If someone eats the cow then the cow likes the lion.
((("someone" "eats" "cow" "+")) -> ("cow" "likes" "lion" "+"))
If the tiger needs the lion and the tiger eats the lion then the tiger is red.
((("tiger" "needs" "lion" "+") ("tiger" "eats" "lion" "+")) -> ("tiger" "is" "red" "+"))
If someone is rough then they eat the lion.
((("someone" "is" "rough" "+")) -> ("someone" "eats" "lion" "+"))
If someone eats the tiger and they like the tiger then they are cold.
((("someone" "eats" "tiger" "+") ("someone" "likes" "tiger" "+")) -> ("someone" "is" "cold" "+"))
The cow is rough.
True
1
proof
[(triple2)]
("cow" "is" "rough" "+")
triple2
The tiger does not need the cow.
False
1
inv-proof
[(triple7)]
("tiger" "needs" "cow" "-")
triple7
The lion needs the tiger.
True
2
proof
[(((triple6) -> rule3))]
("lion" "needs" "tiger" "+")
((triple6) -> (rule3 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The lion does not need the tiger.
False
2
inv-proof
[(((triple6) -> rule3))]
("lion" "needs" "tiger" "-")
((triple6) -> (rule3 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The cow does not eat the cow.
Unknown
inv-rconc
[@1: The cow eats the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "eats" "cow" "-")
The tiger is cold.
Unknown
rconc
[@1: The tiger is cold.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "is" "cold" "+")
The tiger does not need the lion.
Unknown
inv-random
[@0: The tiger needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "lion" "-")
The lion needs the cow.
Unknown
random
[@0: The lion needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "cow" "+")
@0: The cow eats the lion.[(triple1 OR ((triple2) -> rule7))] The cow is rough.[(triple2)] The cow likes the tiger.[(triple3)] The lion is big.[(triple4)] The lion likes the tiger.[(triple5)] The tiger likes the lion.[(triple6)] The tiger needs the cow.[(triple7)] @1: The lion needs the tiger.[(((triple6) -> rule3))]
The cow eats the lion.
("cow" "eats" "lion" "+")
triple1
((triple2) -> (rule7 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
triple2
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple3
The lion is big.
("lion" "is" "big" "+")
triple4
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple5
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple6
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple7
The lion needs the tiger.
("lion" "needs" "tiger" "+")
((triple6) -> (rule3 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1