The dog is blue. The dog is cold. The dog is green. The dog is rough. The dog needs the rabbit. The dog sees the rabbit. The dog visits the rabbit. The rabbit is blue. The rabbit is cold. The rabbit is green. The rabbit is kind. The rabbit is rough. The rabbit needs the dog. The rabbit sees the dog. The rabbit visits the dog. If something is rough and blue then it needs the rabbit. If something needs the dog and it visits the rabbit then the rabbit needs the dog. If something is kind and green then it visits the dog.
The dog is blue.
("dog" "is" "blue" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
If something is rough and blue then it needs the rabbit.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "needs" "rabbit" "+"))
If something needs the dog and it visits the rabbit then the rabbit needs the dog.
((("something" "needs" "dog" "+") ("something" "visits" "rabbit" "+")) -> ("rabbit" "needs" "dog" "+"))
If something is kind and green then it visits the dog.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "visits" "dog" "+"))
The rabbit needs the dog.
True
1
proof
[(triple13)]
("rabbit" "needs" "dog" "+")
triple13
The rabbit is not kind.
False
1
inv-proof
[(triple11)]
("rabbit" "is" "kind" "-")
triple11
The rabbit needs the rabbit.
True
3
proof
[(((triple12 triple8) -> rule1))]
("rabbit" "needs" "rabbit" "+")
((triple12 triple8) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit does not need the rabbit.
False
3
inv-proof
[(((triple12 triple8) -> rule1))]
("rabbit" "needs" "rabbit" "-")
((triple12 triple8) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The dog does not visit the dog.
Unknown
inv-rconc
[@1: The dog visits the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "visits" "dog" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
@0: The dog is blue.[(triple1)] The dog is cold.[(triple2)] The dog is green.[(triple3)] The dog is rough.[(triple4)] The dog needs the rabbit.[(triple5 OR ((triple4 triple1) -> rule1))] The dog sees the rabbit.[(triple6)] The dog visits the rabbit.[(triple7)] The rabbit is blue.[(triple8)] The rabbit is cold.[(triple9)] The rabbit is green.[(triple10)] The rabbit is kind.[(triple11)] The rabbit is rough.[(triple12)] The rabbit needs the dog.[(triple13)] The rabbit sees the dog.[(triple14)] The rabbit visits the dog.[(triple15 OR ((triple11 triple10) -> rule3))] @1: The rabbit needs the rabbit.[(((triple12 triple8) -> rule1))]
The dog is blue.
("dog" "is" "blue" "+")
triple1
The dog is cold.
("dog" "is" "cold" "+")
triple2
The dog is green.
("dog" "is" "green" "+")
triple3
The dog is rough.
("dog" "is" "rough" "+")
triple4
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple5
((triple4 triple1) -> (rule1 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple6
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple7
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple8
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple9
The rabbit is green.
("rabbit" "is" "green" "+")
triple10
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple11
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple12
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple13
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple14
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple15
((triple11 triple10) -> (rule3 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple12 triple8) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1