The cow visits the dog. The dog visits the cow. The mouse visits the dog. If the dog is young then the dog is not cold. If someone visits the dog then they are cold. If someone likes the dog then they do not visit the dog. If the dog visits the cow then the dog is young. If the cow visits the dog and the cow does not like the mouse then the cow is green. If someone visits the dog then the dog likes the mouse.
The cow visits the dog.
("cow" "visits" "dog" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
If the dog is young then the dog is not cold.
((("dog" "is" "young" "+")) -> ("dog" "is" "cold" "-"))
If someone visits the dog then they are cold.
((("someone" "visits" "dog" "+")) -> ("someone" "is" "cold" "+"))
If someone likes the dog then they do not visit the dog.
((("someone" "likes" "dog" "+")) -> ("someone" "visits" "dog" "-"))
If the dog visits the cow then the dog is young.
((("dog" "visits" "cow" "+")) -> ("dog" "is" "young" "+"))
If the cow visits the dog and the cow does not like the mouse then the cow is green.
((("cow" "visits" "dog" "+") ("cow" "likes" "mouse" "~")) -> ("cow" "is" "green" "+"))
If someone visits the dog then the dog likes the mouse.
((("someone" "visits" "dog" "+")) -> ("dog" "likes" "mouse" "+"))
The mouse visits the dog.
True
1
proof
[(triple3)]
("mouse" "visits" "dog" "+")
triple3
The cow does not visit the dog.
False
1
inv-proof
[(triple1)]
("cow" "visits" "dog" "-")
triple1
The dog is young.
True
2
proof
[(((triple2) -> rule4))]
("dog" "is" "young" "+")
((triple2) -> (rule4 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is not young.
False
2
inv-proof
[(((triple2) -> rule4))]
("dog" "is" "young" "-")
((triple2) -> (rule4 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is not cold.
True
3
proof
[(((((triple2) -> rule4)) -> rule1))]
("dog" "is" "cold" "-")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
The dog is not cold.
("dog" "is" "cold" "-")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog is cold.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule1))]
("dog" "is" "cold" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
The dog is not cold.
("dog" "is" "cold" "-")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The cow is not green.
Unknown
inv-rconc
[@1: The cow is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "is" "green" "-")
The cow sees the dog.
Unknown
random
[@0: The cow sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "dog" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
The dog does not like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The mouse sees the dog.
Unknown
random
[@0: The mouse sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "dog" "+")
@0: The cow visits the dog.[(triple1)] The dog visits the cow.[(triple2)] The mouse visits the dog.[(triple3)] @1: The cow is cold.[(((triple1) -> rule2))] The dog is young.[(((triple2) -> rule4))] The dog likes the mouse.[(((triple1) -> rule6) OR ((triple3) -> rule6))] The mouse is cold.[(((triple3) -> rule2))] @2: The dog is not cold.[(((((triple2) -> rule4)) -> rule1))]
The cow visits the dog.
("cow" "visits" "dog" "+")
triple1
The dog visits the cow.
("dog" "visits" "cow" "+")
triple2
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple3
The cow is cold.
("cow" "is" "cold" "+")
((triple1) -> (rule2 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The dog is young.
("dog" "is" "young" "+")
((triple2) -> (rule4 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
((triple1) -> (rule6 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
((triple3) -> (rule6 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
((triple3) -> (rule2 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The dog is not cold.
("dog" "is" "cold" "-")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
The dog is not cold.
("dog" "is" "cold" "-")
int1
The dog is young.
("dog" "is" "young" "+")
int2