The cow is blue. The cow is nice. The cow likes the mouse. The cow needs the mouse. The cow sees the dog. The cow sees the mouse. The dog likes the cow. The dog sees the cow. The mouse is cold. The mouse is nice. If someone sees the cow and the cow likes the mouse then the cow needs the mouse. If someone likes the mouse then they need the dog. If the mouse is cold and the mouse needs the cow then the mouse is nice. If someone sees the dog and they see the cow then the dog likes the mouse. If someone likes the dog then they see the cow. If someone needs the dog then they are blue.
The cow is blue.
("cow" "is" "blue" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The dog likes the cow.
("dog" "likes" "cow" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
If someone sees the cow and the cow likes the mouse then the cow needs the mouse.
((("someone" "sees" "cow" "+") ("cow" "likes" "mouse" "+")) -> ("cow" "needs" "mouse" "+"))
If someone likes the mouse then they need the dog.
((("someone" "likes" "mouse" "+")) -> ("someone" "needs" "dog" "+"))
If the mouse is cold and the mouse needs the cow then the mouse is nice.
((("mouse" "is" "cold" "+") ("mouse" "needs" "cow" "+")) -> ("mouse" "is" "nice" "+"))
If someone sees the dog and they see the cow then the dog likes the mouse.
((("someone" "sees" "dog" "+") ("someone" "sees" "cow" "+")) -> ("dog" "likes" "mouse" "+"))
If someone likes the dog then they see the cow.
((("someone" "likes" "dog" "+")) -> ("someone" "sees" "cow" "+"))
If someone needs the dog then they are blue.
((("someone" "needs" "dog" "+")) -> ("someone" "is" "blue" "+"))
The cow is blue.
True
1
proof
[(triple1 OR ((((triple3) -> rule2)) -> rule6))]
("cow" "is" "blue" "+")
triple1
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow needs the dog.
("cow" "needs" "dog" "+")
int2
The cow does not need the mouse.
False
1
inv-proof
[(triple4 OR ((triple8 triple3) -> rule1))]
("cow" "needs" "mouse" "-")
triple4
((triple8 triple3) -> (rule1 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The cow needs the dog.
True
2
proof
[(((triple3) -> rule2))]
("cow" "needs" "dog" "+")
((triple3) -> (rule2 % int1))
The cow needs the dog.
("cow" "needs" "dog" "+")
int1
The cow does not need the dog.
False
2
inv-proof
[(((triple3) -> rule2))]
("cow" "needs" "dog" "-")
((triple3) -> (rule2 % int1))
The cow needs the dog.
("cow" "needs" "dog" "+")
int1
The mouse does not see the cow.
Unknown
inv-rconc
[@1: The mouse sees the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "sees" "cow" "-")
The dog is blue.
Unknown
rconc
[@4: The dog is blue.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule4 <- rule5 <- FAIL)]]
("dog" "is" "blue" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The mouse likes the dog.
Unknown
random
[@0: The mouse likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "dog" "+")
@0: The cow is blue.[(triple1 OR ((((triple3) -> rule2)) -> rule6))] The cow is nice.[(triple2)] The cow likes the mouse.[(triple3)] The cow needs the mouse.[(triple4 OR ((triple8 triple3) -> rule1))] The cow sees the dog.[(triple5)] The cow sees the mouse.[(triple6)] The dog likes the cow.[(triple7)] The dog sees the cow.[(triple8)] The mouse is cold.[(triple9)] The mouse is nice.[(triple10)] @1: The cow needs the dog.[(((triple3) -> rule2))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow needs the dog.
("cow" "needs" "dog" "+")
int2
The cow is nice.
("cow" "is" "nice" "+")
triple2
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple3
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple4
((triple8 triple3) -> (rule1 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
triple5
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple6
The dog likes the cow.
("dog" "likes" "cow" "+")
triple7
The dog sees the cow.
("dog" "sees" "cow" "+")
triple8
The mouse is cold.
("mouse" "is" "cold" "+")
triple9
The mouse is nice.
("mouse" "is" "nice" "+")
triple10
The cow needs the dog.
("cow" "needs" "dog" "+")
((triple3) -> (rule2 % int1))
The cow needs the dog.
("cow" "needs" "dog" "+")
int1