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