The bear is kind. The bear sees the dog. The cow chases the dog. The cow chases the rabbit. The cow is cold. The cow does not see the dog. The cow sees the rabbit. The cow visits the rabbit. The dog chases the cow. The dog is not cold. The dog is not green. The dog is rough. The dog sees the rabbit. The dog visits the cow. The dog visits the rabbit. The rabbit is big. If something chases the dog and it chases the bear then the dog is green. If something visits the rabbit and it visits the bear then the rabbit chases the dog. If something chases the dog and it is cold then the dog visits the rabbit. If something chases the dog and the dog is not green then it is kind. If something visits the rabbit and it is kind then the rabbit is kind. If something is big and kind then it does not see the bear.
The bear is kind.
("bear" "is" "kind" "+")
The bear sees the dog.
("bear" "sees" "dog" "+")
The cow chases the dog.
("cow" "chases" "dog" "+")
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow does not see the dog.
("cow" "sees" "dog" "-")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The dog is not cold.
("dog" "is" "cold" "-")
The dog is not green.
("dog" "is" "green" "-")
The dog is rough.
("dog" "is" "rough" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
If something chases the dog and it chases the bear then the dog is green.
((("something" "chases" "dog" "+") ("something" "chases" "bear" "+")) -> ("dog" "is" "green" "+"))
If something visits the rabbit and it visits the bear then the rabbit chases the dog.
((("something" "visits" "rabbit" "+") ("something" "visits" "bear" "+")) -> ("rabbit" "chases" "dog" "+"))
If something chases the dog and it is cold then the dog visits the rabbit.
((("something" "chases" "dog" "+") ("something" "is" "cold" "+")) -> ("dog" "visits" "rabbit" "+"))
If something chases the dog and the dog is not green then it is kind.
((("something" "chases" "dog" "+") ("dog" "is" "green" "~")) -> ("something" "is" "kind" "+"))
If something visits the rabbit and it is kind then the rabbit is kind.
((("something" "visits" "rabbit" "+") ("something" "is" "kind" "+")) -> ("rabbit" "is" "kind" "+"))
If something is big and kind then it does not see the bear.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "sees" "bear" "-"))
The dog chases the cow.
True
1
proof
[(triple9)]
("dog" "chases" "cow" "+")
triple9
The cow sees the dog.
False
1
inv-proof
[(triple6)]
("cow" "sees" "dog" "+")
triple6
The cow is kind.
True
3
proof
[(((triple3 triple11) -> rule4))]
("cow" "is" "kind" "+")
((triple3 triple11) -> (rule4 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is not kind.
False
3
inv-proof
[(((triple3 triple11) -> rule4))]
("cow" "is" "kind" "-")
((triple3 triple11) -> (rule4 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The rabbit is kind.
True
5
proof
[(((triple8 ((triple3 triple11) -> rule4)) -> rule5))]
("rabbit" "is" "kind" "+")
((triple8 ((triple3 triple11) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The rabbit is not kind.
False
5
inv-proof
[(((triple8 ((triple3 triple11) -> rule4)) -> rule5))]
("rabbit" "is" "kind" "-")
((triple8 ((triple3 triple11) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The rabbit does not see the bear.
True
7
proof
[(((triple16 ((triple8 ((triple3 triple11) -> rule4)) -> rule5)) -> rule6))]
("rabbit" "sees" "bear" "-")
((triple16 ((triple8 ((triple3 triple11) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The rabbit does not see the bear.
("rabbit" "sees" "bear" "-")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
The rabbit sees the bear.
False
7
inv-proof
[(((triple16 ((triple8 ((triple3 triple11) -> rule4)) -> rule5)) -> rule6))]
("rabbit" "sees" "bear" "+")
((triple16 ((triple8 ((triple3 triple11) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The rabbit does not see the bear.
("rabbit" "sees" "bear" "-")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
The dog is not kind.
Unknown
inv-rconc
[@1: The dog is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "is" "kind" "-")
The rabbit chases the dog.
Unknown
rconc
[@1: The rabbit chases the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "chases" "dog" "+")
The dog does not see the cow.
Unknown
inv-random
[@0: The dog sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "cow" "-")
The bear visits the dog.
Unknown
random
[@0: The bear visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "dog" "+")
The bear is not big.
Unknown
inv-random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "-")
The bear visits the cow.
Unknown
random
[@0: The bear visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "cow" "+")
The cow does not chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "-")
The bear is green.
Unknown
random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "+")
@0: The bear is kind.[(triple1)] The bear sees the dog.[(triple2)] The cow chases the dog.[(triple3)] The cow chases the rabbit.[(triple4)] The cow does not see the dog.[(triple6)] The cow is cold.[(triple5)] The cow sees the rabbit.[(triple7)] The cow visits the rabbit.[(triple8)] The dog chases the cow.[(triple9)] The dog is not cold.[(triple10)] The dog is not green.[(triple11)] The dog is rough.[(triple12)] The dog sees the rabbit.[(triple13)] The dog visits the cow.[(triple14)] The dog visits the rabbit.[(triple15 OR ((triple3 triple5) -> rule3))] The rabbit is big.[(triple16)] @1: The cow is kind.[(((triple3 triple11) -> rule4))] @2: The rabbit is kind.[(((triple8 ((triple3 triple11) -> rule4)) -> rule5))] @3: The rabbit does not see the bear.[(((triple16 ((triple8 ((triple3 triple11) -> rule4)) -> rule5)) -> rule6))]
The bear is kind.
("bear" "is" "kind" "+")
triple1
The bear sees the dog.
("bear" "sees" "dog" "+")
triple2
The cow chases the dog.
("cow" "chases" "dog" "+")
triple3
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple4
The cow does not see the dog.
("cow" "sees" "dog" "-")
triple6
The cow is cold.
("cow" "is" "cold" "+")
triple5
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple7
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
triple8
The dog chases the cow.
("dog" "chases" "cow" "+")
triple9
The dog is not cold.
("dog" "is" "cold" "-")
triple10
The dog is not green.
("dog" "is" "green" "-")
triple11
The dog is rough.
("dog" "is" "rough" "+")
triple12
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple13
The dog visits the cow.
("dog" "visits" "cow" "+")
triple14
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple15
((triple3 triple5) -> (rule3 % int1))
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
triple16
The cow is kind.
("cow" "is" "kind" "+")
((triple3 triple11) -> (rule4 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
((triple8 ((triple3 triple11) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The rabbit does not see the bear.
("rabbit" "sees" "bear" "-")
((triple16 ((triple8 ((triple3 triple11) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The rabbit does not see the bear.
("rabbit" "sees" "bear" "-")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3