The cat chases the rabbit. The rabbit likes the tiger. The tiger is nice. If something eats the tiger and the tiger is red then it chases the rabbit. If something eats the cat then the cat likes the tiger. If something likes the tiger then the tiger eats the cat. If the cat chases the tiger and the cat likes the tiger then the tiger eats the cat. If something is red then it likes the rabbit. If something likes the rabbit and it chases the cat then the cat is nice. If something likes the tiger then the tiger chases the cat. If something is young and it chases the tiger then it eats the cat.
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
If something eats the tiger and the tiger is red then it chases the rabbit.
((("something" "eats" "tiger" "+") ("tiger" "is" "red" "+")) -> ("something" "chases" "rabbit" "+"))
If something eats the cat then the cat likes the tiger.
((("something" "eats" "cat" "+")) -> ("cat" "likes" "tiger" "+"))
If something likes the tiger then the tiger eats the cat.
((("something" "likes" "tiger" "+")) -> ("tiger" "eats" "cat" "+"))
If the cat chases the tiger and the cat likes the tiger then the tiger eats the cat.
((("cat" "chases" "tiger" "+") ("cat" "likes" "tiger" "+")) -> ("tiger" "eats" "cat" "+"))
If something is red then it likes the rabbit.
((("something" "is" "red" "+")) -> ("something" "likes" "rabbit" "+"))
If something likes the rabbit and it chases the cat then the cat is nice.
((("something" "likes" "rabbit" "+") ("something" "chases" "cat" "+")) -> ("cat" "is" "nice" "+"))
If something likes the tiger then the tiger chases the cat.
((("something" "likes" "tiger" "+")) -> ("tiger" "chases" "cat" "+"))
If something is young and it chases the tiger then it eats the cat.
((("something" "is" "young" "+") ("something" "chases" "tiger" "+")) -> ("something" "eats" "cat" "+"))
The tiger is nice.
True
1
proof
[(triple3)]
("tiger" "is" "nice" "+")
triple3
The rabbit does not like the tiger.
False
1
inv-proof
[(triple2)]
("rabbit" "likes" "tiger" "-")
triple2
The tiger chases the cat.
True
2
proof
[(((triple2) -> rule7) OR ((((((triple2) -> rule3)) -> rule2)) -> rule7))]
("tiger" "chases" "cat" "+")
((triple2) -> (rule7 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int2
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int3
The tiger does not eat the cat.
False
2
inv-proof
[(((triple2) -> rule3))]
("tiger" "eats" "cat" "-")
((triple2) -> (rule3 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
The cat likes the tiger.
True
3
proof
[(((((triple2) -> rule3)) -> rule2))]
("cat" "likes" "tiger" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int2
The cat does not like the tiger.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2))]
("cat" "likes" "tiger" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int2
The tiger does not like the rabbit.
Unknown
inv-rconc
[@1: The tiger likes the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "likes" "rabbit" "-")
The rabbit chases the rabbit.
Unknown
rconc
[@1: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "chases" "rabbit" "+")
The tiger does not chase the rabbit.
Unknown
inv-rconc
[@1: The tiger chases the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "chases" "rabbit" "-")
The cat eats the rabbit.
Unknown
random
[@0: The cat eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "rabbit" "+")
The cat is not young.
Unknown
inv-random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
@0: The cat chases the rabbit.[(triple1)] The rabbit likes the tiger.[(triple2)] The tiger is nice.[(triple3)] @1: The tiger chases the cat.[(((triple2) -> rule7) OR ((((((triple2) -> rule3)) -> rule2)) -> rule7))] The tiger eats the cat.[(((triple2) -> rule3))] @2: The cat likes the tiger.[(((((triple2) -> rule3)) -> rule2))]
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple1
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple2
The tiger is nice.
("tiger" "is" "nice" "+")
triple3
The tiger chases the cat.
("tiger" "chases" "cat" "+")
((triple2) -> (rule7 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int2
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int3
The tiger eats the cat.
("tiger" "eats" "cat" "+")
((triple2) -> (rule3 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int2