The mouse is blue. The mouse is cold. The mouse is nice. The mouse is young. The mouse likes the tiger. The mouse needs the tiger. The mouse visits the tiger. The tiger is blue. The tiger is cold. The tiger is young. The tiger needs the mouse. The tiger visits the mouse. If the tiger needs the mouse and the mouse visits the tiger then the mouse needs the tiger. If something needs the mouse then it visits the tiger. If something needs the tiger and it visits the mouse then the mouse is nice. Nice things are red. If something likes the tiger then the tiger is nice. If something is red then it is nice. If something visits the mouse and it likes the mouse then it needs the mouse. If something visits the mouse then it is blue.
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If the tiger needs the mouse and the mouse visits the tiger then the mouse needs the tiger.
((("tiger" "needs" "mouse" "+") ("mouse" "visits" "tiger" "+")) -> ("mouse" "needs" "tiger" "+"))
If something needs the mouse then it visits the tiger.
((("something" "needs" "mouse" "+")) -> ("something" "visits" "tiger" "+"))
If something needs the tiger and it visits the mouse then the mouse is nice.
((("something" "needs" "tiger" "+") ("something" "visits" "mouse" "+")) -> ("mouse" "is" "nice" "+"))
Nice things are red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If something likes the tiger then the tiger is nice.
((("something" "likes" "tiger" "+")) -> ("tiger" "is" "nice" "+"))
If something is red then it is nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
If something visits the mouse and it likes the mouse then it needs the mouse.
((("something" "visits" "mouse" "+") ("something" "likes" "mouse" "+")) -> ("something" "needs" "mouse" "+"))
If something visits the mouse then it is blue.
((("something" "visits" "mouse" "+")) -> ("something" "is" "blue" "+"))
The tiger is cold.
True
1
proof
[(triple9)]
("tiger" "is" "cold" "+")
triple9
The tiger is not cold.
False
1
inv-proof
[(triple9)]
("tiger" "is" "cold" "-")
triple9
The mouse is red.
True
2
proof
[(((triple3) -> rule4))]
("mouse" "is" "red" "+")
((triple3) -> (rule4 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The tiger does not visit the tiger.
False
2
inv-proof
[(((triple11) -> rule2))]
("tiger" "visits" "tiger" "-")
((triple11) -> (rule2 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is red.
True
3
proof
[(((((triple5) -> rule5)) -> rule4))]
("tiger" "is" "red" "+")
((((triple5) -> (rule5 % int2))) -> (rule4 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger is not red.
False
3
inv-proof
[(((((triple5) -> rule5)) -> rule4))]
("tiger" "is" "red" "-")
((((triple5) -> (rule5 % int2))) -> (rule4 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The mouse does not need the mouse.
Unknown
inv-rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "needs" "mouse" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The tiger likes the mouse.
Unknown
random
[@0: The tiger likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "mouse" "+")
@0: The mouse is blue.[(triple1)] The mouse is cold.[(triple2)] The mouse is nice.[(triple3)] The mouse is young.[(triple4)] The mouse likes the tiger.[(triple5)] The mouse needs the tiger.[(triple6 OR ((triple11 triple7) -> rule1))] The mouse visits the tiger.[(triple7)] The tiger is blue.[(triple8 OR ((triple12) -> rule8))] The tiger is cold.[(triple9)] The tiger is young.[(triple10)] The tiger needs the mouse.[(triple11)] The tiger visits the mouse.[(triple12)] @1: The mouse is red.[(((triple3) -> rule4))] The tiger is nice.[(((triple5) -> rule5))] The tiger visits the tiger.[(((triple11) -> rule2))] @2: The tiger is red.[(((((triple5) -> rule5)) -> rule4))]
The mouse is blue.
("mouse" "is" "blue" "+")
triple1
The mouse is cold.
("mouse" "is" "cold" "+")
triple2
The mouse is nice.
("mouse" "is" "nice" "+")
triple3
The mouse is young.
("mouse" "is" "young" "+")
triple4
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple5
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple6
((triple11 triple7) -> (rule1 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple7
The tiger is blue.
("tiger" "is" "blue" "+")
triple8
((triple12) -> (rule8 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
triple9
The tiger is young.
("tiger" "is" "young" "+")
triple10
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple11
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple12
The mouse is red.
("mouse" "is" "red" "+")
((triple3) -> (rule4 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
((triple5) -> (rule5 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple11) -> (rule2 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
((((triple5) -> (rule5 % int2))) -> (rule4 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2