The cow is not big. The dog chases the tiger. The rabbit sees the tiger. The tiger sees the cow. If something sees the tiger then the tiger likes the dog. If the rabbit likes the cow then the rabbit is young.
The cow is not big.
("cow" "is" "big" "-")
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
If something sees the tiger then the tiger likes the dog.
((("something" "sees" "tiger" "+")) -> ("tiger" "likes" "dog" "+"))
If the rabbit likes the cow then the rabbit is young.
((("rabbit" "likes" "cow" "+")) -> ("rabbit" "is" "young" "+"))
The dog chases the tiger.
True
1
proof
[(triple2)]
("dog" "chases" "tiger" "+")
triple2
The dog does not chase the tiger.
False
1
inv-proof
[(triple2)]
("dog" "chases" "tiger" "-")
triple2
The tiger likes the dog.
True
2
proof
[(((triple3) -> rule1))]
("tiger" "likes" "dog" "+")
((triple3) -> (rule1 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger does not like the dog.
False
2
inv-proof
[(((triple3) -> rule1))]
("tiger" "likes" "dog" "-")
((triple3) -> (rule1 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The rabbit is not young.
Unknown
inv-rconc
[@1: The rabbit is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "young" "-")
The dog likes the tiger.
Unknown
random
[@0: The dog likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "tiger" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The cow chases the tiger.
Unknown
random
[@0: The cow chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "tiger" "+")
@0: The cow is not big.[(triple1)] The dog chases the tiger.[(triple2)] The rabbit sees the tiger.[(triple3)] The tiger sees the cow.[(triple4)] @1: The tiger likes the dog.[(((triple3) -> rule1))]
The cow is not big.
("cow" "is" "big" "-")
triple1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple2
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple3
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple4
The tiger likes the dog.
("tiger" "likes" "dog" "+")
((triple3) -> (rule1 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1