The cow eats the mouse. The cow is red. The cow is rough. The cow sees the dog. The dog eats the cow. The dog eats the mouse. The dog is cold. The dog is rough. The dog sees the cow. The dog sees the mouse. The dog visits the cow. The mouse eats the cow. The mouse eats the dog. The mouse is cold. The mouse sees the dog. The mouse visits the dog. If something visits the cow and it eats the mouse then the mouse eats the cow. If something visits the cow and it is round then it eats the dog. If something eats the dog then the dog is rough. If the cow is cold and the cow is nice then the cow visits the mouse. If something visits the mouse and it eats the mouse then the mouse visits the dog. If something is nice and rough then it visits the mouse. If something eats the cow then it sees the cow. If the dog eats the mouse then the mouse is cold.
The cow eats the mouse.
("cow" "eats" "mouse" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
If something visits the cow and it eats the mouse then the mouse eats the cow.
((("something" "visits" "cow" "+") ("something" "eats" "mouse" "+")) -> ("mouse" "eats" "cow" "+"))
If something visits the cow and it is round then it eats the dog.
((("something" "visits" "cow" "+") ("something" "is" "round" "+")) -> ("something" "eats" "dog" "+"))
If something eats the dog then the dog is rough.
((("something" "eats" "dog" "+")) -> ("dog" "is" "rough" "+"))
If the cow is cold and the cow is nice then the cow visits the mouse.
((("cow" "is" "cold" "+") ("cow" "is" "nice" "+")) -> ("cow" "visits" "mouse" "+"))
If something visits the mouse and it eats the mouse then the mouse visits the dog.
((("something" "visits" "mouse" "+") ("something" "eats" "mouse" "+")) -> ("mouse" "visits" "dog" "+"))
If something is nice and rough then it visits the mouse.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "visits" "mouse" "+"))
If something eats the cow then it sees the cow.
((("something" "eats" "cow" "+")) -> ("something" "sees" "cow" "+"))
If the dog eats the mouse then the mouse is cold.
((("dog" "eats" "mouse" "+")) -> ("mouse" "is" "cold" "+"))
The mouse sees the dog.
True
1
proof
[(triple15)]
("mouse" "sees" "dog" "+")
triple15
The mouse is not cold.
False
1
inv-proof
[(triple14 OR ((triple6) -> rule8))]
("mouse" "is" "cold" "-")
triple14
((triple6) -> (rule8 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse sees the cow.
True
2
proof
[(((triple12) -> rule7) OR ((((triple11 triple6) -> rule1)) -> rule7))]
("mouse" "sees" "cow" "+")
((triple12) -> (rule7 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
((((triple11 triple6) -> (rule1 % int2))) -> (rule7 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int2
The mouse does not see the cow.
False
2
inv-proof
[(((triple12) -> rule7) OR ((((triple11 triple6) -> rule1)) -> rule7))]
("mouse" "sees" "cow" "-")
((triple12) -> (rule7 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
((((triple11 triple6) -> (rule1 % int2))) -> (rule7 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int2
The mouse does not visit the mouse.
Unknown
inv-rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "visits" "mouse" "-")
The dog eats the dog.
Unknown
rconc
[@1: The dog eats the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "eats" "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 dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
@0: The cow eats the mouse.[(triple1)] The cow is red.[(triple2)] The cow is rough.[(triple3)] The cow sees the dog.[(triple4)] The dog eats the cow.[(triple5)] The dog eats the mouse.[(triple6)] The dog is cold.[(triple7)] The dog is rough.[(triple8 OR ((triple13) -> rule3))] The dog sees the cow.[(triple9 OR ((triple5) -> rule7))] The dog sees the mouse.[(triple10)] The dog visits the cow.[(triple11)] The mouse eats the cow.[(triple12 OR ((triple11 triple6) -> rule1))] The mouse eats the dog.[(triple13)] The mouse is cold.[(triple14 OR ((triple6) -> rule8))] The mouse sees the dog.[(triple15)] The mouse visits the dog.[(triple16)] @1: The mouse sees the cow.[(((triple12) -> rule7) OR ((((triple11 triple6) -> rule1)) -> rule7))]
The cow eats the mouse.
("cow" "eats" "mouse" "+")
triple1
The cow is red.
("cow" "is" "red" "+")
triple2
The cow is rough.
("cow" "is" "rough" "+")
triple3
The cow sees the dog.
("cow" "sees" "dog" "+")
triple4
The dog eats the cow.
("dog" "eats" "cow" "+")
triple5
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple6
The dog is cold.
("dog" "is" "cold" "+")
triple7
The dog is rough.
("dog" "is" "rough" "+")
triple8
((triple13) -> (rule3 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The dog sees the cow.
("dog" "sees" "cow" "+")
triple9
((triple5) -> (rule7 % int1))
The dog sees the cow.
("dog" "sees" "cow" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple10
The dog visits the cow.
("dog" "visits" "cow" "+")
triple11
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple12
((triple11 triple6) -> (rule1 % int1))
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int1
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple13
The mouse is cold.
("mouse" "is" "cold" "+")
triple14
((triple6) -> (rule8 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple15
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple16
The mouse sees the cow.
("mouse" "sees" "cow" "+")
((triple12) -> (rule7 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
((((triple11 triple6) -> (rule1 % int2))) -> (rule7 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int2