The dog is big. The dog is green. The dog is kind. The dog likes the rabbit. The dog sees the rabbit. The dog visits the rabbit. The rabbit is green. The rabbit is rough. The rabbit is young. The rabbit likes the dog. The rabbit sees the dog. The rabbit visits the dog. If the dog sees the rabbit then the dog is kind. If someone visits the rabbit then they like the rabbit. If someone visits the dog and they are young then the dog sees the rabbit. If someone sees the dog and the dog likes the rabbit then the rabbit is kind. If the dog likes the rabbit and the dog is young then the rabbit is green. If someone sees the dog then they are big. If someone is big and they see the dog then the dog is rough. If someone likes the dog and the dog likes the rabbit then the rabbit visits the dog.
The dog is big.
("dog" "is" "big" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
If the dog sees the rabbit then the dog is kind.
((("dog" "sees" "rabbit" "+")) -> ("dog" "is" "kind" "+"))
If someone visits the rabbit then they like the rabbit.
((("someone" "visits" "rabbit" "+")) -> ("someone" "likes" "rabbit" "+"))
If someone visits the dog and they are young then the dog sees the rabbit.
((("someone" "visits" "dog" "+") ("someone" "is" "young" "+")) -> ("dog" "sees" "rabbit" "+"))
If someone sees the dog and the dog likes the rabbit then the rabbit is kind.
((("someone" "sees" "dog" "+") ("dog" "likes" "rabbit" "+")) -> ("rabbit" "is" "kind" "+"))
If the dog likes the rabbit and the dog is young then the rabbit is green.
((("dog" "likes" "rabbit" "+") ("dog" "is" "young" "+")) -> ("rabbit" "is" "green" "+"))
If someone sees the dog then they are big.
((("someone" "sees" "dog" "+")) -> ("someone" "is" "big" "+"))
If someone is big and they see the dog then the dog is rough.
((("someone" "is" "big" "+") ("someone" "sees" "dog" "+")) -> ("dog" "is" "rough" "+"))
If someone likes the dog and the dog likes the rabbit then the rabbit visits the dog.
((("someone" "likes" "dog" "+") ("dog" "likes" "rabbit" "+")) -> ("rabbit" "visits" "dog" "+"))
The dog sees the rabbit.
True
1
proof
[(triple5 OR ((triple12 triple9) -> rule3) OR ((((triple10 triple4) -> rule8) triple9) -> rule3) OR ((((triple10 ((triple6) -> rule2)) -> rule8) triple9) -> rule3))]
("dog" "sees" "rabbit" "+")
triple5
((triple12 triple9) -> (rule3 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
((((triple10 triple4) -> (rule8 % int2)) triple9) -> (rule3 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int2
((((triple10 ((triple6) -> (rule2 % int3))) -> (rule8 % int2)) triple9) -> (rule3 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int2
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int3
The dog does not visit the rabbit.
False
1
inv-proof
[(triple6)]
("dog" "visits" "rabbit" "-")
triple6
The rabbit is kind.
True
3
proof
[(((triple11 triple4) -> rule4) OR ((triple11 ((triple6) -> rule2)) -> rule4))]
("rabbit" "is" "kind" "+")
((triple11 triple4) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
((triple11 ((triple6) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int2
The rabbit is not big.
False
2
inv-proof
[(((triple11) -> rule6))]
("rabbit" "is" "big" "-")
((triple11) -> (rule6 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The dog is rough.
True
4
proof
[(((((triple11) -> rule6) triple11) -> rule7))]
("dog" "is" "rough" "+")
((((triple11) -> (rule6 % int2)) triple11) -> (rule7 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The dog is not rough.
False
4
inv-proof
[(((((triple11) -> rule6) triple11) -> rule7))]
("dog" "is" "rough" "-")
((((triple11) -> (rule6 % int2)) triple11) -> (rule7 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit does not like the rabbit.
Unknown
inv-rconc
[@1: The rabbit likes the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "likes" "rabbit" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "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 rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
The dog is not young.
Unknown
inv-random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
@0: The dog is big.[(triple1)] The dog is green.[(triple2)] The dog is kind.[(triple3 OR ((triple5) -> rule1) OR ((((triple12 triple9) -> rule3)) -> rule1) OR ((((((triple10 triple4) -> rule8) triple9) -> rule3)) -> rule1) OR ((((((triple10 ((triple6) -> rule2)) -> rule8) triple9) -> rule3)) -> rule1))] The dog likes the rabbit.[(triple4 OR ((triple6) -> rule2))] The dog sees the rabbit.[(triple5 OR ((triple12 triple9) -> rule3) OR ((((triple10 triple4) -> rule8) triple9) -> rule3) OR ((((triple10 ((triple6) -> rule2)) -> rule8) triple9) -> rule3))] The dog visits the rabbit.[(triple6)] The rabbit is green.[(triple7)] The rabbit is rough.[(triple8)] The rabbit is young.[(triple9)] The rabbit likes the dog.[(triple10)] The rabbit sees the dog.[(triple11)] The rabbit visits the dog.[(triple12 OR ((triple10 triple4) -> rule8) OR ((triple10 ((triple6) -> rule2)) -> rule8))] @1: The rabbit is big.[(((triple11) -> rule6))] The rabbit is kind.[(((triple11 triple4) -> rule4) OR ((triple11 ((triple6) -> rule2)) -> rule4))] @2: The dog is rough.[(((((triple11) -> rule6) triple11) -> rule7))]
The dog is big.
("dog" "is" "big" "+")
triple1
The dog is green.
("dog" "is" "green" "+")
triple2
The dog is kind.
("dog" "is" "kind" "+")
triple3
((triple5) -> (rule1 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
((((triple12 triple9) -> (rule3 % int2))) -> (rule1 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int2
((((((triple10 triple4) -> (rule8 % int3)) triple9) -> (rule3 % int2))) -> (rule1 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int2
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int3
((((((triple10 ((triple6) -> (rule2 % int4))) -> (rule8 % int3)) triple9) -> (rule3 % int2))) -> (rule1 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int2
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int3
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int4
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple4
((triple6) -> (rule2 % int1))
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple5
((triple12 triple9) -> (rule3 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
((((triple10 triple4) -> (rule8 % int2)) triple9) -> (rule3 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int2
((((triple10 ((triple6) -> (rule2 % int3))) -> (rule8 % int2)) triple9) -> (rule3 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int2
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int3
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple6
The rabbit is green.
("rabbit" "is" "green" "+")
triple7
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple8
The rabbit is young.
("rabbit" "is" "young" "+")
triple9
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple10
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple11
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple12
((triple10 triple4) -> (rule8 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
((triple10 ((triple6) -> (rule2 % int2))) -> (rule8 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
((triple11) -> (rule6 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
((triple11 triple4) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
((triple11 ((triple6) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int2
The dog is rough.
("dog" "is" "rough" "+")
((((triple11) -> (rule6 % int2)) triple11) -> (rule7 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2