The dog eats the rabbit. The dog is big. The dog is cold. The dog is red. The dog needs the rabbit. The dog does not see the rabbit. The rabbit eats the dog. The rabbit is big. The rabbit needs the dog. The rabbit does not see the dog. If something is red and it needs the dog then it sees the rabbit. If something eats the dog and the dog needs the rabbit then it is red. If the rabbit does not see the dog and the dog does not eat the rabbit then the rabbit needs the dog.
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is red.
("dog" "is" "red" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The dog does not see the rabbit.
("dog" "sees" "rabbit" "-")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit does not see the dog.
("rabbit" "sees" "dog" "-")
If something is red and it needs the dog then it sees the rabbit.
((("something" "is" "red" "+") ("something" "needs" "dog" "+")) -> ("something" "sees" "rabbit" "+"))
If something eats the dog and the dog needs the rabbit then it is red.
((("something" "eats" "dog" "+") ("dog" "needs" "rabbit" "+")) -> ("something" "is" "red" "+"))
If the rabbit does not see the dog and the dog does not eat the rabbit then the rabbit needs the dog.
((("rabbit" "sees" "dog" "~") ("dog" "eats" "rabbit" "~")) -> ("rabbit" "needs" "dog" "+"))
The rabbit does not see the dog.
True
1
proof
[(triple10)]
("rabbit" "sees" "dog" "-")
triple10
The dog sees the rabbit.
False
1
inv-proof
[(triple6)]
("dog" "sees" "rabbit" "+")
triple6
The rabbit is red.
True
3
proof
[(((triple7 triple5) -> rule2))]
("rabbit" "is" "red" "+")
((triple7 triple5) -> (rule2 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is not red.
False
3
inv-proof
[(((triple7 triple5) -> rule2))]
("rabbit" "is" "red" "-")
((triple7 triple5) -> (rule2 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit sees the rabbit.
True
5
proof
[(((((triple7 triple5) -> rule2) triple9) -> rule1))]
("rabbit" "sees" "rabbit" "+")
((((triple7 triple5) -> (rule2 % int2)) triple9) -> (rule1 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit does not see the rabbit.
False
5
inv-proof
[(((((triple7 triple5) -> rule2) triple9) -> rule1))]
("rabbit" "sees" "rabbit" "-")
((((triple7 triple5) -> (rule2 % int2)) triple9) -> (rule1 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit is not blue.
Unknown
inv-random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
The dog is not nice.
Unknown
inv-random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
@0: The dog does not see the rabbit.[(triple6)] The dog eats the rabbit.[(triple1)] The dog is big.[(triple2)] The dog is cold.[(triple3)] The dog is red.[(triple4)] The dog needs the rabbit.[(triple5)] The rabbit does not see the dog.[(triple10)] The rabbit eats the dog.[(triple7)] The rabbit is big.[(triple8)] The rabbit needs the dog.[(triple9)] @1: The rabbit is red.[(((triple7 triple5) -> rule2))] @2: The rabbit sees the rabbit.[(((((triple7 triple5) -> rule2) triple9) -> rule1))]
The dog does not see the rabbit.
("dog" "sees" "rabbit" "-")
triple6
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
triple1
The dog is big.
("dog" "is" "big" "+")
triple2
The dog is cold.
("dog" "is" "cold" "+")
triple3
The dog is red.
("dog" "is" "red" "+")
triple4
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple5
The rabbit does not see the dog.
("rabbit" "sees" "dog" "-")
triple10
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple7
The rabbit is big.
("rabbit" "is" "big" "+")
triple8
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple9
The rabbit is red.
("rabbit" "is" "red" "+")
((triple7 triple5) -> (rule2 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((((triple7 triple5) -> (rule2 % int2)) triple9) -> (rule1 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2