The cow chases the dog. The cow eats the tiger. The cow is round. The cow is young. The cow visits the tiger. The dog chases the cow. The dog eats the cow. The dog eats the tiger. The tiger chases the cow. The tiger chases the dog. The tiger eats the cow. The tiger eats the dog. The tiger is nice. The tiger is round. The tiger visits the cow. The tiger visits the dog. If something visits the cow then the cow is round. If something visits the cow and it eats the cow then it chases the dog. If the dog eats the tiger then the dog eats the cow.
The cow chases the dog.
("cow" "chases" "dog" "+")
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The cow is round.
("cow" "is" "round" "+")
The cow is young.
("cow" "is" "young" "+")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The tiger chases the cow.
("tiger" "chases" "cow" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger eats the dog.
("tiger" "eats" "dog" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If something visits the cow then the cow is round.
((("something" "visits" "cow" "+")) -> ("cow" "is" "round" "+"))
If something visits the cow and it eats the cow then it chases the dog.
((("something" "visits" "cow" "+") ("something" "eats" "cow" "+")) -> ("something" "chases" "dog" "+"))
If the dog eats the tiger then the dog eats the cow.
((("dog" "eats" "tiger" "+")) -> ("dog" "eats" "cow" "+"))
The cow eats the tiger.
True
1
proof
[(triple2)]
("cow" "eats" "tiger" "+")
triple2
The dog does not chase the cow.
False
1
inv-proof
[(triple6)]
("dog" "chases" "cow" "-")
triple6
The dog does not chase the dog.
Unknown
inv-rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "chases" "dog" "-")
The cow is kind.
Unknown
random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "+")
@0: The cow chases the dog.[(triple1)] The cow eats the tiger.[(triple2)] The cow is round.[(triple3 OR ((triple15) -> rule1))] The cow is young.[(triple4)] The cow visits the tiger.[(triple5)] The dog chases the cow.[(triple6)] The dog eats the cow.[(triple7 OR ((triple8) -> rule3))] The dog eats the tiger.[(triple8)] The tiger chases the cow.[(triple9)] The tiger chases the dog.[(triple10 OR ((triple15 triple11) -> rule2))] The tiger eats the cow.[(triple11)] The tiger eats the dog.[(triple12)] The tiger is nice.[(triple13)] The tiger is round.[(triple14)] The tiger visits the cow.[(triple15)] The tiger visits the dog.[(triple16)]
The cow chases the dog.
("cow" "chases" "dog" "+")
triple1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple2
The cow is round.
("cow" "is" "round" "+")
triple3
((triple15) -> (rule1 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow is young.
("cow" "is" "young" "+")
triple4
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple5
The dog chases the cow.
("dog" "chases" "cow" "+")
triple6
The dog eats the cow.
("dog" "eats" "cow" "+")
triple7
((triple8) -> (rule3 % int1))
The dog eats the cow.
("dog" "eats" "cow" "+")
int1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple8
The tiger chases the cow.
("tiger" "chases" "cow" "+")
triple9
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple10
((triple15 triple11) -> (rule2 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple11
The tiger eats the dog.
("tiger" "eats" "dog" "+")
triple12
The tiger is nice.
("tiger" "is" "nice" "+")
triple13
The tiger is round.
("tiger" "is" "round" "+")
triple14
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple15
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple16