The mouse chases the tiger. The mouse is young. The mouse does not like the squirrel. The squirrel chases the tiger. The squirrel is red. The tiger chases the squirrel. The tiger is round. If the mouse is not round then the mouse likes the squirrel. If something is red then it is not kind.
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse does not like the squirrel.
("mouse" "likes" "squirrel" "-")
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger is round.
("tiger" "is" "round" "+")
If the mouse is not round then the mouse likes the squirrel.
((("mouse" "is" "round" "~")) -> ("mouse" "likes" "squirrel" "+"))
If something is red then it is not kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "-"))
The squirrel chases the tiger.
True
1
proof
[(triple4)]
("squirrel" "chases" "tiger" "+")
triple4
The mouse likes the squirrel.
False
1
inv-proof
[(triple3)]
("mouse" "likes" "squirrel" "+")
triple3
The squirrel is not kind.
True
2
proof
[(((triple5) -> rule2))]
("squirrel" "is" "kind" "-")
((triple5) -> (rule2 % int1))
The squirrel is not kind.
("squirrel" "is" "kind" "-")
int1
The squirrel is kind.
False
2
inv-proof
[(((triple5) -> rule2))]
("squirrel" "is" "kind" "+")
((triple5) -> (rule2 % int1))
The squirrel is not kind.
("squirrel" "is" "kind" "-")
int1
The tiger is not kind.
Unknown
inv-random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "-")
The mouse chases the squirrel.
Unknown
random
[@0: The mouse chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "squirrel" "+")
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "-")
The tiger sees the mouse.
Unknown
random
[@0: The tiger sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "mouse" "+")
@0: The mouse chases the tiger.[(triple1)] The mouse does not like the squirrel.[(triple3)] The mouse is young.[(triple2)] The squirrel chases the tiger.[(triple4)] The squirrel is red.[(triple5)] The tiger chases the squirrel.[(triple6)] The tiger is round.[(triple7)] @1: The squirrel is not kind.[(((triple5) -> rule2))]
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple1
The mouse does not like the squirrel.
("mouse" "likes" "squirrel" "-")
triple3
The mouse is young.
("mouse" "is" "young" "+")
triple2
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple4
The squirrel is red.
("squirrel" "is" "red" "+")
triple5
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple6
The tiger is round.
("tiger" "is" "round" "+")
triple7
The squirrel is not kind.
("squirrel" "is" "kind" "-")
((triple5) -> (rule2 % int1))
The squirrel is not kind.
("squirrel" "is" "kind" "-")
int1