The bear is blue. The bear is kind. The bear sees the tiger. The bear visits the tiger. The dog chases the tiger. The dog visits the tiger. The tiger chases the dog. If something visits the dog then it sees the dog. If something is big and nice then it is cold. If something chases the dog and the dog visits the tiger then the dog chases the bear. If something visits the dog and the dog is blue then it chases the bear. Kind, blue things are big. If the dog chases the tiger and the dog is big then the dog sees the bear.
The bear is blue.
("bear" "is" "blue" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
If something visits the dog then it sees the dog.
((("something" "visits" "dog" "+")) -> ("something" "sees" "dog" "+"))
If something is big and nice then it is cold.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something chases the dog and the dog visits the tiger then the dog chases the bear.
((("something" "chases" "dog" "+") ("dog" "visits" "tiger" "+")) -> ("dog" "chases" "bear" "+"))
If something visits the dog and the dog is blue then it chases the bear.
((("something" "visits" "dog" "+") ("dog" "is" "blue" "+")) -> ("something" "chases" "bear" "+"))
Kind, blue things are big.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If the dog chases the tiger and the dog is big then the dog sees the bear.
((("dog" "chases" "tiger" "+") ("dog" "is" "big" "+")) -> ("dog" "sees" "bear" "+"))
The bear visits the tiger.
True
1
proof
[(triple4)]
("bear" "visits" "tiger" "+")
triple4
The bear does not see the tiger.
False
1
inv-proof
[(triple3)]
("bear" "sees" "tiger" "-")
triple3
The bear is big.
True
3
proof
[(((triple2 triple1) -> rule5))]
("bear" "is" "big" "+")
((triple2 triple1) -> (rule5 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The dog does not chase the bear.
False
3
inv-proof
[(((triple7 triple6) -> rule3))]
("dog" "chases" "bear" "-")
((triple7 triple6) -> (rule3 % int1))
The dog chases the bear.
("dog" "chases" "bear" "+")
int1
The bear does not chase the bear.
Unknown
inv-rconc
[@1: The bear chases the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "chases" "bear" "-")
The tiger is cold.
Unknown
rconc
[@1: The tiger is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "cold" "+")
The tiger is not blue.
Unknown
inv-random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
@0: The bear is blue.[(triple1)] The bear is kind.[(triple2)] The bear sees the tiger.[(triple3)] The bear visits the tiger.[(triple4)] The dog chases the tiger.[(triple5)] The dog visits the tiger.[(triple6)] The tiger chases the dog.[(triple7)] @1: The bear is big.[(((triple2 triple1) -> rule5))] The dog chases the bear.[(((triple7 triple6) -> rule3))]
The bear is blue.
("bear" "is" "blue" "+")
triple1
The bear is kind.
("bear" "is" "kind" "+")
triple2
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple3
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple4
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple5
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple6
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple7
The bear is big.
("bear" "is" "big" "+")
((triple2 triple1) -> (rule5 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The dog chases the bear.
("dog" "chases" "bear" "+")
((triple7 triple6) -> (rule3 % int1))
The dog chases the bear.
("dog" "chases" "bear" "+")
int1