The cat is nice. The cat likes the rabbit. The cat visits the lion. The lion visits the tiger. The rabbit is kind. The rabbit likes the tiger. The tiger eats the cat. Nice people are kind. If someone likes the cat and they visit the lion then the lion visits the cat. If someone is round then they are nice. If someone is round then they eat the cat. If the tiger visits the cat and the cat visits the lion then the tiger eats the rabbit. If someone is kind then they visit the rabbit. If the cat is kind and the cat visits the lion then the lion is round.
The cat is nice.
("cat" "is" "nice" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
Nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If someone likes the cat and they visit the lion then the lion visits the cat.
((("someone" "likes" "cat" "+") ("someone" "visits" "lion" "+")) -> ("lion" "visits" "cat" "+"))
If someone is round then they are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
If someone is round then they eat the cat.
((("someone" "is" "round" "+")) -> ("someone" "eats" "cat" "+"))
If the tiger visits the cat and the cat visits the lion then the tiger eats the rabbit.
((("tiger" "visits" "cat" "+") ("cat" "visits" "lion" "+")) -> ("tiger" "eats" "rabbit" "+"))
If someone is kind then they visit the rabbit.
((("someone" "is" "kind" "+")) -> ("someone" "visits" "rabbit" "+"))
If the cat is kind and the cat visits the lion then the lion is round.
((("cat" "is" "kind" "+") ("cat" "visits" "lion" "+")) -> ("lion" "is" "round" "+"))
The tiger eats the cat.
True
1
proof
[(triple7)]
("tiger" "eats" "cat" "+")
triple7
The cat is not nice.
False
1
inv-proof
[(triple1)]
("cat" "is" "nice" "-")
triple1
The rabbit visits the rabbit.
True
2
proof
[(((triple5) -> rule6))]
("rabbit" "visits" "rabbit" "+")
((triple5) -> (rule6 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The cat is not kind.
False
2
inv-proof
[(((triple1) -> rule1))]
("cat" "is" "kind" "-")
((triple1) -> (rule1 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The lion is round.
True
4
proof
[(((((triple1) -> rule1) triple3) -> rule7))]
("lion" "is" "round" "+")
((((triple1) -> (rule1 % int2)) triple3) -> (rule7 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat does not visit the rabbit.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule6))]
("cat" "visits" "rabbit" "-")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The lion is nice.
True
5
proof
[(((((((triple1) -> rule1) triple3) -> rule7)) -> rule3))]
("lion" "is" "nice" "+")
((((((triple1) -> (rule1 % int3)) triple3) -> (rule7 % int2))) -> (rule3 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3
The lion is not nice.
False
5
inv-proof
[(((((((triple1) -> rule1) triple3) -> rule7)) -> rule3))]
("lion" "is" "nice" "-")
((((((triple1) -> (rule1 % int3)) triple3) -> (rule7 % int2))) -> (rule3 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3
The lion is kind.
True
6
proof
[(((((((((triple1) -> rule1) triple3) -> rule7)) -> rule3)) -> rule1))]
("lion" "is" "kind" "+")
((((((((triple1) -> (rule1 % int4)) triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion is round.
("lion" "is" "round" "+")
int3
The cat is kind.
("cat" "is" "kind" "+")
int4
The lion is not kind.
False
6
inv-proof
[(((((((((triple1) -> rule1) triple3) -> rule7)) -> rule3)) -> rule1))]
("lion" "is" "kind" "-")
((((((((triple1) -> (rule1 % int4)) triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion is round.
("lion" "is" "round" "+")
int3
The cat is kind.
("cat" "is" "kind" "+")
int4
The lion visits the rabbit.
True
7
proof
[(((((((((((triple1) -> rule1) triple3) -> rule7)) -> rule3)) -> rule1)) -> rule6))]
("lion" "visits" "rabbit" "+")
((((((((((triple1) -> (rule1 % int5)) triple3) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3
The lion is round.
("lion" "is" "round" "+")
int4
The cat is kind.
("cat" "is" "kind" "+")
int5
The lion does not visit the rabbit.
False
7
inv-proof
[(((((((((((triple1) -> rule1) triple3) -> rule7)) -> rule3)) -> rule1)) -> rule6))]
("lion" "visits" "rabbit" "-")
((((((((((triple1) -> (rule1 % int5)) triple3) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3
The lion is round.
("lion" "is" "round" "+")
int4
The cat is kind.
("cat" "is" "kind" "+")
int5
The cat does not eat the cat.
Unknown
inv-rconc
[@1: The cat eats the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "eats" "cat" "-")
The tiger is kind.
Unknown
rconc
[@2: The tiger is kind.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("tiger" "is" "kind" "+")
The tiger does not visit the rabbit.
Unknown
inv-rconc
[@3: The tiger visits the rabbit.[CWA. Example of deepest failure = (rule6 <- rule1 <- rule3 <- FAIL)]]
("tiger" "visits" "rabbit" "-")
The rabbit is nice.
Unknown
rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "nice" "+")
The tiger is not nice.
Unknown
inv-rconc
[@1: The tiger is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "nice" "-")
The lion visits the cat.
Unknown
rconc
[@1: The lion visits the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "visits" "cat" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cat eats the lion.
Unknown
random
[@0: The cat eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "lion" "+")
The tiger is not green.
Unknown
inv-random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "-")
The cat visits the tiger.
Unknown
random
[@0: The cat visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "tiger" "+")
The rabbit does not eat the tiger.
Unknown
inv-random
[@0: The rabbit eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "tiger" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
@0: The cat is nice.[(triple1)] The cat likes the rabbit.[(triple2)] The cat visits the lion.[(triple3)] The lion visits the tiger.[(triple4)] The rabbit is kind.[(triple5)] The rabbit likes the tiger.[(triple6)] The tiger eats the cat.[(triple7)] @1: The cat is kind.[(((triple1) -> rule1))] The rabbit visits the rabbit.[(((triple5) -> rule6))] @2: The cat visits the rabbit.[(((((triple1) -> rule1)) -> rule6))] The lion is round.[(((((triple1) -> rule1) triple3) -> rule7))] @3: The lion eats the cat.[(((((((triple1) -> rule1) triple3) -> rule7)) -> rule4))] The lion is nice.[(((((((triple1) -> rule1) triple3) -> rule7)) -> rule3))] @4: The lion is kind.[(((((((((triple1) -> rule1) triple3) -> rule7)) -> rule3)) -> rule1))] @5: The lion visits the rabbit.[(((((((((((triple1) -> rule1) triple3) -> rule7)) -> rule3)) -> rule1)) -> rule6))]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple2
The cat visits the lion.
("cat" "visits" "lion" "+")
triple3
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple4
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple5
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple6
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple7
The cat is kind.
("cat" "is" "kind" "+")
((triple1) -> (rule1 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple5) -> (rule6 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The lion is round.
("lion" "is" "round" "+")
((((triple1) -> (rule1 % int2)) triple3) -> (rule7 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The lion eats the cat.
("lion" "eats" "cat" "+")
((((((triple1) -> (rule1 % int3)) triple3) -> (rule7 % int2))) -> (rule4 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3
The lion is nice.
("lion" "is" "nice" "+")
((((((triple1) -> (rule1 % int3)) triple3) -> (rule7 % int2))) -> (rule3 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3
The lion is kind.
("lion" "is" "kind" "+")
((((((((triple1) -> (rule1 % int4)) triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion is round.
("lion" "is" "round" "+")
int3
The cat is kind.
("cat" "is" "kind" "+")
int4
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
((((((((((triple1) -> (rule1 % int5)) triple3) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
int3
The lion is round.
("lion" "is" "round" "+")
int4
The cat is kind.
("cat" "is" "kind" "+")
int5