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