The mouse chases the tiger. The mouse is nice. The mouse needs the tiger. The mouse sees the tiger. The tiger chases the mouse. The tiger is blue. The tiger is cold. The tiger is green. The tiger is nice. The tiger is round. The tiger needs the mouse. The tiger sees the mouse. If something sees the mouse and it needs the tiger then the tiger sees the mouse. If something sees the mouse and the mouse sees the tiger then it chases the tiger. If something chases the tiger and it chases the mouse then the mouse is blue.
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If something sees the mouse and it needs the tiger then the tiger sees the mouse.
((("something" "sees" "mouse" "+") ("something" "needs" "tiger" "+")) -> ("tiger" "sees" "mouse" "+"))
If something sees the mouse and the mouse sees the tiger then it chases the tiger.
((("something" "sees" "mouse" "+") ("mouse" "sees" "tiger" "+")) -> ("something" "chases" "tiger" "+"))
If something chases the tiger and it chases the mouse then the mouse is blue.
((("something" "chases" "tiger" "+") ("something" "chases" "mouse" "+")) -> ("mouse" "is" "blue" "+"))
The tiger is cold.
True
1
proof
[(triple7)]
("tiger" "is" "cold" "+")
triple7
The tiger does not chase the mouse.
False
1
inv-proof
[(triple5)]
("tiger" "chases" "mouse" "-")
triple5
The tiger chases the tiger.
True
3
proof
[(((triple12 triple4) -> rule2))]
("tiger" "chases" "tiger" "+")
((triple12 triple4) -> (rule2 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger does not chase the tiger.
False
3
inv-proof
[(((triple12 triple4) -> rule2))]
("tiger" "chases" "tiger" "-")
((triple12 triple4) -> (rule2 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The mouse is blue.
True
5
proof
[(((((triple12 triple4) -> rule2) triple5) -> rule3))]
("mouse" "is" "blue" "+")
((((triple12 triple4) -> (rule2 % int2)) triple5) -> (rule3 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The mouse is not blue.
False
5
inv-proof
[(((((triple12 triple4) -> rule2) triple5) -> rule3))]
("mouse" "is" "blue" "-")
((((triple12 triple4) -> (rule2 % int2)) triple5) -> (rule3 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
The mouse is not green.
Unknown
inv-random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "-")
The mouse is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
The mouse is not cold.
Unknown
inv-random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The mouse chases the tiger.[(triple1)] The mouse is nice.[(triple2)] The mouse needs the tiger.[(triple3)] The mouse sees the tiger.[(triple4)] The tiger chases the mouse.[(triple5)] The tiger is blue.[(triple6)] The tiger is cold.[(triple7)] The tiger is green.[(triple8)] The tiger is nice.[(triple9)] The tiger is round.[(triple10)] The tiger needs the mouse.[(triple11)] The tiger sees the mouse.[(triple12)] @1: The tiger chases the tiger.[(((triple12 triple4) -> rule2))] @2: The mouse is blue.[(((((triple12 triple4) -> rule2) triple5) -> rule3))]
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple1
The mouse is nice.
("mouse" "is" "nice" "+")
triple2
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple3
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple4
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple5
The tiger is blue.
("tiger" "is" "blue" "+")
triple6
The tiger is cold.
("tiger" "is" "cold" "+")
triple7
The tiger is green.
("tiger" "is" "green" "+")
triple8
The tiger is nice.
("tiger" "is" "nice" "+")
triple9
The tiger is round.
("tiger" "is" "round" "+")
triple10
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple11
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple12
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((triple12 triple4) -> (rule2 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
((((triple12 triple4) -> (rule2 % int2)) triple5) -> (rule3 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2