The bear is not kind. The bear is nice. The bear is round. The bear sees the cat. The bear sees the rabbit. The cat chases the rabbit. The cat is big. The cat is kind. The cat sees the bear. The cat sees the rabbit. The cat visits the bear. The cat visits the rabbit. The rabbit chases the bear. The rabbit does not chase the cat. The rabbit sees the cat. If something is green then it visits the bear. If the cat is round and the cat is not big then the cat sees the bear. If something visits the bear then it visits the cat.
The bear is not kind.
("bear" "is" "kind" "-")
The bear is nice.
("bear" "is" "nice" "+")
The bear is round.
("bear" "is" "round" "+")
The bear sees the cat.
("bear" "sees" "cat" "+")
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat sees the bear.
("cat" "sees" "bear" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
If something is green then it visits the bear.
((("something" "is" "green" "+")) -> ("something" "visits" "bear" "+"))
If the cat is round and the cat is not big then the cat sees the bear.
((("cat" "is" "round" "+") ("cat" "is" "big" "~")) -> ("cat" "sees" "bear" "+"))
If something visits the bear then it visits the cat.
((("something" "visits" "bear" "+")) -> ("something" "visits" "cat" "+"))
The bear is round.
True
1
proof
[(triple3)]
("bear" "is" "round" "+")
triple3
The rabbit does not see the cat.
False
1
inv-proof
[(triple15)]
("rabbit" "sees" "cat" "-")
triple15
The rabbit does not visit the bear.
Unknown
inv-rconc
[@1: The rabbit visits the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "visits" "bear" "-")
The bear chases the cat.
Unknown
random
[@0: The bear chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "cat" "+")
@0: The bear is nice.[(triple2)] The bear is not kind.[(triple1)] The bear is round.[(triple3)] The bear sees the cat.[(triple4)] The bear sees the rabbit.[(triple5)] The cat chases the rabbit.[(triple6)] The cat is big.[(triple7)] The cat is kind.[(triple8)] The cat sees the bear.[(triple9)] The cat sees the rabbit.[(triple10)] The cat visits the bear.[(triple11)] The cat visits the rabbit.[(triple12)] The rabbit chases the bear.[(triple13)] The rabbit does not chase the cat.[(triple14)] The rabbit sees the cat.[(triple15)] @1: The cat visits the cat.[(((triple11) -> rule3))]
The bear is nice.
("bear" "is" "nice" "+")
triple2
The bear is not kind.
("bear" "is" "kind" "-")
triple1
The bear is round.
("bear" "is" "round" "+")
triple3
The bear sees the cat.
("bear" "sees" "cat" "+")
triple4
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple5
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple6
The cat is big.
("cat" "is" "big" "+")
triple7
The cat is kind.
("cat" "is" "kind" "+")
triple8
The cat sees the bear.
("cat" "sees" "bear" "+")
triple9
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple10
The cat visits the bear.
("cat" "visits" "bear" "+")
triple11
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple12
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple13
The rabbit does not chase the cat.
("rabbit" "chases" "cat" "-")
triple14
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple15
The cat visits the cat.
("cat" "visits" "cat" "+")
((triple11) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1