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