The cat is young. The cat needs the tiger. The cat sees the mouse. The cat sees the tiger. The cat visits the mouse. The cat visits the tiger. The mouse is blue. The mouse is young. The mouse sees the cat. The mouse visits the cat. The mouse visits the tiger. The tiger is cold. The tiger is kind. The tiger needs the cat. The tiger sees the cat. If something needs the mouse and the mouse is cold then it sees the mouse. If something needs the tiger and it sees the mouse then the mouse needs the tiger.
The cat is young.
("cat" "is" "young" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If something needs the mouse and the mouse is cold then it sees the mouse.
((("something" "needs" "mouse" "+") ("mouse" "is" "cold" "+")) -> ("something" "sees" "mouse" "+"))
If something needs the tiger and it sees the mouse then the mouse needs the tiger.
((("something" "needs" "tiger" "+") ("something" "sees" "mouse" "+")) -> ("mouse" "needs" "tiger" "+"))
The tiger sees the cat.
True
1
proof
[(triple15)]
("tiger" "sees" "cat" "+")
triple15
The cat does not visit the mouse.
False
1
inv-proof
[(triple5)]
("cat" "visits" "mouse" "-")
triple5
The mouse needs the tiger.
True
3
proof
[(((triple2 triple3) -> rule2))]
("mouse" "needs" "tiger" "+")
((triple2 triple3) -> (rule2 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The mouse does not need the tiger.
False
3
inv-proof
[(((triple2 triple3) -> rule2))]
("mouse" "needs" "tiger" "-")
((triple2 triple3) -> (rule2 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The tiger does not see the mouse.
Unknown
inv-rconc
[@1: The tiger sees the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "sees" "mouse" "-")
The mouse sees the mouse.
Unknown
rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "sees" "mouse" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
@0: The cat is young.[(triple1)] The cat needs the tiger.[(triple2)] The cat sees the mouse.[(triple3)] The cat sees the tiger.[(triple4)] The cat visits the mouse.[(triple5)] The cat visits the tiger.[(triple6)] The mouse is blue.[(triple7)] The mouse is young.[(triple8)] The mouse sees the cat.[(triple9)] The mouse visits the cat.[(triple10)] The mouse visits the tiger.[(triple11)] The tiger is cold.[(triple12)] The tiger is kind.[(triple13)] The tiger needs the cat.[(triple14)] The tiger sees the cat.[(triple15)] @1: The mouse needs the tiger.[(((triple2 triple3) -> rule2))]
The cat is young.
("cat" "is" "young" "+")
triple1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple2
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple3
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple4
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple5
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple6
The mouse is blue.
("mouse" "is" "blue" "+")
triple7
The mouse is young.
("mouse" "is" "young" "+")
triple8
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple9
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple10
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple11
The tiger is cold.
("tiger" "is" "cold" "+")
triple12
The tiger is kind.
("tiger" "is" "kind" "+")
triple13
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple14
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple15
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
((triple2 triple3) -> (rule2 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1