The dog is blue. The dog needs the mouse. The dog sees the mouse. The dog sees the squirrel. The mouse is blue. The mouse needs the squirrel. The mouse sees the squirrel. The squirrel is kind. The squirrel needs the mouse. The squirrel sees the mouse. If the squirrel sees the mouse then the squirrel needs the dog. If something needs the mouse and it sees the squirrel then the squirrel is kind. If something needs the squirrel and it is blue then the squirrel is nice. If something needs the squirrel and it is blue then it needs the dog. If something needs the dog and it is round then the dog is nice. If something needs the squirrel then the squirrel needs the mouse. If something needs the dog and it needs the mouse then the dog chases the squirrel. All blue, kind things are nice.
The dog is blue.
("dog" "is" "blue" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
If the squirrel sees the mouse then the squirrel needs the dog.
((("squirrel" "sees" "mouse" "+")) -> ("squirrel" "needs" "dog" "+"))
If something needs the mouse and it sees the squirrel then the squirrel is kind.
((("something" "needs" "mouse" "+") ("something" "sees" "squirrel" "+")) -> ("squirrel" "is" "kind" "+"))
If something needs the squirrel and it is blue then the squirrel is nice.
((("something" "needs" "squirrel" "+") ("something" "is" "blue" "+")) -> ("squirrel" "is" "nice" "+"))
If something needs the squirrel and it is blue then it needs the dog.
((("something" "needs" "squirrel" "+") ("something" "is" "blue" "+")) -> ("something" "needs" "dog" "+"))
If something needs the dog and it is round then the dog is nice.
((("something" "needs" "dog" "+") ("something" "is" "round" "+")) -> ("dog" "is" "nice" "+"))
If something needs the squirrel then the squirrel needs the mouse.
((("something" "needs" "squirrel" "+")) -> ("squirrel" "needs" "mouse" "+"))
If something needs the dog and it needs the mouse then the dog chases the squirrel.
((("something" "needs" "dog" "+") ("something" "needs" "mouse" "+")) -> ("dog" "chases" "squirrel" "+"))
All blue, kind things are nice.
((("something" "is" "blue" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
The squirrel is kind.
True
1
proof
[(triple8 OR ((triple2 triple4) -> rule2))]
("squirrel" "is" "kind" "+")
triple8
((triple2 triple4) -> (rule2 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The mouse does not see the squirrel.
False
1
inv-proof
[(triple7)]
("mouse" "sees" "squirrel" "-")
triple7
The mouse needs the dog.
True
3
proof
[(((triple6 triple5) -> rule4))]
("mouse" "needs" "dog" "+")
((triple6 triple5) -> (rule4 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The squirrel is not nice.
False
3
inv-proof
[(((triple6 triple5) -> rule3))]
("squirrel" "is" "nice" "-")
((triple6 triple5) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The dog is not nice.
Unknown
inv-rconc
[@1: The dog is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "nice" "-")
The mouse is nice.
Unknown
rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "is" "nice" "+")
The mouse does not chase the squirrel.
Unknown
inv-random
[@0: The mouse chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "squirrel" "-")
The dog is cold.
Unknown
random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "+")
@0: The dog is blue.[(triple1)] The dog needs the mouse.[(triple2)] The dog sees the mouse.[(triple3)] The dog sees the squirrel.[(triple4)] The mouse is blue.[(triple5)] The mouse needs the squirrel.[(triple6)] The mouse sees the squirrel.[(triple7)] The squirrel is kind.[(triple8 OR ((triple2 triple4) -> rule2))] The squirrel needs the mouse.[(triple9 OR ((triple6) -> rule6))] The squirrel sees the mouse.[(triple10)] @1: The mouse needs the dog.[(((triple6 triple5) -> rule4))] The squirrel is nice.[(((triple6 triple5) -> rule3))] The squirrel needs the dog.[(((triple10) -> rule1))] @2: The dog chases the squirrel.[(((((triple10) -> rule1) triple9) -> rule7) OR ((((triple10) -> rule1) ((triple6) -> rule6)) -> rule7))]
The dog is blue.
("dog" "is" "blue" "+")
triple1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple2
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple3
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple4
The mouse is blue.
("mouse" "is" "blue" "+")
triple5
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple6
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple7
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple8
((triple2 triple4) -> (rule2 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple9
((triple6) -> (rule6 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple10
The mouse needs the dog.
("mouse" "needs" "dog" "+")
((triple6 triple5) -> (rule4 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
((triple6 triple5) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
((triple10) -> (rule1 % int1))
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
int1
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
((((triple10) -> (rule1 % int2)) triple9) -> (rule7 % int1))
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int1
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
int2
((((triple10) -> (rule1 % int3)) ((triple6) -> (rule6 % int2))) -> (rule7 % int1))
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
int3