The lion chases the mouse. The lion is not blue. The lion is not nice. The lion does not visit the mouse. The mouse chases the rabbit. The mouse is not nice. The mouse is red. The mouse does not like the rabbit. The mouse visits the tiger. The rabbit chases the tiger. The rabbit is nice. The rabbit is not rough. The tiger chases the mouse. The tiger is blue. The tiger is nice. The tiger likes the mouse. If something chases the rabbit and it visits the rabbit then the rabbit visits the tiger. If something visits the tiger and the tiger is nice then it is blue. If something is red then it chases the mouse. If something is nice and it likes the rabbit then it chases the lion. If something is rough then it chases the lion. If something likes the rabbit and the rabbit visits the tiger then the tiger likes the lion. If something visits the rabbit and the rabbit likes the lion then the lion visits the tiger. If something chases the tiger and the tiger is nice then the tiger visits the mouse. If something is blue then it visits the rabbit.
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion is not blue.
("lion" "is" "blue" "-")
The lion is not nice.
("lion" "is" "nice" "-")
The lion does not visit the mouse.
("lion" "visits" "mouse" "-")
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse is not nice.
("mouse" "is" "nice" "-")
The mouse is red.
("mouse" "is" "red" "+")
The mouse does not like the rabbit.
("mouse" "likes" "rabbit" "-")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is not rough.
("rabbit" "is" "rough" "-")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
If something chases the rabbit and it visits the rabbit then the rabbit visits the tiger.
((("something" "chases" "rabbit" "+") ("something" "visits" "rabbit" "+")) -> ("rabbit" "visits" "tiger" "+"))
If something visits the tiger and the tiger is nice then it is blue.
((("something" "visits" "tiger" "+") ("tiger" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
If something is red then it chases the mouse.
((("something" "is" "red" "+")) -> ("something" "chases" "mouse" "+"))
If something is nice and it likes the rabbit then it chases the lion.
((("something" "is" "nice" "+") ("something" "likes" "rabbit" "+")) -> ("something" "chases" "lion" "+"))
If something is rough then it chases the lion.
((("something" "is" "rough" "+")) -> ("something" "chases" "lion" "+"))
If something likes the rabbit and the rabbit visits the tiger then the tiger likes the lion.
((("something" "likes" "rabbit" "+") ("rabbit" "visits" "tiger" "+")) -> ("tiger" "likes" "lion" "+"))
If something visits the rabbit and the rabbit likes the lion then the lion visits the tiger.
((("something" "visits" "rabbit" "+") ("rabbit" "likes" "lion" "+")) -> ("lion" "visits" "tiger" "+"))
If something chases the tiger and the tiger is nice then the tiger visits the mouse.
((("something" "chases" "tiger" "+") ("tiger" "is" "nice" "+")) -> ("tiger" "visits" "mouse" "+"))
If something is blue then it visits the rabbit.
((("something" "is" "blue" "+")) -> ("something" "visits" "rabbit" "+"))
The lion does not visit the mouse.
True
1
proof
[(triple4)]
("lion" "visits" "mouse" "-")
triple4
The lion visits the mouse.
False
1
inv-proof
[(triple4)]
("lion" "visits" "mouse" "+")
triple4
The tiger visits the rabbit.
True
2
proof
[(((triple14) -> rule9))]
("tiger" "visits" "rabbit" "+")
((triple14) -> (rule9 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The tiger does not visit the rabbit.
False
2
inv-proof
[(((triple14) -> rule9))]
("tiger" "visits" "rabbit" "-")
((triple14) -> (rule9 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The mouse visits the rabbit.
True
4
proof
[(((((triple9 triple15) -> rule2)) -> rule9))]
("mouse" "visits" "rabbit" "+")
((((triple9 triple15) -> (rule2 % int2))) -> (rule9 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse does not visit the rabbit.
False
4
inv-proof
[(((((triple9 triple15) -> rule2)) -> rule9))]
("mouse" "visits" "rabbit" "-")
((((triple9 triple15) -> (rule2 % int2))) -> (rule9 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The rabbit visits the tiger.
True
6
proof
[(((triple5 ((((triple9 triple15) -> rule2)) -> rule9)) -> rule1))]
("rabbit" "visits" "tiger" "+")
((triple5 ((((triple9 triple15) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The rabbit does not visit the tiger.
False
6
inv-proof
[(((triple5 ((((triple9 triple15) -> rule2)) -> rule9)) -> rule1))]
("rabbit" "visits" "tiger" "-")
((triple5 ((((triple9 triple15) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The rabbit is blue.
True
8
proof
[(((((triple5 ((((triple9 triple15) -> rule2)) -> rule9)) -> rule1) triple15) -> rule2))]
("rabbit" "is" "blue" "+")
((((triple5 ((((triple9 triple15) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule1 % int2)) triple15) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int3
The mouse is blue.
("mouse" "is" "blue" "+")
int4
The rabbit is not blue.
False
8
inv-proof
[(((((triple5 ((((triple9 triple15) -> rule2)) -> rule9)) -> rule1) triple15) -> rule2))]
("rabbit" "is" "blue" "-")
((((triple5 ((((triple9 triple15) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule1 % int2)) triple15) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int3
The mouse is blue.
("mouse" "is" "blue" "+")
int4
The rabbit visits the rabbit.
True
9
proof
[(((((((triple5 ((((triple9 triple15) -> rule2)) -> rule9)) -> rule1) triple15) -> rule2)) -> rule9))]
("rabbit" "visits" "rabbit" "+")
((((((triple5 ((((triple9 triple15) -> (rule2 % int5))) -> (rule9 % int4))) -> (rule1 % int3)) triple15) -> (rule2 % int2))) -> (rule9 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int3
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int4
The mouse is blue.
("mouse" "is" "blue" "+")
int5
The rabbit does not visit the rabbit.
False
9
inv-proof
[(((((((triple5 ((((triple9 triple15) -> rule2)) -> rule9)) -> rule1) triple15) -> rule2)) -> rule9))]
("rabbit" "visits" "rabbit" "-")
((((((triple5 ((((triple9 triple15) -> (rule2 % int5))) -> (rule9 % int4))) -> (rule1 % int3)) triple15) -> (rule2 % int2))) -> (rule9 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int3
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int4
The mouse is blue.
("mouse" "is" "blue" "+")
int5
The mouse does not chase the lion.
Unknown
inv-rconc
[@1: The mouse chases the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "chases" "lion" "-")
The lion visits the rabbit.
Unknown
rconc
[@1: The lion visits the rabbit.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("lion" "visits" "rabbit" "+")
The lion does not chase the lion.
Unknown
inv-rconc
[@1: The lion chases the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "chases" "lion" "-")
The tiger chases the lion.
Unknown
rconc
[@1: The tiger chases the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "chases" "lion" "+")
The tiger does not like the lion.
Unknown
inv-rconc
[@1: The tiger likes the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "likes" "lion" "-")
The rabbit chases the lion.
Unknown
rconc
[@1: The rabbit chases the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "chases" "lion" "+")
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
The mouse does not like the lion.
Unknown
inv-random
[@0: The mouse likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "lion" "-")
The lion likes the rabbit.
Unknown
random
[@0: The lion likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "rabbit" "+")
The tiger does not visit the lion.
Unknown
inv-random
[@0: The tiger visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "lion" "-")
The lion chases the tiger.
Unknown
random
[@0: The lion chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "tiger" "+")
@0: The lion chases the mouse.[(triple1)] The lion does not visit the mouse.[(triple4)] The lion is not blue.[(triple2)] The lion is not nice.[(triple3)] The mouse chases the rabbit.[(triple5)] The mouse does not like the rabbit.[(triple8)] The mouse is not nice.[(triple6)] The mouse is red.[(triple7)] The mouse visits the tiger.[(triple9)] The rabbit chases the tiger.[(triple10)] The rabbit is nice.[(triple11)] The rabbit is not rough.[(triple12)] The tiger chases the mouse.[(triple13)] The tiger is blue.[(triple14)] The tiger is nice.[(triple15)] The tiger likes the mouse.[(triple16)] @1: The mouse chases the mouse.[(((triple7) -> rule3))] The mouse is blue.[(((triple9 triple15) -> rule2))] The tiger visits the mouse.[(((triple10 triple15) -> rule8))] The tiger visits the rabbit.[(((triple14) -> rule9))] @2: The mouse visits the rabbit.[(((((triple9 triple15) -> rule2)) -> rule9))] @3: The rabbit visits the tiger.[(((triple5 ((((triple9 triple15) -> rule2)) -> rule9)) -> rule1))] @4: The rabbit is blue.[(((((triple5 ((((triple9 triple15) -> rule2)) -> rule9)) -> rule1) triple15) -> rule2))] @5: The rabbit visits the rabbit.[(((((((triple5 ((((triple9 triple15) -> rule2)) -> rule9)) -> rule1) triple15) -> rule2)) -> rule9))]
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple1
The lion does not visit the mouse.
("lion" "visits" "mouse" "-")
triple4
The lion is not blue.
("lion" "is" "blue" "-")
triple2
The lion is not nice.
("lion" "is" "nice" "-")
triple3
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple5
The mouse does not like the rabbit.
("mouse" "likes" "rabbit" "-")
triple8
The mouse is not nice.
("mouse" "is" "nice" "-")
triple6
The mouse is red.
("mouse" "is" "red" "+")
triple7
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple9
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple10
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple11
The rabbit is not rough.
("rabbit" "is" "rough" "-")
triple12
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple13
The tiger is blue.
("tiger" "is" "blue" "+")
triple14
The tiger is nice.
("tiger" "is" "nice" "+")
triple15
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple16
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((triple7) -> (rule3 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
((triple9 triple15) -> (rule2 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
((triple10 triple15) -> (rule8 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
((triple14) -> (rule9 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
((((triple9 triple15) -> (rule2 % int2))) -> (rule9 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
((triple5 ((((triple9 triple15) -> (rule2 % int3))) -> (rule9 % int2))) -> (rule1 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The rabbit is blue.
("rabbit" "is" "blue" "+")
((((triple5 ((((triple9 triple15) -> (rule2 % int4))) -> (rule9 % int3))) -> (rule1 % int2)) triple15) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int3
The mouse is blue.
("mouse" "is" "blue" "+")
int4
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((((((triple5 ((((triple9 triple15) -> (rule2 % int5))) -> (rule9 % int4))) -> (rule1 % int3)) triple15) -> (rule2 % int2))) -> (rule9 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int3
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int4
The mouse is blue.
("mouse" "is" "blue" "+")
int5