The cat is green. The cat sees the squirrel. The dog is green. The dog likes the rabbit. The dog needs the cat. The dog needs the squirrel. The rabbit sees the cat. The rabbit sees the squirrel. The squirrel is red. The squirrel likes the rabbit. If something sees the dog and the dog is big then it is red. If something likes the rabbit then it is nice. If something is kind and it likes the dog then the dog is green.
The cat is green.
("cat" "is" "green" "+")
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
The dog is green.
("dog" "is" "green" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
If something sees the dog and the dog is big then it is red.
((("something" "sees" "dog" "+") ("dog" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something likes the rabbit then it is nice.
((("something" "likes" "rabbit" "+")) -> ("something" "is" "nice" "+"))
If something is kind and it likes the dog then the dog is green.
((("something" "is" "kind" "+") ("something" "likes" "dog" "+")) -> ("dog" "is" "green" "+"))
The dog needs the cat.
True
1
proof
[(triple5)]
("dog" "needs" "cat" "+")
triple5
The rabbit does not see the cat.
False
1
inv-proof
[(triple7)]
("rabbit" "sees" "cat" "-")
triple7
The dog is nice.
True
2
proof
[(((triple4) -> rule2))]
("dog" "is" "nice" "+")
((triple4) -> (rule2 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is not nice.
False
2
inv-proof
[(((triple4) -> rule2))]
("dog" "is" "nice" "-")
((triple4) -> (rule2 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The rabbit is not nice.
Unknown
inv-rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "nice" "-")
The dog is red.
Unknown
rconc
[@1: The dog is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "red" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The dog is kind.
Unknown
random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "+")
@0: The cat is green.[(triple1)] The cat sees the squirrel.[(triple2)] The dog is green.[(triple3)] The dog likes the rabbit.[(triple4)] The dog needs the cat.[(triple5)] The dog needs the squirrel.[(triple6)] The rabbit sees the cat.[(triple7)] The rabbit sees the squirrel.[(triple8)] The squirrel is red.[(triple9)] The squirrel likes the rabbit.[(triple10)] @1: The dog is nice.[(((triple4) -> rule2))] The squirrel is nice.[(((triple10) -> rule2))]
The cat is green.
("cat" "is" "green" "+")
triple1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
triple2
The dog is green.
("dog" "is" "green" "+")
triple3
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple4
The dog needs the cat.
("dog" "needs" "cat" "+")
triple5
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
triple6
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple7
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple8
The squirrel is red.
("squirrel" "is" "red" "+")
triple9
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
triple10
The dog is nice.
("dog" "is" "nice" "+")
((triple4) -> (rule2 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
((triple10) -> (rule2 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1