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