The dog chases the squirrel. The dog is cold. The dog sees the tiger. The dog visits the mouse. The mouse is blue. The mouse is kind. The mouse is rough. The squirrel chases the dog. The squirrel chases the tiger. The squirrel is cold. The squirrel sees the mouse. The tiger is cold. Kind things are cold.
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
Kind things are cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
The squirrel sees the mouse.
True
1
proof
[(triple11)]
("squirrel" "sees" "mouse" "+")
triple11
The mouse is not blue.
False
1
inv-proof
[(triple5)]
("mouse" "is" "blue" "-")
triple5
The mouse is cold.
True
2
proof
[(((triple6) -> rule1))]
("mouse" "is" "cold" "+")
((triple6) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse is not cold.
False
2
inv-proof
[(((triple6) -> rule1))]
("mouse" "is" "cold" "-")
((triple6) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
The mouse does not chase the dog.
Unknown
inv-random
[@0: The mouse chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "dog" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
@0: The dog chases the squirrel.[(triple1)] The dog is cold.[(triple2)] The dog sees the tiger.[(triple3)] The dog visits the mouse.[(triple4)] The mouse is blue.[(triple5)] The mouse is kind.[(triple6)] The mouse is rough.[(triple7)] The squirrel chases the dog.[(triple8)] The squirrel chases the tiger.[(triple9)] The squirrel is cold.[(triple10)] The squirrel sees the mouse.[(triple11)] The tiger is cold.[(triple12)] @1: The mouse is cold.[(((triple6) -> rule1))]
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
triple1
The dog is cold.
("dog" "is" "cold" "+")
triple2
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple3
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple4
The mouse is blue.
("mouse" "is" "blue" "+")
triple5
The mouse is kind.
("mouse" "is" "kind" "+")
triple6
The mouse is rough.
("mouse" "is" "rough" "+")
triple7
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
triple8
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple9
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple10
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple11
The tiger is cold.
("tiger" "is" "cold" "+")
triple12
The mouse is cold.
("mouse" "is" "cold" "+")
((triple6) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1