The bear sees the cat. The bear sees the rabbit. The bear visits the cat. The cat chases the bear. The cat is nice. The cat is red. The cat sees the rabbit. The cat visits the rabbit. The rabbit is red. The rabbit is young. If someone is young then they chase the bear. If the rabbit is young and the rabbit visits the cat then the rabbit chases the cat. If someone is nice and they see the rabbit then the rabbit is young. If someone sees the rabbit and the rabbit is green then they see the bear. If someone visits the rabbit and they chase the cat then the rabbit visits the cat. If someone sees the rabbit then they chase the cat. If someone is red and they see the cat then the cat is green. If someone is green then they visit the bear.
The bear sees the cat.
("bear" "sees" "cat" "+")
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
The bear visits the cat.
("bear" "visits" "cat" "+")
The cat chases the bear.
("cat" "chases" "bear" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is red.
("cat" "is" "red" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
If someone is young then they chase the bear.
((("someone" "is" "young" "+")) -> ("someone" "chases" "bear" "+"))
If the rabbit is young and the rabbit visits the cat then the rabbit chases the cat.
((("rabbit" "is" "young" "+") ("rabbit" "visits" "cat" "+")) -> ("rabbit" "chases" "cat" "+"))
If someone is nice and they see the rabbit then the rabbit is young.
((("someone" "is" "nice" "+") ("someone" "sees" "rabbit" "+")) -> ("rabbit" "is" "young" "+"))
If someone sees the rabbit and the rabbit is green then they see the bear.
((("someone" "sees" "rabbit" "+") ("rabbit" "is" "green" "+")) -> ("someone" "sees" "bear" "+"))
If someone visits the rabbit and they chase the cat then the rabbit visits the cat.
((("someone" "visits" "rabbit" "+") ("someone" "chases" "cat" "+")) -> ("rabbit" "visits" "cat" "+"))
If someone sees the rabbit then they chase the cat.
((("someone" "sees" "rabbit" "+")) -> ("someone" "chases" "cat" "+"))
If someone is red and they see the cat then the cat is green.
((("someone" "is" "red" "+") ("someone" "sees" "cat" "+")) -> ("cat" "is" "green" "+"))
If someone is green then they visit the bear.
((("someone" "is" "green" "+")) -> ("someone" "visits" "bear" "+"))
The cat chases the bear.
True
1
proof
[(triple4)]
("cat" "chases" "bear" "+")
triple4
The rabbit is not young.
False
1
inv-proof
[(triple10 OR ((triple5 triple7) -> rule3))]
("rabbit" "is" "young" "-")
triple10
((triple5 triple7) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The bear chases the cat.
True
2
proof
[(((triple2) -> rule6))]
("bear" "chases" "cat" "+")
((triple2) -> (rule6 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The bear does not chase the cat.
False
2
inv-proof
[(((triple2) -> rule6))]
("bear" "chases" "cat" "-")
((triple2) -> (rule6 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The rabbit visits the cat.
True
4
proof
[(((triple8 ((triple7) -> rule6)) -> rule5))]
("rabbit" "visits" "cat" "+")
((triple8 ((triple7) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The rabbit does not visit the cat.
False
4
inv-proof
[(((triple8 ((triple7) -> rule6)) -> rule5))]
("rabbit" "visits" "cat" "-")
((triple8 ((triple7) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The rabbit chases the cat.
True
6
proof
[(((triple10 ((triple8 ((triple7) -> rule6)) -> rule5)) -> rule2) OR ((((triple5 triple7) -> rule3) ((triple8 ((triple7) -> rule6)) -> rule5)) -> rule2))]
("rabbit" "chases" "cat" "+")
((triple10 ((triple8 ((triple7) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
((((triple5 triple7) -> (rule3 % int4)) ((triple8 ((triple7) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
The rabbit is young.
("rabbit" "is" "young" "+")
int4
The rabbit does not chase the cat.
False
6
inv-proof
[(((triple10 ((triple8 ((triple7) -> rule6)) -> rule5)) -> rule2) OR ((((triple5 triple7) -> rule3) ((triple8 ((triple7) -> rule6)) -> rule5)) -> rule2))]
("rabbit" "chases" "cat" "-")
((triple10 ((triple8 ((triple7) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
((((triple5 triple7) -> (rule3 % int4)) ((triple8 ((triple7) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
The rabbit is young.
("rabbit" "is" "young" "+")
int4
The rabbit does not see the bear.
Unknown
inv-rconc
[@1: The rabbit sees the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "sees" "bear" "-")
The bear visits the bear.
Unknown
rconc
[@1: The bear visits the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "visits" "bear" "+")
The rabbit does not visit the bear.
Unknown
inv-rconc
[@1: The rabbit visits the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "visits" "bear" "-")
The cat sees the bear.
Unknown
rconc
[@1: The cat sees the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "sees" "bear" "+")
The bear does not visit the rabbit.
Unknown
inv-random
[@0: The bear visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "rabbit" "-")
The bear is nice.
Unknown
random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "+")
The rabbit is not green.
Unknown
inv-random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "-")
The cat chases the rabbit.
Unknown
random
[@0: The cat chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "rabbit" "+")
@0: The bear sees the cat.[(triple1)] The bear sees the rabbit.[(triple2)] The bear visits the cat.[(triple3)] The cat chases the bear.[(triple4)] The cat is nice.[(triple5)] The cat is red.[(triple6)] The cat sees the rabbit.[(triple7)] The cat visits the rabbit.[(triple8)] The rabbit is red.[(triple9)] The rabbit is young.[(triple10 OR ((triple5 triple7) -> rule3))] @1: The bear chases the cat.[(((triple2) -> rule6))] The cat chases the cat.[(((triple7) -> rule6))] The rabbit chases the bear.[(((triple10) -> rule1) OR ((((triple5 triple7) -> rule3)) -> rule1))] @2: The rabbit visits the cat.[(((triple8 ((triple7) -> rule6)) -> rule5))] @3: The rabbit chases the cat.[(((triple10 ((triple8 ((triple7) -> rule6)) -> rule5)) -> rule2) OR ((((triple5 triple7) -> rule3) ((triple8 ((triple7) -> rule6)) -> rule5)) -> rule2))]
The bear sees the cat.
("bear" "sees" "cat" "+")
triple1
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple2
The bear visits the cat.
("bear" "visits" "cat" "+")
triple3
The cat chases the bear.
("cat" "chases" "bear" "+")
triple4
The cat is nice.
("cat" "is" "nice" "+")
triple5
The cat is red.
("cat" "is" "red" "+")
triple6
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple7
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple8
The rabbit is red.
("rabbit" "is" "red" "+")
triple9
The rabbit is young.
("rabbit" "is" "young" "+")
triple10
((triple5 triple7) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The bear chases the cat.
("bear" "chases" "cat" "+")
((triple2) -> (rule6 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
((triple7) -> (rule6 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
((triple10) -> (rule1 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
((((triple5 triple7) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
((triple8 ((triple7) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
((triple10 ((triple8 ((triple7) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
((((triple5 triple7) -> (rule3 % int4)) ((triple8 ((triple7) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
int2
The cat chases the cat.
("cat" "chases" "cat" "+")
int3
The rabbit is young.
("rabbit" "is" "young" "+")
int4