The bear chases the dog. The bear is red. The bear is rough. The bear likes the dog. The bear needs the tiger. The dog chases the tiger. The dog is big. The dog is red. The dog is rough. The dog likes the bear. The tiger chases the bear. The tiger chases the dog. The tiger is big. The tiger is green. The tiger is rough. The tiger likes the bear. All green things are kind.
The bear chases the dog.
("bear" "chases" "dog" "+")
The bear is red.
("bear" "is" "red" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear likes the dog.
("bear" "likes" "dog" "+")
The bear needs the tiger.
("bear" "needs" "tiger" "+")
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog likes the bear.
("dog" "likes" "bear" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger likes the bear.
("tiger" "likes" "bear" "+")
All green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
The dog is rough.
True
1
proof
[(triple9)]
("dog" "is" "rough" "+")
triple9
The bear is not rough.
False
1
inv-proof
[(triple3)]
("bear" "is" "rough" "-")
triple3
The tiger is kind.
True
2
proof
[(((triple14) -> rule1))]
("tiger" "is" "kind" "+")
((triple14) -> (rule1 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is not kind.
False
2
inv-proof
[(((triple14) -> rule1))]
("tiger" "is" "kind" "-")
((triple14) -> (rule1 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The bear is not kind.
Unknown
inv-rconc
[@1: The bear is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "kind" "-")
The dog is kind.
Unknown
rconc
[@1: The dog is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "kind" "+")
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
@0: The bear chases the dog.[(triple1)] The bear is red.[(triple2)] The bear is rough.[(triple3)] The bear likes the dog.[(triple4)] The bear needs the tiger.[(triple5)] The dog chases the tiger.[(triple6)] The dog is big.[(triple7)] The dog is red.[(triple8)] The dog is rough.[(triple9)] The dog likes the bear.[(triple10)] The tiger chases the bear.[(triple11)] The tiger chases the dog.[(triple12)] The tiger is big.[(triple13)] The tiger is green.[(triple14)] The tiger is rough.[(triple15)] The tiger likes the bear.[(triple16)] @1: The tiger is kind.[(((triple14) -> rule1))]
The bear chases the dog.
("bear" "chases" "dog" "+")
triple1
The bear is red.
("bear" "is" "red" "+")
triple2
The bear is rough.
("bear" "is" "rough" "+")
triple3
The bear likes the dog.
("bear" "likes" "dog" "+")
triple4
The bear needs the tiger.
("bear" "needs" "tiger" "+")
triple5
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple6
The dog is big.
("dog" "is" "big" "+")
triple7
The dog is red.
("dog" "is" "red" "+")
triple8
The dog is rough.
("dog" "is" "rough" "+")
triple9
The dog likes the bear.
("dog" "likes" "bear" "+")
triple10
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple11
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple12
The tiger is big.
("tiger" "is" "big" "+")
triple13
The tiger is green.
("tiger" "is" "green" "+")
triple14
The tiger is rough.
("tiger" "is" "rough" "+")
triple15
The tiger likes the bear.
("tiger" "likes" "bear" "+")
triple16
The tiger is kind.
("tiger" "is" "kind" "+")
((triple14) -> (rule1 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1