The bear chases the cat. The bear chases the rabbit. The bear is red. The bear is young. The bear likes the rabbit. The bear visits the cat. The cat chases the bear. The cat chases the rabbit. The cat is red. The cat is rough. The cat is young. The cat likes the bear. The cat likes the rabbit. The rabbit chases the bear. The rabbit is red. The rabbit likes the cat. If someone is red and they like the bear then they chase the bear. If the bear chases the rabbit then the rabbit likes the bear. If someone visits the cat then they are kind. If someone chases the bear and they visit the rabbit then the rabbit visits the cat. If someone visits the rabbit and the rabbit is young then the rabbit chases the bear. If someone is young and cold then they visit the rabbit. All rough people are cold. If someone visits the cat then they are kind.
The bear chases the cat.
("bear" "chases" "cat" "+")
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The bear is red.
("bear" "is" "red" "+")
The bear is young.
("bear" "is" "young" "+")
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The bear visits the cat.
("bear" "visits" "cat" "+")
The cat chases the bear.
("cat" "chases" "bear" "+")
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the bear.
("cat" "likes" "bear" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
If someone is red and they like the bear then they chase the bear.
((("someone" "is" "red" "+") ("someone" "likes" "bear" "+")) -> ("someone" "chases" "bear" "+"))
If the bear chases the rabbit then the rabbit likes the bear.
((("bear" "chases" "rabbit" "+")) -> ("rabbit" "likes" "bear" "+"))
If someone visits the cat then they are kind.
((("someone" "visits" "cat" "+")) -> ("someone" "is" "kind" "+"))
If someone chases the bear and they visit the rabbit then the rabbit visits the cat.
((("someone" "chases" "bear" "+") ("someone" "visits" "rabbit" "+")) -> ("rabbit" "visits" "cat" "+"))
If someone visits the rabbit and the rabbit is young then the rabbit chases the bear.
((("someone" "visits" "rabbit" "+") ("rabbit" "is" "young" "+")) -> ("rabbit" "chases" "bear" "+"))
If someone is young and cold then they visit the rabbit.
((("someone" "is" "young" "+") ("someone" "is" "cold" "+")) -> ("someone" "visits" "rabbit" "+"))
All rough people are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If someone visits the cat then they are kind.
((("someone" "visits" "cat" "+")) -> ("someone" "is" "kind" "+"))
The bear visits the cat.
True
1
proof
[(triple6)]
("bear" "visits" "cat" "+")
triple6
The cat is not young.
False
1
inv-proof
[(triple11)]
("cat" "is" "young" "-")
triple11
The bear is kind.
True
2
proof
[(((triple6) -> rule3) OR ((triple6) -> rule8))]
("bear" "is" "kind" "+")
((triple6) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
((triple6) -> (rule8 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The cat is not cold.
False
2
inv-proof
[(((triple10) -> rule7))]
("cat" "is" "cold" "-")
((triple10) -> (rule7 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat visits the rabbit.
True
4
proof
[(((triple11 ((triple10) -> rule7)) -> rule6))]
("cat" "visits" "rabbit" "+")
((triple11 ((triple10) -> (rule7 % int2))) -> (rule6 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat does not visit the rabbit.
False
4
inv-proof
[(((triple11 ((triple10) -> rule7)) -> rule6))]
("cat" "visits" "rabbit" "-")
((triple11 ((triple10) -> (rule7 % int2))) -> (rule6 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The rabbit visits the cat.
True
6
proof
[(((triple7 ((triple11 ((triple10) -> rule7)) -> rule6)) -> rule4) OR ((((triple9 triple12) -> rule1) ((triple11 ((triple10) -> rule7)) -> rule6)) -> rule4))]
("rabbit" "visits" "cat" "+")
((triple7 ((triple11 ((triple10) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
((((triple9 triple12) -> (rule1 % int4)) ((triple11 ((triple10) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
The cat chases the bear.
("cat" "chases" "bear" "+")
int4
The rabbit does not visit the cat.
False
6
inv-proof
[(((triple7 ((triple11 ((triple10) -> rule7)) -> rule6)) -> rule4) OR ((((triple9 triple12) -> rule1) ((triple11 ((triple10) -> rule7)) -> rule6)) -> rule4))]
("rabbit" "visits" "cat" "-")
((triple7 ((triple11 ((triple10) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
((((triple9 triple12) -> (rule1 % int4)) ((triple11 ((triple10) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
The cat chases the bear.
("cat" "chases" "bear" "+")
int4
The bear is not cold.
Unknown
inv-rconc
[@1: The bear is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "is" "cold" "-")
The bear chases the bear.
Unknown
rconc
[@1: The bear chases the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "chases" "bear" "+")
The bear does not visit the rabbit.
Unknown
inv-rconc
[@2: The bear visits the rabbit.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("bear" "visits" "rabbit" "-")
The rabbit visits the rabbit.
Unknown
rconc
[@1: The rabbit visits the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "visits" "rabbit" "+")
The bear is not rough.
Unknown
inv-random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "-")
The rabbit is young.
Unknown
random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "+")
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The bear likes the cat.
Unknown
random
[@0: The bear likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "cat" "+")
@0: The bear chases the cat.[(triple1)] The bear chases the rabbit.[(triple2)] The bear is red.[(triple3)] The bear is young.[(triple4)] The bear likes the rabbit.[(triple5)] The bear visits the cat.[(triple6)] The cat chases the bear.[(triple7 OR ((triple9 triple12) -> rule1))] The cat chases the rabbit.[(triple8)] The cat is red.[(triple9)] The cat is rough.[(triple10)] The cat is young.[(triple11)] The cat likes the bear.[(triple12)] The cat likes the rabbit.[(triple13)] The rabbit chases the bear.[(triple14 OR ((triple15 ((triple2) -> rule2)) -> rule1))] The rabbit is red.[(triple15)] The rabbit likes the cat.[(triple16)] @1: The bear is kind.[(((triple6) -> rule3) OR ((triple6) -> rule8))] The cat is cold.[(((triple10) -> rule7))] The rabbit likes the bear.[(((triple2) -> rule2))] @2: The cat visits the rabbit.[(((triple11 ((triple10) -> rule7)) -> rule6))] @3: The rabbit visits the cat.[(((triple7 ((triple11 ((triple10) -> rule7)) -> rule6)) -> rule4) OR ((((triple9 triple12) -> rule1) ((triple11 ((triple10) -> rule7)) -> rule6)) -> rule4))] @4: The rabbit is kind.[(((((triple7 ((triple11 ((triple10) -> rule7)) -> rule6)) -> rule4)) -> rule3) OR ((((triple7 ((triple11 ((triple10) -> rule7)) -> rule6)) -> rule4)) -> rule8) OR ((((((triple9 triple12) -> rule1) ((triple11 ((triple10) -> rule7)) -> rule6)) -> rule4)) -> rule3) OR ((((((triple9 triple12) -> rule1) ((triple11 ((triple10) -> rule7)) -> rule6)) -> rule4)) -> rule8))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple2
The bear is red.
("bear" "is" "red" "+")
triple3
The bear is young.
("bear" "is" "young" "+")
triple4
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple5
The bear visits the cat.
("bear" "visits" "cat" "+")
triple6
The cat chases the bear.
("cat" "chases" "bear" "+")
triple7
((triple9 triple12) -> (rule1 % int1))
The cat chases the bear.
("cat" "chases" "bear" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple8
The cat is red.
("cat" "is" "red" "+")
triple9
The cat is rough.
("cat" "is" "rough" "+")
triple10
The cat is young.
("cat" "is" "young" "+")
triple11
The cat likes the bear.
("cat" "likes" "bear" "+")
triple12
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple13
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple14
((triple15 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
triple15
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple16
The bear is kind.
("bear" "is" "kind" "+")
((triple6) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
((triple6) -> (rule8 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
((triple10) -> (rule7 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
((triple2) -> (rule2 % int1))
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
((triple11 ((triple10) -> (rule7 % int2))) -> (rule6 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
((triple7 ((triple11 ((triple10) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
((((triple9 triple12) -> (rule1 % int4)) ((triple11 ((triple10) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
The cat chases the bear.
("cat" "chases" "bear" "+")
int4
The rabbit is kind.
("rabbit" "is" "kind" "+")
((((triple7 ((triple11 ((triple10) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int3
The cat is cold.
("cat" "is" "cold" "+")
int4
((((triple7 ((triple11 ((triple10) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int3
The cat is cold.
("cat" "is" "cold" "+")
int4
((((((triple9 triple12) -> (rule1 % int5)) ((triple11 ((triple10) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int3
The cat is cold.
("cat" "is" "cold" "+")
int4
The cat chases the bear.
("cat" "chases" "bear" "+")
int5
((((((triple9 triple12) -> (rule1 % int5)) ((triple11 ((triple10) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int3
The cat is cold.
("cat" "is" "cold" "+")
int4
The cat chases the bear.
("cat" "chases" "bear" "+")
int5