The cow eats the tiger. The dog is nice. The lion eats the tiger. The tiger eats the cow. If the cow visits the lion then the cow is not nice. If something eats the cow and the cow does not visit the dog then it needs the cow. If something eats the tiger then the tiger is not round. If something eats the dog then the dog is not red. If the cow is young and the cow visits the dog then the dog is red. If something is red and it visits the lion then the lion visits the cow. If something needs the tiger and the tiger is not round then the tiger eats the dog. If something eats the tiger then the tiger eats the dog.
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The dog is nice.
("dog" "is" "nice" "+")
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
If the cow visits the lion then the cow is not nice.
((("cow" "visits" "lion" "+")) -> ("cow" "is" "nice" "-"))
If something eats the cow and the cow does not visit the dog then it needs the cow.
((("something" "eats" "cow" "+") ("cow" "visits" "dog" "~")) -> ("something" "needs" "cow" "+"))
If something eats the tiger then the tiger is not round.
((("something" "eats" "tiger" "+")) -> ("tiger" "is" "round" "-"))
If something eats the dog then the dog is not red.
((("something" "eats" "dog" "+")) -> ("dog" "is" "red" "-"))
If the cow is young and the cow visits the dog then the dog is red.
((("cow" "is" "young" "+") ("cow" "visits" "dog" "+")) -> ("dog" "is" "red" "+"))
If something is red and it visits the lion then the lion visits the cow.
((("something" "is" "red" "+") ("something" "visits" "lion" "+")) -> ("lion" "visits" "cow" "+"))
If something needs the tiger and the tiger is not round then the tiger eats the dog.
((("something" "needs" "tiger" "+") ("tiger" "is" "round" "~")) -> ("tiger" "eats" "dog" "+"))
If something eats the tiger then the tiger eats the dog.
((("something" "eats" "tiger" "+")) -> ("tiger" "eats" "dog" "+"))
The lion eats the tiger.
True
1
proof
[(triple3)]
("lion" "eats" "tiger" "+")
triple3
The dog is not nice.
False
1
inv-proof
[(triple2)]
("dog" "is" "nice" "-")
triple2
The tiger is not round.
True
2
proof
[(((triple1) -> rule3) OR ((triple3) -> rule3))]
("tiger" "is" "round" "-")
((triple1) -> (rule3 % int1))
The tiger is not round.
("tiger" "is" "round" "-")
int1
((triple3) -> (rule3 % int1))
The tiger is not round.
("tiger" "is" "round" "-")
int1
The tiger does not eat the dog.
False
2
inv-proof
[(((triple1) -> rule8) OR ((triple3) -> rule8))]
("tiger" "eats" "dog" "-")
((triple1) -> (rule8 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
((triple3) -> (rule8 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The dog is not red.
True
3
proof
[(((((triple1) -> rule8)) -> rule4) OR ((((triple3) -> rule8)) -> rule4))]
("dog" "is" "red" "-")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The dog is not red.
("dog" "is" "red" "-")
int1
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int2
((((triple3) -> (rule8 % int2))) -> (rule4 % int1))
The dog is not red.
("dog" "is" "red" "-")
int1
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int2
The dog is red.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule4) OR ((((triple3) -> rule8)) -> rule4))]
("dog" "is" "red" "+")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The dog is not red.
("dog" "is" "red" "-")
int1
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int2
((((triple3) -> (rule8 % int2))) -> (rule4 % int1))
The dog is not red.
("dog" "is" "red" "-")
int1
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int2
The cow does not need the cow.
Unknown
inv-rconc
[@1: The cow needs the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "needs" "cow" "-")
The tiger needs the cow.
Unknown
rconc
[@1: The tiger needs the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "needs" "cow" "+")
The dog does not need the cow.
Unknown
inv-rconc
[@1: The dog needs the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "needs" "cow" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
The tiger does not eat the lion.
Unknown
inv-random
[@0: The tiger eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "lion" "-")
The tiger visits the lion.
Unknown
random
[@0: The tiger visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "lion" "+")
@0: The cow eats the tiger.[(triple1)] The dog is nice.[(triple2)] The lion eats the tiger.[(triple3)] The tiger eats the cow.[(triple4)] @1: The tiger eats the dog.[(((triple1) -> rule8) OR ((triple3) -> rule8))] The tiger is not round.[(((triple1) -> rule3) OR ((triple3) -> rule3))] @2: The dog is not red.[(((((triple1) -> rule8)) -> rule4) OR ((((triple3) -> rule8)) -> rule4))]
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple1
The dog is nice.
("dog" "is" "nice" "+")
triple2
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple3
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple4
The tiger eats the dog.
("tiger" "eats" "dog" "+")
((triple1) -> (rule8 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
((triple3) -> (rule8 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The tiger is not round.
("tiger" "is" "round" "-")
((triple1) -> (rule3 % int1))
The tiger is not round.
("tiger" "is" "round" "-")
int1
((triple3) -> (rule3 % int1))
The tiger is not round.
("tiger" "is" "round" "-")
int1
The dog is not red.
("dog" "is" "red" "-")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The dog is not red.
("dog" "is" "red" "-")
int1
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int2
((((triple3) -> (rule8 % int2))) -> (rule4 % int1))
The dog is not red.
("dog" "is" "red" "-")
int1
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int2