The cow chases the dog. The cow is blue. The cow is red. The cow is young. The cow likes the dog. The cow sees the dog. The dog chases the cow. The dog is green. The dog is nice. The dog is young. The dog likes the cow. The dog sees the cow. If someone is blue then they see the cow. If someone is young then they like the dog. If the cow sees the dog then the dog sees the cow. If someone is green then they chase the cow. If someone chases the cow then they see the dog. If someone chases the dog and the dog likes the cow then they are young. If the dog likes the cow and the cow chases the dog then the dog is red. If someone sees the cow then they are young.
The cow chases the dog.
("cow" "chases" "dog" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is young.
("cow" "is" "young" "+")
The cow likes the dog.
("cow" "likes" "dog" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog is young.
("dog" "is" "young" "+")
The dog likes the cow.
("dog" "likes" "cow" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
If someone is blue then they see the cow.
((("someone" "is" "blue" "+")) -> ("someone" "sees" "cow" "+"))
If someone is young then they like the dog.
((("someone" "is" "young" "+")) -> ("someone" "likes" "dog" "+"))
If the cow sees the dog then the dog sees the cow.
((("cow" "sees" "dog" "+")) -> ("dog" "sees" "cow" "+"))
If someone is green then they chase the cow.
((("someone" "is" "green" "+")) -> ("someone" "chases" "cow" "+"))
If someone chases the cow then they see the dog.
((("someone" "chases" "cow" "+")) -> ("someone" "sees" "dog" "+"))
If someone chases the dog and the dog likes the cow then they are young.
((("someone" "chases" "dog" "+") ("dog" "likes" "cow" "+")) -> ("someone" "is" "young" "+"))
If the dog likes the cow and the cow chases the dog then the dog is red.
((("dog" "likes" "cow" "+") ("cow" "chases" "dog" "+")) -> ("dog" "is" "red" "+"))
If someone sees the cow then they are young.
((("someone" "sees" "cow" "+")) -> ("someone" "is" "young" "+"))
The dog sees the cow.
True
1
proof
[(triple12 OR ((triple6) -> rule3))]
("dog" "sees" "cow" "+")
triple12
((triple6) -> (rule3 % int1))
The dog sees the cow.
("dog" "sees" "cow" "+")
int1
The cow is not red.
False
1
inv-proof
[(triple3)]
("cow" "is" "red" "-")
triple3
The dog sees the dog.
True
2
proof
[(((triple7) -> rule5) OR ((((triple8) -> rule4)) -> rule5))]
("dog" "sees" "dog" "+")
((triple7) -> (rule5 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
((((triple8) -> (rule4 % int2))) -> (rule5 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
int2
The dog does not see the dog.
False
2
inv-proof
[(((triple7) -> rule5) OR ((((triple8) -> rule4)) -> rule5))]
("dog" "sees" "dog" "-")
((triple7) -> (rule5 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
((((triple8) -> (rule4 % int2))) -> (rule5 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
int2
The cow does not chase the cow.
Unknown
inv-rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "chases" "cow" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
The cow is not nice.
Unknown
inv-random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
@0: The cow chases the dog.[(triple1)] The cow is blue.[(triple2)] The cow is red.[(triple3)] The cow is young.[(triple4 OR ((triple1 triple11) -> rule6) OR ((((triple2) -> rule1)) -> rule8))] The cow likes the dog.[(triple5 OR ((triple4) -> rule2) OR ((((triple1 triple11) -> rule6)) -> rule2) OR ((((((triple2) -> rule1)) -> rule8)) -> rule2))] The cow sees the dog.[(triple6)] The dog chases the cow.[(triple7 OR ((triple8) -> rule4))] The dog is green.[(triple8)] The dog is nice.[(triple9)] The dog is young.[(triple10 OR ((triple12) -> rule8) OR ((((triple6) -> rule3)) -> rule8))] The dog likes the cow.[(triple11)] The dog sees the cow.[(triple12 OR ((triple6) -> rule3))] @1: The cow sees the cow.[(((triple2) -> rule1))] The dog is red.[(((triple11 triple1) -> rule7))] The dog likes the dog.[(((triple10) -> rule2) OR ((((triple12) -> rule8)) -> rule2) OR ((((((triple6) -> rule3)) -> rule8)) -> rule2))] The dog sees the dog.[(((triple7) -> rule5) OR ((((triple8) -> rule4)) -> rule5))]
The cow chases the dog.
("cow" "chases" "dog" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The cow is red.
("cow" "is" "red" "+")
triple3
The cow is young.
("cow" "is" "young" "+")
triple4
((triple1 triple11) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The cow likes the dog.
("cow" "likes" "dog" "+")
triple5
((triple4) -> (rule2 % int1))
The cow likes the dog.
("cow" "likes" "dog" "+")
int1
((((triple1 triple11) -> (rule6 % int2))) -> (rule2 % int1))
The cow likes the dog.
("cow" "likes" "dog" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
((((((triple2) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The cow likes the dog.
("cow" "likes" "dog" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
int3
The cow sees the dog.
("cow" "sees" "dog" "+")
triple6
The dog chases the cow.
("dog" "chases" "cow" "+")
triple7
((triple8) -> (rule4 % int1))
The dog chases the cow.
("dog" "chases" "cow" "+")
int1
The dog is green.
("dog" "is" "green" "+")
triple8
The dog is nice.
("dog" "is" "nice" "+")
triple9
The dog is young.
("dog" "is" "young" "+")
triple10
((triple12) -> (rule8 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule8 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog sees the cow.
("dog" "sees" "cow" "+")
int2
The dog likes the cow.
("dog" "likes" "cow" "+")
triple11
The dog sees the cow.
("dog" "sees" "cow" "+")
triple12
((triple6) -> (rule3 % int1))
The dog sees the cow.
("dog" "sees" "cow" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
((triple2) -> (rule1 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The dog is red.
("dog" "is" "red" "+")
((triple11 triple1) -> (rule7 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
((triple10) -> (rule2 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
((((triple12) -> (rule8 % int2))) -> (rule2 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
((((((triple6) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog sees the cow.
("dog" "sees" "cow" "+")
int3
The dog sees the dog.
("dog" "sees" "dog" "+")
((triple7) -> (rule5 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
((((triple8) -> (rule4 % int2))) -> (rule5 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
int2