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