The lion is nice. The lion sees the squirrel. The rabbit is nice. The rabbit is round. The rabbit likes the squirrel. The squirrel is big. The squirrel likes the tiger. The tiger likes the rabbit. The tiger sees the squirrel. The tiger visits the lion. If something visits the lion and it visits the tiger then it sees the lion. If something is red then it visits the tiger. All kind things are red. If something visits the rabbit and it is big then the rabbit sees the squirrel. If something is round then it visits the squirrel. If something visits the tiger and the tiger is red then it is round. If the squirrel is nice then the squirrel likes the rabbit. If something sees the squirrel and the squirrel is big then it is red.
The lion is nice.
("lion" "is" "nice" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If something visits the lion and it visits the tiger then it sees the lion.
((("something" "visits" "lion" "+") ("something" "visits" "tiger" "+")) -> ("something" "sees" "lion" "+"))
If something is red then it visits the tiger.
((("something" "is" "red" "+")) -> ("something" "visits" "tiger" "+"))
All kind things are red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If something visits the rabbit and it is big then the rabbit sees the squirrel.
((("something" "visits" "rabbit" "+") ("something" "is" "big" "+")) -> ("rabbit" "sees" "squirrel" "+"))
If something is round then it visits the squirrel.
((("something" "is" "round" "+")) -> ("something" "visits" "squirrel" "+"))
If something visits the tiger and the tiger is red then it is round.
((("something" "visits" "tiger" "+") ("tiger" "is" "red" "+")) -> ("something" "is" "round" "+"))
If the squirrel is nice then the squirrel likes the rabbit.
((("squirrel" "is" "nice" "+")) -> ("squirrel" "likes" "rabbit" "+"))
If something sees the squirrel and the squirrel is big then it is red.
((("something" "sees" "squirrel" "+") ("squirrel" "is" "big" "+")) -> ("something" "is" "red" "+"))
The tiger visits the lion.
True
1
proof
[(triple10)]
("tiger" "visits" "lion" "+")
triple10
The rabbit is not nice.
False
1
inv-proof
[(triple3)]
("rabbit" "is" "nice" "-")
triple3
The rabbit visits the squirrel.
True
2
proof
[(((triple4) -> rule5))]
("rabbit" "visits" "squirrel" "+")
((triple4) -> (rule5 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The rabbit does not visit the squirrel.
False
2
inv-proof
[(((triple4) -> rule5))]
("rabbit" "visits" "squirrel" "-")
((triple4) -> (rule5 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The lion visits the tiger.
True
4
proof
[(((((triple2 triple6) -> rule8)) -> rule2))]
("lion" "visits" "tiger" "+")
((((triple2 triple6) -> (rule8 % int2))) -> (rule2 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion does not visit the tiger.
False
4
inv-proof
[(((((triple2 triple6) -> rule8)) -> rule2))]
("lion" "visits" "tiger" "-")
((((triple2 triple6) -> (rule8 % int2))) -> (rule2 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The tiger sees the lion.
True
6
proof
[(((triple10 ((((triple9 triple6) -> rule8)) -> rule2)) -> rule1))]
("tiger" "sees" "lion" "+")
((triple10 ((((triple9 triple6) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
The tiger is not round.
False
8
inv-proof
[(((((((triple9 triple6) -> rule8)) -> rule2) ((triple9 triple6) -> rule8)) -> rule6))]
("tiger" "is" "round" "-")
((((((triple9 triple6) -> (rule8 % int3))) -> (rule2 % int2)) ((triple9 triple6) -> (rule8 % int3))) -> (rule6 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
The rabbit does not see the squirrel.
Unknown
inv-rconc
[@1: The rabbit sees the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "sees" "squirrel" "-")
The rabbit is red.
Unknown
rconc
[@2: The rabbit is red.[CWA. Example of deepest failure = (rule8 <- rule4 <- FAIL)]]
("rabbit" "is" "red" "+")
The squirrel does not visit the tiger.
Unknown
inv-rconc
[@2: The squirrel visits the tiger.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("squirrel" "visits" "tiger" "-")
The squirrel sees the lion.
Unknown
rconc
[@1: The squirrel sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "sees" "lion" "+")
The squirrel does not like the lion.
Unknown
inv-random
[@0: The squirrel likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "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 lion does not see the tiger.
Unknown
inv-random
[@0: The lion sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "tiger" "-")
The rabbit is big.
Unknown
random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "+")
@0: The lion is nice.[(triple1)] The lion sees the squirrel.[(triple2)] The rabbit is nice.[(triple3)] The rabbit is round.[(triple4)] The rabbit likes the squirrel.[(triple5)] The squirrel is big.[(triple6)] The squirrel likes the tiger.[(triple7)] The tiger likes the rabbit.[(triple8)] The tiger sees the squirrel.[(triple9)] The tiger visits the lion.[(triple10)] @1: The lion is red.[(((triple2 triple6) -> rule8))] The rabbit visits the squirrel.[(((triple4) -> rule5))] The tiger is red.[(((triple9 triple6) -> rule8))] @2: The lion visits the tiger.[(((((triple2 triple6) -> rule8)) -> rule2))] The tiger visits the tiger.[(((((triple9 triple6) -> rule8)) -> rule2))] @3: The lion is round.[(((((((triple2 triple6) -> rule8)) -> rule2) ((triple9 triple6) -> rule8)) -> rule6))] The tiger is round.[(((((((triple9 triple6) -> rule8)) -> rule2) ((triple9 triple6) -> rule8)) -> rule6))] The tiger sees the lion.[(((triple10 ((((triple9 triple6) -> rule8)) -> rule2)) -> rule1))] @4: The lion visits the squirrel.[(((((((((triple2 triple6) -> rule8)) -> rule2) ((triple9 triple6) -> rule8)) -> rule6)) -> rule5))] The tiger visits the squirrel.[(((((((((triple9 triple6) -> rule8)) -> rule2) ((triple9 triple6) -> rule8)) -> rule6)) -> rule5))]
The lion is nice.
("lion" "is" "nice" "+")
triple1
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple2
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple3
The rabbit is round.
("rabbit" "is" "round" "+")
triple4
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
triple5
The squirrel is big.
("squirrel" "is" "big" "+")
triple6
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
triple7
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple8
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple9
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple10
The lion is red.
("lion" "is" "red" "+")
((triple2 triple6) -> (rule8 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
((triple4) -> (rule5 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
((triple9 triple6) -> (rule8 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
((((triple2 triple6) -> (rule8 % int2))) -> (rule2 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((((triple9 triple6) -> (rule8 % int2))) -> (rule2 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The lion is round.
("lion" "is" "round" "+")
((((((triple2 triple6) -> (rule8 % int4))) -> (rule2 % int3)) ((triple9 triple6) -> (rule8 % int2))) -> (rule6 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
The tiger is round.
("tiger" "is" "round" "+")
((((((triple9 triple6) -> (rule8 % int3))) -> (rule2 % int2)) ((triple9 triple6) -> (rule8 % int3))) -> (rule6 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
The tiger sees the lion.
("tiger" "sees" "lion" "+")
((triple10 ((((triple9 triple6) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
((((((((triple2 triple6) -> (rule8 % int5))) -> (rule2 % int4)) ((triple9 triple6) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int4
The lion is red.
("lion" "is" "red" "+")
int5
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
((((((((triple9 triple6) -> (rule8 % int4))) -> (rule2 % int3)) ((triple9 triple6) -> (rule8 % int4))) -> (rule6 % int2))) -> (rule5 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int3
The tiger is red.
("tiger" "is" "red" "+")
int4