The bear sees the tiger. The bear visits the lion. The cat sees the lion. The lion is round. The lion likes the tiger. The lion visits the bear. The lion visits the tiger. The tiger is nice. The tiger likes the bear. The tiger likes the lion. The tiger visits the lion. If someone is rough then they see the cat. If someone likes the lion and they like the tiger then the lion sees the tiger. If someone is kind and they see the cat then the cat is nice. If someone is round and rough then they visit the cat. If someone visits the lion and they like the tiger then the lion is rough. If someone visits the cat then they see the tiger. If someone visits the tiger and the tiger likes the lion then they are kind. If someone is nice then they like the tiger. If someone is nice and they see the lion then the lion visits the tiger.
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The bear visits the lion.
("bear" "visits" "lion" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The lion is round.
("lion" "is" "round" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger likes the bear.
("tiger" "likes" "bear" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If someone is rough then they see the cat.
((("someone" "is" "rough" "+")) -> ("someone" "sees" "cat" "+"))
If someone likes the lion and they like the tiger then the lion sees the tiger.
((("someone" "likes" "lion" "+") ("someone" "likes" "tiger" "+")) -> ("lion" "sees" "tiger" "+"))
If someone is kind and they see the cat then the cat is nice.
((("someone" "is" "kind" "+") ("someone" "sees" "cat" "+")) -> ("cat" "is" "nice" "+"))
If someone is round and rough then they visit the cat.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "visits" "cat" "+"))
If someone visits the lion and they like the tiger then the lion is rough.
((("someone" "visits" "lion" "+") ("someone" "likes" "tiger" "+")) -> ("lion" "is" "rough" "+"))
If someone visits the cat then they see the tiger.
((("someone" "visits" "cat" "+")) -> ("someone" "sees" "tiger" "+"))
If someone visits the tiger and the tiger likes the lion then they are kind.
((("someone" "visits" "tiger" "+") ("tiger" "likes" "lion" "+")) -> ("someone" "is" "kind" "+"))
If someone is nice then they like the tiger.
((("someone" "is" "nice" "+")) -> ("someone" "likes" "tiger" "+"))
If someone is nice and they see the lion then the lion visits the tiger.
((("someone" "is" "nice" "+") ("someone" "sees" "lion" "+")) -> ("lion" "visits" "tiger" "+"))
The tiger is nice.
True
1
proof
[(triple8)]
("tiger" "is" "nice" "+")
triple8
The cat does not see the lion.
False
1
inv-proof
[(triple3)]
("cat" "sees" "lion" "-")
triple3
The lion is kind.
True
3
proof
[(((triple7 triple10) -> rule7))]
("lion" "is" "kind" "+")
((triple7 triple10) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is not kind.
False
3
inv-proof
[(((triple7 triple10) -> rule7))]
("lion" "is" "kind" "-")
((triple7 triple10) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is rough.
True
4
proof
[(((triple11 ((triple8) -> rule8)) -> rule5))]
("lion" "is" "rough" "+")
((triple11 ((triple8) -> (rule8 % int2))) -> (rule5 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The lion does not see the tiger.
False
4
inv-proof
[(((triple10 ((triple8) -> rule8)) -> rule2) OR ((((triple4 ((triple11 ((triple8) -> rule8)) -> rule5)) -> rule4)) -> rule6))]
("lion" "sees" "tiger" "-")
((triple10 ((triple8) -> (rule8 % int2))) -> (rule2 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
((((triple4 ((triple11 ((triple8) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int4
The lion sees the cat.
True
5
proof
[(((((triple11 ((triple8) -> rule8)) -> rule5)) -> rule1))]
("lion" "sees" "cat" "+")
((((triple11 ((triple8) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The lion does not visit the cat.
False
6
inv-proof
[(((triple4 ((triple11 ((triple8) -> rule8)) -> rule5)) -> rule4))]
("lion" "visits" "cat" "-")
((triple4 ((triple11 ((triple8) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The cat is nice.
True
9
proof
[(((((triple7 triple10) -> rule7) ((((triple11 ((triple8) -> rule8)) -> rule5)) -> rule1)) -> rule3))]
("cat" "is" "nice" "+")
((((triple7 triple10) -> (rule7 % int5)) ((((triple11 ((triple8) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int4
The lion is kind.
("lion" "is" "kind" "+")
int5
The cat is not nice.
False
9
inv-proof
[(((((triple7 triple10) -> rule7) ((((triple11 ((triple8) -> rule8)) -> rule5)) -> rule1)) -> rule3))]
("cat" "is" "nice" "-")
((((triple7 triple10) -> (rule7 % int5)) ((((triple11 ((triple8) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int4
The lion is kind.
("lion" "is" "kind" "+")
int5
The cat likes the tiger.
True
10
proof
[(((((((triple7 triple10) -> rule7) ((((triple11 ((triple8) -> rule8)) -> rule5)) -> rule1)) -> rule3)) -> rule8))]
("cat" "likes" "tiger" "+")
((((((triple7 triple10) -> (rule7 % int6)) ((((triple11 ((triple8) -> (rule8 % int5))) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
int3
The lion is rough.
("lion" "is" "rough" "+")
int4
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int5
The lion is kind.
("lion" "is" "kind" "+")
int6
The cat does not like the tiger.
False
10
inv-proof
[(((((((triple7 triple10) -> rule7) ((((triple11 ((triple8) -> rule8)) -> rule5)) -> rule1)) -> rule3)) -> rule8))]
("cat" "likes" "tiger" "-")
((((((triple7 triple10) -> (rule7 % int6)) ((((triple11 ((triple8) -> (rule8 % int5))) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
int3
The lion is rough.
("lion" "is" "rough" "+")
int4
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int5
The lion is kind.
("lion" "is" "kind" "+")
int6
The bear does not see the cat.
Unknown
inv-rconc
[@1: The bear sees the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "sees" "cat" "-")
The cat sees the cat.
Unknown
rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "sees" "cat" "+")
The cat does not visit the cat.
Unknown
inv-rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "visits" "cat" "-")
The tiger sees the tiger.
Unknown
rconc
[@2: The tiger sees the tiger.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("tiger" "sees" "tiger" "+")
The cat does not see the tiger.
Unknown
inv-rconc
[@2: The cat sees the tiger.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("cat" "sees" "tiger" "-")
The tiger sees the cat.
Unknown
rconc
[@1: The tiger sees the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "sees" "cat" "+")
The bear does not like the cat.
Unknown
inv-random
[@0: The bear likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "cat" "-")
The lion is nice.
Unknown
random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "+")
The tiger does not see the bear.
Unknown
inv-random
[@0: The tiger sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "bear" "-")
The cat likes the lion.
Unknown
random
[@0: The cat likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "lion" "+")
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The cat likes the bear.
Unknown
random
[@0: The cat likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "bear" "+")
@0: The bear sees the tiger.[(triple1)] The bear visits the lion.[(triple2)] The cat sees the lion.[(triple3)] The lion is round.[(triple4)] The lion likes the tiger.[(triple5)] The lion visits the bear.[(triple6)] The lion visits the tiger.[(triple7)] The tiger is nice.[(triple8)] The tiger likes the bear.[(triple9)] The tiger likes the lion.[(triple10)] The tiger visits the lion.[(triple11)] @1: The lion is kind.[(((triple7 triple10) -> rule7))] The tiger likes the tiger.[(((triple8) -> rule8))] @2: The lion is rough.[(((triple11 ((triple8) -> rule8)) -> rule5))] The lion sees the tiger.[(((triple10 ((triple8) -> rule8)) -> rule2) OR ((((triple4 ((triple11 ((triple8) -> rule8)) -> rule5)) -> rule4)) -> rule6))] @3: The lion sees the cat.[(((((triple11 ((triple8) -> rule8)) -> rule5)) -> rule1))] The lion visits the cat.[(((triple4 ((triple11 ((triple8) -> rule8)) -> rule5)) -> rule4))] @4: The cat is nice.[(((((triple7 triple10) -> rule7) ((((triple11 ((triple8) -> rule8)) -> rule5)) -> rule1)) -> rule3))] @5: The cat likes the tiger.[(((((((triple7 triple10) -> rule7) ((((triple11 ((triple8) -> rule8)) -> rule5)) -> rule1)) -> rule3)) -> rule8))]
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple1
The bear visits the lion.
("bear" "visits" "lion" "+")
triple2
The cat sees the lion.
("cat" "sees" "lion" "+")
triple3
The lion is round.
("lion" "is" "round" "+")
triple4
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple5
The lion visits the bear.
("lion" "visits" "bear" "+")
triple6
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple7
The tiger is nice.
("tiger" "is" "nice" "+")
triple8
The tiger likes the bear.
("tiger" "likes" "bear" "+")
triple9
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple10
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple11
The lion is kind.
("lion" "is" "kind" "+")
((triple7 triple10) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple8) -> (rule8 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
((triple11 ((triple8) -> (rule8 % int2))) -> (rule5 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
((triple10 ((triple8) -> (rule8 % int2))) -> (rule2 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
((((triple4 ((triple11 ((triple8) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int4
The lion sees the cat.
("lion" "sees" "cat" "+")
((((triple11 ((triple8) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The lion visits the cat.
("lion" "visits" "cat" "+")
((triple4 ((triple11 ((triple8) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The cat is nice.
("cat" "is" "nice" "+")
((((triple7 triple10) -> (rule7 % int5)) ((((triple11 ((triple8) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int4
The lion is kind.
("lion" "is" "kind" "+")
int5
The cat likes the tiger.
("cat" "likes" "tiger" "+")
((((((triple7 triple10) -> (rule7 % int6)) ((((triple11 ((triple8) -> (rule8 % int5))) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
int3
The lion is rough.
("lion" "is" "rough" "+")
int4
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int5
The lion is kind.
("lion" "is" "kind" "+")
int6