The cow chases the tiger. The dog is red. The dog visits the tiger. The tiger chases the cow. The tiger chases the dog. The tiger is nice. The tiger is rough. The tiger is young. The tiger likes the cow. The tiger likes the dog. If someone likes the tiger then they are big. If someone likes the dog then they are not big. If someone chases the tiger then they are not young.
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The dog is red.
("dog" "is" "red" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
If someone likes the tiger then they are big.
((("someone" "likes" "tiger" "+")) -> ("someone" "is" "big" "+"))
If someone likes the dog then they are not big.
((("someone" "likes" "dog" "+")) -> ("someone" "is" "big" "-"))
If someone chases the tiger then they are not young.
((("someone" "chases" "tiger" "+")) -> ("someone" "is" "young" "-"))
The tiger is young.
True
1
proof
[(triple8)]
("tiger" "is" "young" "+")
triple8
The tiger is not young.
False
1
inv-proof
[(triple8)]
("tiger" "is" "young" "-")
triple8
The cow is not young.
True
2
proof
[(((triple1) -> rule3))]
("cow" "is" "young" "-")
((triple1) -> (rule3 % int1))
The cow is not young.
("cow" "is" "young" "-")
int1
The tiger is big.
False
2
inv-proof
[(((triple10) -> rule2))]
("tiger" "is" "big" "+")
((triple10) -> (rule2 % int1))
The tiger is not big.
("tiger" "is" "big" "-")
int1
The cow is not big.
Unknown
inv-rconc
[@1: The cow is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "big" "-")
The dog is big.
Unknown
rconc
[@1: The dog is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "big" "+")
The cow does not visit the tiger.
Unknown
inv-random
[@0: The cow visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "tiger" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
@0: The cow chases the tiger.[(triple1)] The dog is red.[(triple2)] The dog visits the tiger.[(triple3)] The tiger chases the cow.[(triple4)] The tiger chases the dog.[(triple5)] The tiger is nice.[(triple6)] The tiger is rough.[(triple7)] The tiger is young.[(triple8)] The tiger likes the cow.[(triple9)] The tiger likes the dog.[(triple10)] @1: The cow is not young.[(((triple1) -> rule3))] The tiger is not big.[(((triple10) -> rule2))]
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple1
The dog is red.
("dog" "is" "red" "+")
triple2
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple3
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple4
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple5
The tiger is nice.
("tiger" "is" "nice" "+")
triple6
The tiger is rough.
("tiger" "is" "rough" "+")
triple7
The tiger is young.
("tiger" "is" "young" "+")
triple8
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple9
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple10
The cow is not young.
("cow" "is" "young" "-")
((triple1) -> (rule3 % int1))
The cow is not young.
("cow" "is" "young" "-")
int1
The tiger is not big.
("tiger" "is" "big" "-")
((triple10) -> (rule2 % int1))
The tiger is not big.
("tiger" "is" "big" "-")
int1