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