The bear is round. The bear needs the dog. The bear needs the mouse. The cat visits the mouse. The dog is round. The mouse is round. The mouse needs the bear. The mouse sees the bear. The mouse visits the cat. The mouse visits the dog. If something visits the dog then it is blue.
The bear is round.
("bear" "is" "round" "+")
The bear needs the dog.
("bear" "needs" "dog" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The dog is round.
("dog" "is" "round" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
If something visits the dog then it is blue.
((("something" "visits" "dog" "+")) -> ("something" "is" "blue" "+"))
The dog is round.
True
1
proof
[(triple5)]
("dog" "is" "round" "+")
triple5
The mouse does not visit the dog.
False
1
inv-proof
[(triple10)]
("mouse" "visits" "dog" "-")
triple10
The mouse is blue.
True
2
proof
[(((triple10) -> rule1))]
("mouse" "is" "blue" "+")
((triple10) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse is not blue.
False
2
inv-proof
[(((triple10) -> rule1))]
("mouse" "is" "blue" "-")
((triple10) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The dog is not blue.
Unknown
inv-rconc
[@1: The dog is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "blue" "-")
The bear is blue.
Unknown
rconc
[@1: The bear is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "blue" "+")
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
@0: The bear is round.[(triple1)] The bear needs the dog.[(triple2)] The bear needs the mouse.[(triple3)] The cat visits the mouse.[(triple4)] The dog is round.[(triple5)] The mouse is round.[(triple6)] The mouse needs the bear.[(triple7)] The mouse sees the bear.[(triple8)] The mouse visits the cat.[(triple9)] The mouse visits the dog.[(triple10)] @1: The mouse is blue.[(((triple10) -> rule1))]
The bear is round.
("bear" "is" "round" "+")
triple1
The bear needs the dog.
("bear" "needs" "dog" "+")
triple2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple3
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple4
The dog is round.
("dog" "is" "round" "+")
triple5
The mouse is round.
("mouse" "is" "round" "+")
triple6
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple7
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple8
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple9
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple10
The mouse is blue.
("mouse" "is" "blue" "+")
((triple10) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1