The cow needs the mouse. The dog eats the mouse. The mouse is rough. If someone eats the dog then the dog needs the mouse. If someone needs the mouse and they are rough then the mouse needs the cow. If someone needs the mouse then they eat the dog. If someone needs the cow and they eat the mouse then they need the dog. If someone eats the dog and the dog is cold then they are nice. If someone visits the mouse then they need the dog.
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
If someone eats the dog then the dog needs the mouse.
((("someone" "eats" "dog" "+")) -> ("dog" "needs" "mouse" "+"))
If someone needs the mouse and they are rough then the mouse needs the cow.
((("someone" "needs" "mouse" "+") ("someone" "is" "rough" "+")) -> ("mouse" "needs" "cow" "+"))
If someone needs the mouse then they eat the dog.
((("someone" "needs" "mouse" "+")) -> ("someone" "eats" "dog" "+"))
If someone needs the cow and they eat the mouse then they need the dog.
((("someone" "needs" "cow" "+") ("someone" "eats" "mouse" "+")) -> ("someone" "needs" "dog" "+"))
If someone eats the dog and the dog is cold then they are nice.
((("someone" "eats" "dog" "+") ("dog" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
If someone visits the mouse then they need the dog.
((("someone" "visits" "mouse" "+")) -> ("someone" "needs" "dog" "+"))
The mouse is rough.
True
1
proof
[(triple3)]
("mouse" "is" "rough" "+")
triple3
The mouse is not rough.
False
1
inv-proof
[(triple3)]
("mouse" "is" "rough" "-")
triple3
The cow eats the dog.
True
2
proof
[(((triple1) -> rule3))]
("cow" "eats" "dog" "+")
((triple1) -> (rule3 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The cow does not eat the dog.
False
2
inv-proof
[(((triple1) -> rule3))]
("cow" "eats" "dog" "-")
((triple1) -> (rule3 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The dog needs the mouse.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("dog" "needs" "mouse" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The cow eats the dog.
("cow" "eats" "dog" "+")
int2
The dog does not need the mouse.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("dog" "needs" "mouse" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The cow eats the dog.
("cow" "eats" "dog" "+")
int2
The dog eats the dog.
True
4
proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule3))]
("dog" "eats" "dog" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
The cow eats the dog.
("cow" "eats" "dog" "+")
int3
The dog does not eat the dog.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule3))]
("dog" "eats" "dog" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
The cow eats the dog.
("cow" "eats" "dog" "+")
int3
The cow is not nice.
Unknown
inv-rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "is" "nice" "-")
The mouse needs the cow.
Unknown
rconc
[@1: The mouse needs the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "needs" "cow" "+")
The dog is not nice.
Unknown
inv-rconc
[@1: The dog is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "nice" "-")
The cow needs the dog.
Unknown
rconc
[@1: The cow needs the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "needs" "dog" "+")
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 mouse visits the cow.
Unknown
random
[@0: The mouse visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "cow" "+")
The dog does not visit the cow.
Unknown
inv-random
[@0: The dog visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "cow" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
@0: The cow needs the mouse.[(triple1)] The dog eats the mouse.[(triple2)] The mouse is rough.[(triple3)] @1: The cow eats the dog.[(((triple1) -> rule3))] @2: The dog needs the mouse.[(((((triple1) -> rule3)) -> rule1))] @3: The dog eats the dog.[(((((((triple1) -> rule3)) -> rule1)) -> rule3))]
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple2
The mouse is rough.
("mouse" "is" "rough" "+")
triple3
The cow eats the dog.
("cow" "eats" "dog" "+")
((triple1) -> (rule3 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The cow eats the dog.
("cow" "eats" "dog" "+")
int2
The dog eats the dog.
("dog" "eats" "dog" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int2
The cow eats the dog.
("cow" "eats" "dog" "+")
int3