The lion chases the mouse. The lion does not chase the tiger. The lion is red. The lion does not visit the tiger. The mouse chases the lion. The mouse is green. The mouse is round. The mouse is not young. The mouse sees the lion. The mouse visits the lion. The mouse visits the tiger. The tiger is red. The tiger is not round. The tiger sees the mouse. The tiger visits the lion. If someone chases the mouse and they are young then they see the tiger. If someone chases the lion then they visit the mouse. If someone is big and they chase the mouse then they visit the mouse. If someone sees the lion then they are not young. If someone is red and young then they chase the lion. If someone chases the lion then the lion is young. If someone chases the mouse and they are not young then the mouse does not chase the tiger. If someone visits the tiger and the tiger does not visit the mouse then they visit the lion.
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion does not chase the tiger.
("lion" "chases" "tiger" "-")
The lion is red.
("lion" "is" "red" "+")
The lion does not visit the tiger.
("lion" "visits" "tiger" "-")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse is not young.
("mouse" "is" "young" "-")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is not round.
("tiger" "is" "round" "-")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If someone chases the mouse and they are young then they see the tiger.
((("someone" "chases" "mouse" "+") ("someone" "is" "young" "+")) -> ("someone" "sees" "tiger" "+"))
If someone chases the lion then they visit the mouse.
((("someone" "chases" "lion" "+")) -> ("someone" "visits" "mouse" "+"))
If someone is big and they chase the mouse then they visit the mouse.
((("someone" "is" "big" "+") ("someone" "chases" "mouse" "+")) -> ("someone" "visits" "mouse" "+"))
If someone sees the lion then they are not young.
((("someone" "sees" "lion" "+")) -> ("someone" "is" "young" "-"))
If someone is red and young then they chase the lion.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "chases" "lion" "+"))
If someone chases the lion then the lion is young.
((("someone" "chases" "lion" "+")) -> ("lion" "is" "young" "+"))
If someone chases the mouse and they are not young then the mouse does not chase the tiger.
((("someone" "chases" "mouse" "+") ("someone" "is" "young" "~")) -> ("mouse" "chases" "tiger" "-"))
If someone visits the tiger and the tiger does not visit the mouse then they visit the lion.
((("someone" "visits" "tiger" "+") ("tiger" "visits" "mouse" "~")) -> ("someone" "visits" "lion" "+"))
The tiger sees the mouse.
True
1
proof
[(triple14)]
("tiger" "sees" "mouse" "+")
triple14
The lion chases the tiger.
False
1
inv-proof
[(triple2)]
("lion" "chases" "tiger" "+")
triple2
The lion is young.
True
2
proof
[(((triple5) -> rule6))]
("lion" "is" "young" "+")
((triple5) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is not young.
False
2
inv-proof
[(((triple5) -> rule6))]
("lion" "is" "young" "-")
((triple5) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion sees the tiger.
True
4
proof
[(((triple1 ((triple5) -> rule6)) -> rule1))]
("lion" "sees" "tiger" "+")
((triple1 ((triple5) -> (rule6 % int2))) -> (rule1 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion does not chase the lion.
False
4
inv-proof
[(((triple3 ((triple5) -> rule6)) -> rule5))]
("lion" "chases" "lion" "-")
((triple3 ((triple5) -> (rule6 % int2))) -> (rule5 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion visits the mouse.
True
5
proof
[(((((triple3 ((triple5) -> rule6)) -> rule5)) -> rule2))]
("lion" "visits" "mouse" "+")
((((triple3 ((triple5) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion does not visit the mouse.
False
5
inv-proof
[(((((triple3 ((triple5) -> rule6)) -> rule5)) -> rule2))]
("lion" "visits" "mouse" "-")
((((triple3 ((triple5) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The mouse does not see the tiger.
Unknown
inv-rconc
[@1: The mouse sees the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "sees" "tiger" "-")
The tiger chases the lion.
Unknown
rconc
[@1: The tiger chases the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "chases" "lion" "+")
The tiger does not see the tiger.
Unknown
inv-rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "sees" "tiger" "-")
The tiger visits the mouse.
Unknown
rconc
[@2: The tiger visits the mouse.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("tiger" "visits" "mouse" "+")
The lion is not big.
Unknown
inv-random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The lion chases the mouse.[(triple1)] The lion does not chase the tiger.[(triple2)] The lion does not visit the tiger.[(triple4)] The lion is red.[(triple3)] The mouse chases the lion.[(triple5)] The mouse is green.[(triple6)] The mouse is not young.[(triple8 OR ((triple9) -> rule4))] The mouse is round.[(triple7)] The mouse sees the lion.[(triple9)] The mouse visits the lion.[(triple10)] The mouse visits the tiger.[(triple11)] The tiger is not round.[(triple13)] The tiger is red.[(triple12)] The tiger sees the mouse.[(triple14)] The tiger visits the lion.[(triple15)] @1: The lion is young.[(((triple5) -> rule6))] The mouse visits the mouse.[(((triple5) -> rule2))] @2: The lion chases the lion.[(((triple3 ((triple5) -> rule6)) -> rule5))] The lion sees the tiger.[(((triple1 ((triple5) -> rule6)) -> rule1))] @3: The lion visits the mouse.[(((((triple3 ((triple5) -> rule6)) -> rule5)) -> rule2))]
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple1
The lion does not chase the tiger.
("lion" "chases" "tiger" "-")
triple2
The lion does not visit the tiger.
("lion" "visits" "tiger" "-")
triple4
The lion is red.
("lion" "is" "red" "+")
triple3
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple5
The mouse is green.
("mouse" "is" "green" "+")
triple6
The mouse is not young.
("mouse" "is" "young" "-")
triple8
((triple9) -> (rule4 % int1))
The mouse is not young.
("mouse" "is" "young" "-")
int1
The mouse is round.
("mouse" "is" "round" "+")
triple7
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple9
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple10
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple11
The tiger is not round.
("tiger" "is" "round" "-")
triple13
The tiger is red.
("tiger" "is" "red" "+")
triple12
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple14
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple15
The lion is young.
("lion" "is" "young" "+")
((triple5) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((triple5) -> (rule2 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
((triple3 ((triple5) -> (rule6 % int2))) -> (rule5 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
((triple1 ((triple5) -> (rule6 % int2))) -> (rule1 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion visits the mouse.
("lion" "visits" "mouse" "+")
((((triple3 ((triple5) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3