The dog is big. The rabbit likes the dog. If something likes the dog then it is kind. If the rabbit likes the dog and the rabbit sees the dog then the rabbit needs the dog. If something needs the rabbit then the rabbit sees the dog. If the rabbit needs the dog and the dog likes the rabbit then the dog sees the rabbit. If something sees the rabbit and it sees the dog then it is big. If something likes the dog then it needs the rabbit.
The dog is big.
("dog" "is" "big" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
If something likes the dog then it is kind.
((("something" "likes" "dog" "+")) -> ("something" "is" "kind" "+"))
If the rabbit likes the dog and the rabbit sees the dog then the rabbit needs the dog.
((("rabbit" "likes" "dog" "+") ("rabbit" "sees" "dog" "+")) -> ("rabbit" "needs" "dog" "+"))
If something needs the rabbit then the rabbit sees the dog.
((("something" "needs" "rabbit" "+")) -> ("rabbit" "sees" "dog" "+"))
If the rabbit needs the dog and the dog likes the rabbit then the dog sees the rabbit.
((("rabbit" "needs" "dog" "+") ("dog" "likes" "rabbit" "+")) -> ("dog" "sees" "rabbit" "+"))
If something sees the rabbit and it sees the dog then it is big.
((("something" "sees" "rabbit" "+") ("something" "sees" "dog" "+")) -> ("something" "is" "big" "+"))
If something likes the dog then it needs the rabbit.
((("something" "likes" "dog" "+")) -> ("something" "needs" "rabbit" "+"))
The dog is big.
True
1
proof
[(triple1)]
("dog" "is" "big" "+")
triple1
The dog is not big.
False
1
inv-proof
[(triple1)]
("dog" "is" "big" "-")
triple1
The rabbit needs the rabbit.
True
2
proof
[(((triple2) -> rule6))]
("rabbit" "needs" "rabbit" "+")
((triple2) -> (rule6 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is not kind.
False
2
inv-proof
[(((triple2) -> rule1))]
("rabbit" "is" "kind" "-")
((triple2) -> (rule1 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit sees the dog.
True
3
proof
[(((((triple2) -> rule6)) -> rule3))]
("rabbit" "sees" "dog" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit does not see the dog.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule3))]
("rabbit" "sees" "dog" "-")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit needs the dog.
True
5
proof
[(((triple2 ((((triple2) -> rule6)) -> rule3)) -> rule2))]
("rabbit" "needs" "dog" "+")
((triple2 ((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3
The rabbit does not need the dog.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule6)) -> rule3)) -> rule2))]
("rabbit" "needs" "dog" "-")
((triple2 ((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3
The dog is not kind.
Unknown
inv-rconc
[@1: The dog is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "kind" "-")
The dog needs the rabbit.
Unknown
rconc
[@1: The dog needs the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "needs" "rabbit" "+")
The dog does not see the rabbit.
Unknown
inv-rconc
[@1: The dog sees the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "sees" "rabbit" "-")
The rabbit is big.
Unknown
rconc
[@1: The rabbit is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "big" "+")
The dog is not blue.
Unknown
inv-random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
The rabbit is not red.
Unknown
inv-random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "-")
The rabbit is nice.
Unknown
random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "+")
@0: The dog is big.[(triple1)] The rabbit likes the dog.[(triple2)] @1: The rabbit is kind.[(((triple2) -> rule1))] The rabbit needs the rabbit.[(((triple2) -> rule6))] @2: The rabbit sees the dog.[(((((triple2) -> rule6)) -> rule3))] @3: The rabbit needs the dog.[(((triple2 ((((triple2) -> rule6)) -> rule3)) -> rule2))]
The dog is big.
("dog" "is" "big" "+")
triple1
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple2
The rabbit is kind.
("rabbit" "is" "kind" "+")
((triple2) -> (rule1 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple2) -> (rule6 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
((triple2 ((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3