The bear is round. The bear needs the cow. The bear visits the cat. The cat is big. The cat is not blue. The cat is cold. The cat is round. The cat does not visit the cow. The cow is big. The cow is kind. The cow is not round. The tiger needs the bear. If something likes the tiger then it is cold. If something needs the bear then the bear does not visit the tiger. If the cat visits the tiger and the cat is not round then the cat does not visit the bear.
The bear is round.
("bear" "is" "round" "+")
The bear needs the cow.
("bear" "needs" "cow" "+")
The bear visits the cat.
("bear" "visits" "cat" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is not blue.
("cat" "is" "blue" "-")
The cat is cold.
("cat" "is" "cold" "+")
The cat is round.
("cat" "is" "round" "+")
The cat does not visit the cow.
("cat" "visits" "cow" "-")
The cow is big.
("cow" "is" "big" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is not round.
("cow" "is" "round" "-")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
If something likes the tiger then it is cold.
((("something" "likes" "tiger" "+")) -> ("something" "is" "cold" "+"))
If something needs the bear then the bear does not visit the tiger.
((("something" "needs" "bear" "+")) -> ("bear" "visits" "tiger" "-"))
If the cat visits the tiger and the cat is not round then the cat does not visit the bear.
((("cat" "visits" "tiger" "+") ("cat" "is" "round" "~")) -> ("cat" "visits" "bear" "-"))
The cow is big.
True
1
proof
[(triple9)]
("cow" "is" "big" "+")
triple9
The tiger does not need the bear.
False
1
inv-proof
[(triple12)]
("tiger" "needs" "bear" "-")
triple12
The tiger is not cold.
Unknown
inv-rconc
[@1: The tiger is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "cold" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
@0: The bear is round.[(triple1)] The bear needs the cow.[(triple2)] The bear visits the cat.[(triple3)] The cat does not visit the cow.[(triple8)] The cat is big.[(triple4)] The cat is cold.[(triple6)] The cat is not blue.[(triple5)] The cat is round.[(triple7)] The cow is big.[(triple9)] The cow is kind.[(triple10)] The cow is not round.[(triple11)] The tiger needs the bear.[(triple12)] @1: The bear does not visit the tiger.[(((triple12) -> rule2))]
The bear is round.
("bear" "is" "round" "+")
triple1
The bear needs the cow.
("bear" "needs" "cow" "+")
triple2
The bear visits the cat.
("bear" "visits" "cat" "+")
triple3
The cat does not visit the cow.
("cat" "visits" "cow" "-")
triple8
The cat is big.
("cat" "is" "big" "+")
triple4
The cat is cold.
("cat" "is" "cold" "+")
triple6
The cat is not blue.
("cat" "is" "blue" "-")
triple5
The cat is round.
("cat" "is" "round" "+")
triple7
The cow is big.
("cow" "is" "big" "+")
triple9
The cow is kind.
("cow" "is" "kind" "+")
triple10
The cow is not round.
("cow" "is" "round" "-")
triple11
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple12
The bear does not visit the tiger.
("bear" "visits" "tiger" "-")
((triple12) -> (rule2 % int1))
The bear does not visit the tiger.
("bear" "visits" "tiger" "-")
int1