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