The mouse is blue. The mouse is cold. The mouse is green. The mouse is red. The mouse is young. The mouse likes the tiger. The mouse sees the tiger. The mouse visits the tiger. The tiger is not blue. The tiger is cold. The tiger is green. The tiger is red. The tiger is young. The tiger likes the mouse. The tiger sees the mouse. The tiger does not visit the mouse. If the tiger visits the mouse and the tiger does not see the mouse then the tiger likes the mouse. If something is blue and young then it does not like the mouse. If something sees the mouse then it does not visit the mouse. If something visits the mouse and it sees the mouse then the mouse sees the tiger. Cold things are young. If something visits the mouse and the mouse likes the tiger then it does not like the tiger. If something sees the tiger and it is cold then the tiger is not blue. If something sees the tiger and it is not blue then it is green.
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger is not blue.
("tiger" "is" "blue" "-")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
The tiger does not visit the mouse.
("tiger" "visits" "mouse" "-")
If the tiger visits the mouse and the tiger does not see the mouse then the tiger likes the mouse.
((("tiger" "visits" "mouse" "+") ("tiger" "sees" "mouse" "~")) -> ("tiger" "likes" "mouse" "+"))
If something is blue and young then it does not like the mouse.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "likes" "mouse" "-"))
If something sees the mouse then it does not visit the mouse.
((("something" "sees" "mouse" "+")) -> ("something" "visits" "mouse" "-"))
If something visits the mouse and it sees the mouse then the mouse sees the tiger.
((("something" "visits" "mouse" "+") ("something" "sees" "mouse" "+")) -> ("mouse" "sees" "tiger" "+"))
Cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If something visits the mouse and the mouse likes the tiger then it does not like the tiger.
((("something" "visits" "mouse" "+") ("mouse" "likes" "tiger" "+")) -> ("something" "likes" "tiger" "-"))
If something sees the tiger and it is cold then the tiger is not blue.
((("something" "sees" "tiger" "+") ("something" "is" "cold" "+")) -> ("tiger" "is" "blue" "-"))
If something sees the tiger and it is not blue then it is green.
((("something" "sees" "tiger" "+") ("something" "is" "blue" "~")) -> ("something" "is" "green" "+"))
The tiger likes the mouse.
True
1
proof
[(triple14)]
("tiger" "likes" "mouse" "+")
triple14
The tiger visits the mouse.
False
1
inv-proof
[(triple16 OR ((triple15) -> rule3))]
("tiger" "visits" "mouse" "+")
triple16
((triple15) -> (rule3 % int1))
The tiger does not visit the mouse.
("tiger" "visits" "mouse" "-")
int1
The mouse does not like the mouse.
True
3
proof
[(((triple1 triple5) -> rule2) OR ((triple1 ((triple2) -> rule5)) -> rule2))]
("mouse" "likes" "mouse" "-")
((triple1 triple5) -> (rule2 % int1))
The mouse does not like the mouse.
("mouse" "likes" "mouse" "-")
int1
((triple1 ((triple2) -> (rule5 % int2))) -> (rule2 % int1))
The mouse does not like the mouse.
("mouse" "likes" "mouse" "-")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse likes the mouse.
False
3
inv-proof
[(((triple1 triple5) -> rule2) OR ((triple1 ((triple2) -> rule5)) -> rule2))]
("mouse" "likes" "mouse" "+")
((triple1 triple5) -> (rule2 % int1))
The mouse does not like the mouse.
("mouse" "likes" "mouse" "-")
int1
((triple1 ((triple2) -> (rule5 % int2))) -> (rule2 % int1))
The mouse does not like the mouse.
("mouse" "likes" "mouse" "-")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The mouse is blue.[(triple1)] The mouse is cold.[(triple2)] The mouse is green.[(triple3)] The mouse is red.[(triple4)] The mouse is young.[(triple5 OR ((triple2) -> rule5))] The mouse likes the tiger.[(triple6)] The mouse sees the tiger.[(triple7)] The mouse visits the tiger.[(triple8)] The tiger does not visit the mouse.[(triple16 OR ((triple15) -> rule3))] The tiger is cold.[(triple10)] The tiger is green.[(triple11)] The tiger is not blue.[(triple9 OR ((triple7 triple2) -> rule7))] The tiger is red.[(triple12)] The tiger is young.[(triple13 OR ((triple10) -> rule5))] The tiger likes the mouse.[(triple14)] The tiger sees the mouse.[(triple15)] @1: The mouse does not like the mouse.[(((triple1 triple5) -> rule2) OR ((triple1 ((triple2) -> rule5)) -> rule2))]
The mouse is blue.
("mouse" "is" "blue" "+")
triple1
The mouse is cold.
("mouse" "is" "cold" "+")
triple2
The mouse is green.
("mouse" "is" "green" "+")
triple3
The mouse is red.
("mouse" "is" "red" "+")
triple4
The mouse is young.
("mouse" "is" "young" "+")
triple5
((triple2) -> (rule5 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple6
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple7
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple8
The tiger does not visit the mouse.
("tiger" "visits" "mouse" "-")
triple16
((triple15) -> (rule3 % int1))
The tiger does not visit the mouse.
("tiger" "visits" "mouse" "-")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
triple10
The tiger is green.
("tiger" "is" "green" "+")
triple11
The tiger is not blue.
("tiger" "is" "blue" "-")
triple9
((triple7 triple2) -> (rule7 % int1))
The tiger is not blue.
("tiger" "is" "blue" "-")
int1
The tiger is red.
("tiger" "is" "red" "+")
triple12
The tiger is young.
("tiger" "is" "young" "+")
triple13
((triple10) -> (rule5 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple14
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple15
The mouse does not like the mouse.
("mouse" "likes" "mouse" "-")
((triple1 triple5) -> (rule2 % int1))
The mouse does not like the mouse.
("mouse" "likes" "mouse" "-")
int1
((triple1 ((triple2) -> (rule5 % int2))) -> (rule2 % int1))
The mouse does not like the mouse.
("mouse" "likes" "mouse" "-")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2