The cow is blue. The cow is nice. The cow sees the rabbit. The cow sees the tiger. The cow visits the tiger. The rabbit sees the cow. The rabbit visits the cow. The tiger is blue. The tiger needs the rabbit. The tiger sees the rabbit. If someone sees the rabbit then the rabbit sees the cow. If someone sees the rabbit then they need the cow. If someone visits the cow then they see the cow. If someone needs the rabbit and the rabbit is blue then they need the tiger. Green, nice people are blue. If someone visits the cow then they see the rabbit. If someone needs the cow then they visit the rabbit. If someone sees the tiger and they need the tiger then the tiger sees the rabbit.
The cow is blue.
("cow" "is" "blue" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If someone sees the rabbit then the rabbit sees the cow.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "sees" "cow" "+"))
If someone sees the rabbit then they need the cow.
((("someone" "sees" "rabbit" "+")) -> ("someone" "needs" "cow" "+"))
If someone visits the cow then they see the cow.
((("someone" "visits" "cow" "+")) -> ("someone" "sees" "cow" "+"))
If someone needs the rabbit and the rabbit is blue then they need the tiger.
((("someone" "needs" "rabbit" "+") ("rabbit" "is" "blue" "+")) -> ("someone" "needs" "tiger" "+"))
Green, nice people are blue.
((("someone" "is" "green" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If someone visits the cow then they see the rabbit.
((("someone" "visits" "cow" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone needs the cow then they visit the rabbit.
((("someone" "needs" "cow" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone sees the tiger and they need the tiger then the tiger sees the rabbit.
((("someone" "sees" "tiger" "+") ("someone" "needs" "tiger" "+")) -> ("tiger" "sees" "rabbit" "+"))
The cow is nice.
True
1
proof
[(triple2)]
("cow" "is" "nice" "+")
triple2
The cow does not visit the tiger.
False
1
inv-proof
[(triple5)]
("cow" "visits" "tiger" "-")
triple5
The cow needs the cow.
True
2
proof
[(((triple3) -> rule2))]
("cow" "needs" "cow" "+")
((triple3) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow does not need the cow.
False
2
inv-proof
[(((triple3) -> rule2))]
("cow" "needs" "cow" "-")
((triple3) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The tiger visits the rabbit.
True
3
proof
[(((((triple10) -> rule2)) -> rule7))]
("tiger" "visits" "rabbit" "+")
((((triple10) -> (rule2 % int2))) -> (rule7 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The tiger does not visit the rabbit.
False
3
inv-proof
[(((((triple10) -> rule2)) -> rule7))]
("tiger" "visits" "rabbit" "-")
((((triple10) -> (rule2 % int2))) -> (rule7 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The rabbit visits the rabbit.
True
4
proof
[(((((((triple7) -> rule6)) -> rule2)) -> rule7))]
("rabbit" "visits" "rabbit" "+")
((((((triple7) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int3
The rabbit does not visit the rabbit.
False
4
inv-proof
[(((((((triple7) -> rule6)) -> rule2)) -> rule7))]
("rabbit" "visits" "rabbit" "-")
((((((triple7) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int3
The tiger does not see the cow.
Unknown
inv-rconc
[@1: The tiger sees the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "sees" "cow" "-")
The rabbit is blue.
Unknown
rconc
[@1: The rabbit is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "blue" "+")
The tiger does not need the tiger.
Unknown
inv-rconc
[@2: The tiger needs the tiger.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("tiger" "needs" "tiger" "-")
The rabbit needs the tiger.
Unknown
rconc
[@1: The rabbit needs the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "needs" "tiger" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
The rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
The cow is not cold.
Unknown
inv-random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
@0: The cow is blue.[(triple1)] The cow is nice.[(triple2)] The cow sees the rabbit.[(triple3)] The cow sees the tiger.[(triple4)] The cow visits the tiger.[(triple5)] The rabbit sees the cow.[(triple6 OR ((triple10) -> rule1) OR ((triple3) -> rule1) OR ((triple7) -> rule3) OR ((((triple7) -> rule6)) -> rule1))] The rabbit visits the cow.[(triple7)] The tiger is blue.[(triple8)] The tiger needs the rabbit.[(triple9)] The tiger sees the rabbit.[(triple10)] @1: The cow needs the cow.[(((triple3) -> rule2))] The rabbit sees the rabbit.[(((triple7) -> rule6))] The tiger needs the cow.[(((triple10) -> rule2))] @2: The cow visits the rabbit.[(((((triple3) -> rule2)) -> rule7))] The rabbit needs the cow.[(((((triple7) -> rule6)) -> rule2))] The tiger visits the rabbit.[(((((triple10) -> rule2)) -> rule7))] @3: The rabbit visits the rabbit.[(((((((triple7) -> rule6)) -> rule2)) -> rule7))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
The cow is nice.
("cow" "is" "nice" "+")
triple2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple3
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple4
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple5
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple6
((triple10) -> (rule1 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
((triple3) -> (rule1 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
((triple7) -> (rule3 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
((((triple7) -> (rule6 % int2))) -> (rule1 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple7
The tiger is blue.
("tiger" "is" "blue" "+")
triple8
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple9
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple10
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple3) -> (rule2 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((triple7) -> (rule6 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
((triple10) -> (rule2 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
((((triple3) -> (rule2 % int2))) -> (rule7 % int1))
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
((((triple7) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
((((triple10) -> (rule2 % int2))) -> (rule7 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((((((triple7) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int3