The bear visits the tiger. The cow chases the bear. The tiger visits the bear. If someone chases the bear then they visit the cow. If the cow is rough then the cow chases the bear. If someone sees the cow then they chase the cow. If someone sees the tiger and the tiger chases the bear then the tiger sees the cow. If someone chases the bear then they see the tiger. If someone visits the cow then the cow visits the tiger. If someone visits the tiger then they are blue. If someone sees the bear and the bear visits the tiger then they visit the cow.
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The cow chases the bear.
("cow" "chases" "bear" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
If someone chases the bear then they visit the cow.
((("someone" "chases" "bear" "+")) -> ("someone" "visits" "cow" "+"))
If the cow is rough then the cow chases the bear.
((("cow" "is" "rough" "+")) -> ("cow" "chases" "bear" "+"))
If someone sees the cow then they chase the cow.
((("someone" "sees" "cow" "+")) -> ("someone" "chases" "cow" "+"))
If someone sees the tiger and the tiger chases the bear then the tiger sees the cow.
((("someone" "sees" "tiger" "+") ("tiger" "chases" "bear" "+")) -> ("tiger" "sees" "cow" "+"))
If someone chases the bear then they see the tiger.
((("someone" "chases" "bear" "+")) -> ("someone" "sees" "tiger" "+"))
If someone visits the cow then the cow visits the tiger.
((("someone" "visits" "cow" "+")) -> ("cow" "visits" "tiger" "+"))
If someone visits the tiger then they are blue.
((("someone" "visits" "tiger" "+")) -> ("someone" "is" "blue" "+"))
If someone sees the bear and the bear visits the tiger then they visit the cow.
((("someone" "sees" "bear" "+") ("bear" "visits" "tiger" "+")) -> ("someone" "visits" "cow" "+"))
The tiger visits the bear.
True
1
proof
[(triple3)]
("tiger" "visits" "bear" "+")
triple3
The tiger does not visit the bear.
False
1
inv-proof
[(triple3)]
("tiger" "visits" "bear" "-")
triple3
The cow sees the tiger.
True
2
proof
[(((triple2) -> rule5))]
("cow" "sees" "tiger" "+")
((triple2) -> (rule5 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The cow does not visit the cow.
False
2
inv-proof
[(((triple2) -> rule1))]
("cow" "visits" "cow" "-")
((triple2) -> (rule1 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow visits the tiger.
True
3
proof
[(((((triple2) -> rule1)) -> rule6))]
("cow" "visits" "tiger" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow does not visit the tiger.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule6))]
("cow" "visits" "tiger" "-")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow does not chase the cow.
Unknown
inv-rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "chases" "cow" "-")
The tiger visits the cow.
Unknown
rconc
[@1: The tiger visits the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "visits" "cow" "+")
The bear does not chase the cow.
Unknown
inv-rconc
[@1: The bear chases the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "chases" "cow" "-")
The bear is young.
Unknown
random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "+")
The tiger does not chase the bear.
Unknown
inv-random
[@0: The tiger chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "bear" "-")
The tiger sees the bear.
Unknown
random
[@0: The tiger sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "bear" "+")
@0: The bear visits the tiger.[(triple1)] The cow chases the bear.[(triple2)] The tiger visits the bear.[(triple3)] @1: The bear is blue.[(((triple1) -> rule7))] The cow sees the tiger.[(((triple2) -> rule5))] The cow visits the cow.[(((triple2) -> rule1))] @2: The cow visits the tiger.[(((((triple2) -> rule1)) -> rule6))] @3: The cow is blue.[(((((((triple2) -> rule1)) -> rule6)) -> rule7))]
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple1
The cow chases the bear.
("cow" "chases" "bear" "+")
triple2
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple3
The bear is blue.
("bear" "is" "blue" "+")
((triple1) -> (rule7 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
((triple2) -> (rule5 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
((triple2) -> (rule1 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow visits the tiger.
("cow" "visits" "tiger" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
((((((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow visits the tiger.
("cow" "visits" "tiger" "+")
int2
The cow visits the cow.
("cow" "visits" "cow" "+")
int3