The cow is young. The dog eats the cow. The dog is blue. The dog is kind. The dog sees the mouse. The mouse is nice. The mouse needs the dog. If something needs the dog then it sees the dog. If something eats the mouse then it eats the dog. If something eats the cow then the cow eats the mouse. If something is young and it needs the dog then it needs the mouse. If the dog needs the cow then the cow eats the dog. If something eats the dog and the dog sees the mouse then the mouse sees the cow.
The cow is young.
("cow" "is" "young" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
If something needs the dog then it sees the dog.
((("something" "needs" "dog" "+")) -> ("something" "sees" "dog" "+"))
If something eats the mouse then it eats the dog.
((("something" "eats" "mouse" "+")) -> ("something" "eats" "dog" "+"))
If something eats the cow then the cow eats the mouse.
((("something" "eats" "cow" "+")) -> ("cow" "eats" "mouse" "+"))
If something is young and it needs the dog then it needs the mouse.
((("something" "is" "young" "+") ("something" "needs" "dog" "+")) -> ("something" "needs" "mouse" "+"))
If the dog needs the cow then the cow eats the dog.
((("dog" "needs" "cow" "+")) -> ("cow" "eats" "dog" "+"))
If something eats the dog and the dog sees the mouse then the mouse sees the cow.
((("something" "eats" "dog" "+") ("dog" "sees" "mouse" "+")) -> ("mouse" "sees" "cow" "+"))
The cow is young.
True
1
proof
[(triple1)]
("cow" "is" "young" "+")
triple1
The dog is not blue.
False
1
inv-proof
[(triple3)]
("dog" "is" "blue" "-")
triple3
The mouse sees the dog.
True
2
proof
[(((triple7) -> rule1))]
("mouse" "sees" "dog" "+")
((triple7) -> (rule1 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
The mouse does not see the dog.
False
2
inv-proof
[(((triple7) -> rule1))]
("mouse" "sees" "dog" "-")
((triple7) -> (rule1 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
The cow eats the dog.
True
3
proof
[(((((triple2) -> rule3)) -> rule2))]
("cow" "eats" "dog" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int2
The cow does not eat the dog.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2))]
("cow" "eats" "dog" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int2
The cow does not see the dog.
Unknown
inv-rconc
[@1: The cow sees the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "sees" "dog" "-")
The dog needs the mouse.
Unknown
rconc
[@1: The dog needs the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "needs" "mouse" "+")
The mouse does not need the mouse.
Unknown
inv-rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "needs" "mouse" "-")
The dog needs the cow.
Unknown
random
[@0: The dog needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "cow" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The cow is young.[(triple1)] The dog eats the cow.[(triple2)] The dog is blue.[(triple3)] The dog is kind.[(triple4)] The dog sees the mouse.[(triple5)] The mouse is nice.[(triple6)] The mouse needs the dog.[(triple7)] @1: The cow eats the mouse.[(((triple2) -> rule3))] The mouse sees the dog.[(((triple7) -> rule1))] @2: The cow eats the dog.[(((((triple2) -> rule3)) -> rule2))] @3: The mouse sees the cow.[(((((((triple2) -> rule3)) -> rule2) triple5) -> rule6))]
The cow is young.
("cow" "is" "young" "+")
triple1
The dog eats the cow.
("dog" "eats" "cow" "+")
triple2
The dog is blue.
("dog" "is" "blue" "+")
triple3
The dog is kind.
("dog" "is" "kind" "+")
triple4
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple5
The mouse is nice.
("mouse" "is" "nice" "+")
triple6
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple7
The cow eats the mouse.
("cow" "eats" "mouse" "+")
((triple2) -> (rule3 % int1))
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
((triple7) -> (rule1 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
The cow eats the dog.
("cow" "eats" "dog" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int2
The mouse sees the cow.
("mouse" "sees" "cow" "+")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2)) triple5) -> (rule6 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The cow eats the dog.
("cow" "eats" "dog" "+")
int2
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int3