The dog is big. The dog is cold. The dog is nice. The dog is red. The dog likes the rabbit. The dog needs the rabbit. The rabbit chases the dog. The rabbit is big. The rabbit is cold. The rabbit is red. The rabbit likes the dog. The rabbit needs the dog. If something is big then it likes the dog. If the dog is young and the dog chases the rabbit then the rabbit needs the dog. If the rabbit needs the dog then the rabbit likes the dog. If something likes the dog then it chases the dog. If something needs the dog then it chases the dog. If something is young then it likes the dog.
The dog is big.
("dog" "is" "big" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is red.
("dog" "is" "red" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
If something is big then it likes the dog.
((("something" "is" "big" "+")) -> ("something" "likes" "dog" "+"))
If the dog is young and the dog chases the rabbit then the rabbit needs the dog.
((("dog" "is" "young" "+") ("dog" "chases" "rabbit" "+")) -> ("rabbit" "needs" "dog" "+"))
If the rabbit needs the dog then the rabbit likes the dog.
((("rabbit" "needs" "dog" "+")) -> ("rabbit" "likes" "dog" "+"))
If something likes the dog then it chases the dog.
((("something" "likes" "dog" "+")) -> ("something" "chases" "dog" "+"))
If something needs the dog then it chases the dog.
((("something" "needs" "dog" "+")) -> ("something" "chases" "dog" "+"))
If something is young then it likes the dog.
((("something" "is" "young" "+")) -> ("something" "likes" "dog" "+"))
The rabbit needs the dog.
True
1
proof
[(triple12)]
("rabbit" "needs" "dog" "+")
triple12
The rabbit does not need the dog.
False
1
inv-proof
[(triple12)]
("rabbit" "needs" "dog" "-")
triple12
The dog likes the dog.
True
2
proof
[(((triple1) -> rule1))]
("dog" "likes" "dog" "+")
((triple1) -> (rule1 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog does not like the dog.
False
2
inv-proof
[(((triple1) -> rule1))]
("dog" "likes" "dog" "-")
((triple1) -> (rule1 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog chases the dog.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("dog" "chases" "dog" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2
The dog does not chase the dog.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule4))]
("dog" "chases" "dog" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2
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 dog chases the rabbit.
Unknown
random
[@0: The dog chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "rabbit" "+")
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The dog is young.
Unknown
random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "+")
The rabbit is not young.
Unknown
inv-random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
@0: The dog is big.[(triple1)] The dog is cold.[(triple2)] The dog is nice.[(triple3)] The dog is red.[(triple4)] The dog likes the rabbit.[(triple5)] The dog needs the rabbit.[(triple6)] The rabbit chases the dog.[(triple7 OR ((triple11) -> rule4) OR ((triple12) -> rule5) OR ((((triple12) -> rule3)) -> rule4) OR ((((triple8) -> rule1)) -> rule4))] The rabbit is big.[(triple8)] The rabbit is cold.[(triple9)] The rabbit is red.[(triple10)] The rabbit likes the dog.[(triple11 OR ((triple12) -> rule3) OR ((triple8) -> rule1))] The rabbit needs the dog.[(triple12)] @1: The dog likes the dog.[(((triple1) -> rule1))] @2: The dog chases the dog.[(((((triple1) -> rule1)) -> rule4))]
The dog is big.
("dog" "is" "big" "+")
triple1
The dog is cold.
("dog" "is" "cold" "+")
triple2
The dog is nice.
("dog" "is" "nice" "+")
triple3
The dog is red.
("dog" "is" "red" "+")
triple4
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple5
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple6
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple7
((triple11) -> (rule4 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
((triple12) -> (rule5 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
((((triple12) -> (rule3 % int2))) -> (rule4 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int2
((((triple8) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
triple8
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple9
The rabbit is red.
("rabbit" "is" "red" "+")
triple10
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple11
((triple12) -> (rule3 % int1))
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int1
((triple8) -> (rule1 % int1))
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple12
The dog likes the dog.
("dog" "likes" "dog" "+")
((triple1) -> (rule1 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2