The cow chases the dog. The cow chases the rabbit. The cow needs the dog. The dog chases the cow. The dog needs the cow. The rabbit chases the dog. The rabbit is red. The rabbit is round. The rabbit does not need the dog. The rabbit visits the dog. If someone is cold and they visit the dog then they visit the rabbit. If someone needs the rabbit then they chase the cow. If someone chases the cow and they are cold then they visit the cow. If someone is round then they are cold. If the dog chases the cow then the dog needs the rabbit. If someone needs the rabbit then the rabbit does not need the cow.
The cow chases the dog.
("cow" "chases" "dog" "+")
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The cow needs the dog.
("cow" "needs" "dog" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit does not need the dog.
("rabbit" "needs" "dog" "-")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
If someone is cold and they visit the dog then they visit the rabbit.
((("someone" "is" "cold" "+") ("someone" "visits" "dog" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone needs the rabbit then they chase the cow.
((("someone" "needs" "rabbit" "+")) -> ("someone" "chases" "cow" "+"))
If someone chases the cow and they are cold then they visit the cow.
((("someone" "chases" "cow" "+") ("someone" "is" "cold" "+")) -> ("someone" "visits" "cow" "+"))
If someone is round then they are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
If the dog chases the cow then the dog needs the rabbit.
((("dog" "chases" "cow" "+")) -> ("dog" "needs" "rabbit" "+"))
If someone needs the rabbit then the rabbit does not need the cow.
((("someone" "needs" "rabbit" "+")) -> ("rabbit" "needs" "cow" "-"))
The dog needs the cow.
True
1
proof
[(triple5)]
("dog" "needs" "cow" "+")
triple5
The cow does not chase the rabbit.
False
1
inv-proof
[(triple2)]
("cow" "chases" "rabbit" "-")
triple2
The rabbit is cold.
True
2
proof
[(((triple8) -> rule4))]
("rabbit" "is" "cold" "+")
((triple8) -> (rule4 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The dog does not need the rabbit.
False
2
inv-proof
[(((triple4) -> rule5))]
("dog" "needs" "rabbit" "-")
((triple4) -> (rule5 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The rabbit visits the rabbit.
True
4
proof
[(((((triple8) -> rule4) triple10) -> rule1))]
("rabbit" "visits" "rabbit" "+")
((((triple8) -> (rule4 % int2)) triple10) -> (rule1 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit does not visit the rabbit.
False
4
inv-proof
[(((((triple8) -> rule4) triple10) -> rule1))]
("rabbit" "visits" "rabbit" "-")
((((triple8) -> (rule4 % int2)) triple10) -> (rule1 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit does not visit the cow.
Unknown
inv-rconc
[@2: The rabbit visits the cow.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("rabbit" "visits" "cow" "-")
The cow visits the cow.
Unknown
rconc
[@2: The cow visits the cow.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("cow" "visits" "cow" "+")
The rabbit does not chase the cow.
Unknown
inv-rconc
[@1: The rabbit chases the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "chases" "cow" "-")
The dog is green.
Unknown
random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "+")
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 cow needs the rabbit.
Unknown
random
[@0: The cow needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "rabbit" "+")
@0: The cow chases the dog.[(triple1)] The cow chases the rabbit.[(triple2)] The cow needs the dog.[(triple3)] The dog chases the cow.[(triple4)] The dog needs the cow.[(triple5)] The rabbit chases the dog.[(triple6)] The rabbit does not need the dog.[(triple9)] The rabbit is red.[(triple7)] The rabbit is round.[(triple8)] The rabbit visits the dog.[(triple10)] @1: The dog needs the rabbit.[(((triple4) -> rule5))] The rabbit is cold.[(((triple8) -> rule4))] @2: The rabbit does not need the cow.[(((((triple4) -> rule5)) -> rule6))] The rabbit visits the rabbit.[(((((triple8) -> rule4) triple10) -> rule1))]
The cow chases the dog.
("cow" "chases" "dog" "+")
triple1
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple2
The cow needs the dog.
("cow" "needs" "dog" "+")
triple3
The dog chases the cow.
("dog" "chases" "cow" "+")
triple4
The dog needs the cow.
("dog" "needs" "cow" "+")
triple5
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple6
The rabbit does not need the dog.
("rabbit" "needs" "dog" "-")
triple9
The rabbit is red.
("rabbit" "is" "red" "+")
triple7
The rabbit is round.
("rabbit" "is" "round" "+")
triple8
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple10
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
((triple4) -> (rule5 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
((triple8) -> (rule4 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit does not need the cow.
("rabbit" "needs" "cow" "-")
((((triple4) -> (rule5 % int2))) -> (rule6 % int1))
The rabbit does not need the cow.
("rabbit" "needs" "cow" "-")
int1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((((triple8) -> (rule4 % int2)) triple10) -> (rule1 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2