The cow chases the rabbit. The cow is blue. The cow is green. The cow is nice. The cow is rough. The cow needs the rabbit. The cow visits the rabbit. The rabbit chases the cow. The rabbit is blue. The rabbit needs the cow. Rough people are cold. If someone is cold then they do not need the cow. If someone visits the cow then they chase the rabbit. If someone visits the cow then they chase the rabbit. If someone chases the rabbit and the rabbit is rough then the rabbit visits the cow. If someone visits the rabbit and they are not rough then they are green. If someone chases the rabbit then the rabbit is not nice. If someone needs the rabbit then the rabbit is not green.
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
Rough people are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold then they do not need the cow.
((("someone" "is" "cold" "+")) -> ("someone" "needs" "cow" "-"))
If someone visits the cow then they chase the rabbit.
((("someone" "visits" "cow" "+")) -> ("someone" "chases" "rabbit" "+"))
If someone visits the cow then they chase the rabbit.
((("someone" "visits" "cow" "+")) -> ("someone" "chases" "rabbit" "+"))
If someone chases the rabbit and the rabbit is rough then the rabbit visits the cow.
((("someone" "chases" "rabbit" "+") ("rabbit" "is" "rough" "+")) -> ("rabbit" "visits" "cow" "+"))
If someone visits the rabbit and they are not rough then they are green.
((("someone" "visits" "rabbit" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "green" "+"))
If someone chases the rabbit then the rabbit is not nice.
((("someone" "chases" "rabbit" "+")) -> ("rabbit" "is" "nice" "-"))
If someone needs the rabbit then the rabbit is not green.
((("someone" "needs" "rabbit" "+")) -> ("rabbit" "is" "green" "-"))
The cow is green.
True
1
proof
[(triple3)]
("cow" "is" "green" "+")
triple3
The cow does not visit the rabbit.
False
1
inv-proof
[(triple7)]
("cow" "visits" "rabbit" "-")
triple7
The rabbit is not nice.
True
2
proof
[(((triple1) -> rule7))]
("rabbit" "is" "nice" "-")
((triple1) -> (rule7 % int1))
The rabbit is not nice.
("rabbit" "is" "nice" "-")
int1
The rabbit is green.
False
2
inv-proof
[(((triple6) -> rule8))]
("rabbit" "is" "green" "+")
((triple6) -> (rule8 % int1))
The rabbit is not green.
("rabbit" "is" "green" "-")
int1
The cow does not need the cow.
True
3
proof
[(((((triple5) -> rule1)) -> rule2))]
("cow" "needs" "cow" "-")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The cow does not need the cow.
("cow" "needs" "cow" "-")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow needs the cow.
False
3
inv-proof
[(((((triple5) -> rule1)) -> rule2))]
("cow" "needs" "cow" "+")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The cow does not need the cow.
("cow" "needs" "cow" "-")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The rabbit does not chase the rabbit.
Unknown
inv-rconc
[@2: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("rabbit" "chases" "rabbit" "-")
The rabbit is cold.
Unknown
rconc
[@1: The rabbit is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "cold" "+")
The rabbit does not visit the cow.
Unknown
inv-rconc
[@1: The rabbit visits the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "visits" "cow" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
@0: The cow chases the rabbit.[(triple1)] The cow is blue.[(triple2)] The cow is green.[(triple3)] The cow is nice.[(triple4)] The cow is rough.[(triple5)] The cow needs the rabbit.[(triple6)] The cow visits the rabbit.[(triple7)] The rabbit chases the cow.[(triple8)] The rabbit is blue.[(triple9)] The rabbit needs the cow.[(triple10)] @1: The cow is cold.[(((triple5) -> rule1))] The rabbit is not green.[(((triple6) -> rule8))] The rabbit is not nice.[(((triple1) -> rule7))] @2: The cow does not need the cow.[(((((triple5) -> rule1)) -> rule2))]
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The cow is green.
("cow" "is" "green" "+")
triple3
The cow is nice.
("cow" "is" "nice" "+")
triple4
The cow is rough.
("cow" "is" "rough" "+")
triple5
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple6
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
triple7
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
triple8
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple9
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple10
The cow is cold.
("cow" "is" "cold" "+")
((triple5) -> (rule1 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The rabbit is not green.
("rabbit" "is" "green" "-")
((triple6) -> (rule8 % int1))
The rabbit is not green.
("rabbit" "is" "green" "-")
int1
The rabbit is not nice.
("rabbit" "is" "nice" "-")
((triple1) -> (rule7 % int1))
The rabbit is not nice.
("rabbit" "is" "nice" "-")
int1
The cow does not need the cow.
("cow" "needs" "cow" "-")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The cow does not need the cow.
("cow" "needs" "cow" "-")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2