The dog is kind. The dog needs the mouse. The mouse chases the dog. The mouse is cold. The squirrel chases the tiger. The squirrel is cold. The squirrel needs the dog. The tiger chases the mouse. The tiger chases the squirrel. The tiger is blue. The tiger is kind. The tiger is not round. If someone sees the squirrel then they are kind. If someone is cold and they need the squirrel then they do not need the mouse. If the dog does not see the mouse and the dog does not see the tiger then the dog sees the squirrel. If someone chases the mouse then the mouse sees the squirrel. If the dog sees the tiger then the tiger is not young. If the mouse sees the dog and the mouse is not blue then the dog is round. If the squirrel chases the tiger and the tiger sees the dog then the squirrel is cold. If someone is kind and not cold then they are round.
The dog is kind.
("dog" "is" "kind" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is not round.
("tiger" "is" "round" "-")
If someone sees the squirrel then they are kind.
((("someone" "sees" "squirrel" "+")) -> ("someone" "is" "kind" "+"))
If someone is cold and they need the squirrel then they do not need the mouse.
((("someone" "is" "cold" "+") ("someone" "needs" "squirrel" "+")) -> ("someone" "needs" "mouse" "-"))
If the dog does not see the mouse and the dog does not see the tiger then the dog sees the squirrel.
((("dog" "sees" "mouse" "~") ("dog" "sees" "tiger" "~")) -> ("dog" "sees" "squirrel" "+"))
If someone chases the mouse then the mouse sees the squirrel.
((("someone" "chases" "mouse" "+")) -> ("mouse" "sees" "squirrel" "+"))
If the dog sees the tiger then the tiger is not young.
((("dog" "sees" "tiger" "+")) -> ("tiger" "is" "young" "-"))
If the mouse sees the dog and the mouse is not blue then the dog is round.
((("mouse" "sees" "dog" "+") ("mouse" "is" "blue" "~")) -> ("dog" "is" "round" "+"))
If the squirrel chases the tiger and the tiger sees the dog then the squirrel is cold.
((("squirrel" "chases" "tiger" "+") ("tiger" "sees" "dog" "+")) -> ("squirrel" "is" "cold" "+"))
If someone is kind and not cold then they are round.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "round" "+"))
The squirrel needs the dog.
True
1
proof
[(triple7)]
("squirrel" "needs" "dog" "+")
triple7
The tiger does not chase the mouse.
False
1
inv-proof
[(triple8)]
("tiger" "chases" "mouse" "-")
triple8
The mouse sees the squirrel.
True
2
proof
[(((triple8) -> rule4))]
("mouse" "sees" "squirrel" "+")
((triple8) -> (rule4 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The mouse does not see the squirrel.
False
2
inv-proof
[(((triple8) -> rule4))]
("mouse" "sees" "squirrel" "-")
((triple8) -> (rule4 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The mouse is kind.
True
3
proof
[(((((triple8) -> rule4)) -> rule1))]
("mouse" "is" "kind" "+")
((((triple8) -> (rule4 % int2))) -> (rule1 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The mouse is not kind.
False
3
inv-proof
[(((((triple8) -> rule4)) -> rule1))]
("mouse" "is" "kind" "-")
((((triple8) -> (rule4 % int2))) -> (rule1 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The dog is not round.
Unknown
inv-rconc
[@1: The dog is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "is" "round" "-")
The mouse is round.
Unknown
rconc
[@1: The mouse is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "is" "round" "+")
The squirrel is not round.
Unknown
inv-rconc
[@1: The squirrel is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "is" "round" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
The mouse does not see the tiger.
Unknown
inv-random
[@0: The mouse sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "tiger" "-")
The mouse needs the dog.
Unknown
random
[@0: The mouse needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "dog" "+")
@0: The dog is kind.[(triple1)] The dog needs the mouse.[(triple2)] The mouse chases the dog.[(triple3)] The mouse is cold.[(triple4)] The squirrel chases the tiger.[(triple5)] The squirrel is cold.[(triple6)] The squirrel needs the dog.[(triple7)] The tiger chases the mouse.[(triple8)] The tiger chases the squirrel.[(triple9)] The tiger is blue.[(triple10)] The tiger is kind.[(triple11)] The tiger is not round.[(triple12)] @1: The mouse sees the squirrel.[(((triple8) -> rule4))] @2: The mouse is kind.[(((((triple8) -> rule4)) -> rule1))]
The dog is kind.
("dog" "is" "kind" "+")
triple1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple2
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple3
The mouse is cold.
("mouse" "is" "cold" "+")
triple4
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple5
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple6
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
triple7
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple8
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple9
The tiger is blue.
("tiger" "is" "blue" "+")
triple10
The tiger is kind.
("tiger" "is" "kind" "+")
triple11
The tiger is not round.
("tiger" "is" "round" "-")
triple12
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
((triple8) -> (rule4 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
((((triple8) -> (rule4 % int2))) -> (rule1 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2