The lion eats the tiger. The mouse is rough. The rabbit eats the mouse. The tiger eats the rabbit. If the lion does not like the mouse then the lion likes the rabbit. If the tiger likes the lion then the tiger is rough. If someone eats the tiger then the tiger likes the rabbit. If someone likes the rabbit then the rabbit likes the tiger. If someone likes the mouse then the mouse is not red. If someone likes the rabbit then the rabbit visits the tiger. If someone visits the rabbit and the rabbit visits the mouse then the mouse does not like the tiger. If the rabbit likes the tiger then the tiger likes the lion.
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
If the lion does not like the mouse then the lion likes the rabbit.
((("lion" "likes" "mouse" "~")) -> ("lion" "likes" "rabbit" "+"))
If the tiger likes the lion then the tiger is rough.
((("tiger" "likes" "lion" "+")) -> ("tiger" "is" "rough" "+"))
If someone eats the tiger then the tiger likes the rabbit.
((("someone" "eats" "tiger" "+")) -> ("tiger" "likes" "rabbit" "+"))
If someone likes the rabbit then the rabbit likes the tiger.
((("someone" "likes" "rabbit" "+")) -> ("rabbit" "likes" "tiger" "+"))
If someone likes the mouse then the mouse is not red.
((("someone" "likes" "mouse" "+")) -> ("mouse" "is" "red" "-"))
If someone likes the rabbit then the rabbit visits the tiger.
((("someone" "likes" "rabbit" "+")) -> ("rabbit" "visits" "tiger" "+"))
If someone visits the rabbit and the rabbit visits the mouse then the mouse does not like the tiger.
((("someone" "visits" "rabbit" "+") ("rabbit" "visits" "mouse" "+")) -> ("mouse" "likes" "tiger" "-"))
If the rabbit likes the tiger then the tiger likes the lion.
((("rabbit" "likes" "tiger" "+")) -> ("tiger" "likes" "lion" "+"))
The tiger eats the rabbit.
True
1
proof
[(triple4)]
("tiger" "eats" "rabbit" "+")
triple4
The rabbit does not eat the mouse.
False
1
inv-proof
[(triple3)]
("rabbit" "eats" "mouse" "-")
triple3
The tiger likes the rabbit.
True
2
proof
[(((triple1) -> rule3))]
("tiger" "likes" "rabbit" "+")
((triple1) -> (rule3 % int1))
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int1
The tiger does not like the rabbit.
False
2
inv-proof
[(((triple1) -> rule3))]
("tiger" "likes" "rabbit" "-")
((triple1) -> (rule3 % int1))
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int1
The rabbit visits the tiger.
True
3
proof
[(((((triple1) -> rule3)) -> rule6))]
("rabbit" "visits" "tiger" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int2
The rabbit does not visit the tiger.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule6))]
("rabbit" "visits" "tiger" "-")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int2
The tiger likes the lion.
True
4
proof
[(((((((triple1) -> rule3)) -> rule4)) -> rule8))]
("tiger" "likes" "lion" "+")
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
int2
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int3
The tiger does not like the lion.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule4)) -> rule8))]
("tiger" "likes" "lion" "-")
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
int2
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int3
The lion does not like the rabbit.
Unknown
inv-rconc
[@1: The lion likes the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "likes" "rabbit" "-")
The lion likes the tiger.
Unknown
random
[@0: The lion likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "tiger" "+")
The rabbit does not visit the mouse.
Unknown
inv-random
[@0: The rabbit visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "mouse" "-")
The mouse likes the rabbit.
Unknown
random
[@0: The mouse likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "rabbit" "+")
The tiger does not visit the lion.
Unknown
inv-random
[@0: The tiger visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "lion" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
The tiger is not nice.
Unknown
inv-random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "-")
The rabbit is nice.
Unknown
random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "+")
@0: The lion eats the tiger.[(triple1)] The mouse is rough.[(triple2)] The rabbit eats the mouse.[(triple3)] The tiger eats the rabbit.[(triple4)] @1: The tiger likes the rabbit.[(((triple1) -> rule3))] @2: The rabbit likes the tiger.[(((((triple1) -> rule3)) -> rule4))] The rabbit visits the tiger.[(((((triple1) -> rule3)) -> rule6))] @3: The tiger likes the lion.[(((((((triple1) -> rule3)) -> rule4)) -> rule8))] @4: The tiger is rough.[(((((((((triple1) -> rule3)) -> rule4)) -> rule8)) -> rule2))]
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple1
The mouse is rough.
("mouse" "is" "rough" "+")
triple2
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple3
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple4
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
((triple1) -> (rule3 % int1))
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int1
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
int1
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int2
The tiger likes the lion.
("tiger" "likes" "lion" "+")
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
int2
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int3
The tiger is rough.
("tiger" "is" "rough" "+")
((((((((triple1) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int2
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
int3
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int4