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