The cow chases the dog. The dog is green. The lion chases the cow. If someone chases the cow then they chase the lion. If someone eats the dog then they need the cow. If someone chases the lion then they eat the lion.
The cow chases the dog.
("cow" "chases" "dog" "+")
The dog is green.
("dog" "is" "green" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
If someone chases the cow then they chase the lion.
((("someone" "chases" "cow" "+")) -> ("someone" "chases" "lion" "+"))
If someone eats the dog then they need the cow.
((("someone" "eats" "dog" "+")) -> ("someone" "needs" "cow" "+"))
If someone chases the lion then they eat the lion.
((("someone" "chases" "lion" "+")) -> ("someone" "eats" "lion" "+"))
The lion chases the cow.
True
1
proof
[(triple3)]
("lion" "chases" "cow" "+")
triple3
The cow does not chase the dog.
False
1
inv-proof
[(triple1)]
("cow" "chases" "dog" "-")
triple1
The lion chases the lion.
True
2
proof
[(((triple3) -> rule1))]
("lion" "chases" "lion" "+")
((triple3) -> (rule1 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion does not chase the lion.
False
2
inv-proof
[(((triple3) -> rule1))]
("lion" "chases" "lion" "-")
((triple3) -> (rule1 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion eats the lion.
True
3
proof
[(((((triple3) -> rule1)) -> rule3))]
("lion" "eats" "lion" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion does not eat the lion.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule3))]
("lion" "eats" "lion" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The cow does not eat the lion.
Unknown
inv-rconc
[@2: The cow eats the lion.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("cow" "eats" "lion" "-")
The lion needs the cow.
Unknown
rconc
[@1: The lion needs the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "needs" "cow" "+")
The dog does not chase the lion.
Unknown
inv-rconc
[@1: The dog chases the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "chases" "lion" "-")
The dog needs the lion.
Unknown
random
[@0: The dog needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "lion" "+")
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The dog chases the cow.
Unknown
random
[@0: The dog chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "cow" "+")
@0: The cow chases the dog.[(triple1)] The dog is green.[(triple2)] The lion chases the cow.[(triple3)] @1: The lion chases the lion.[(((triple3) -> rule1))] @2: The lion eats the lion.[(((((triple3) -> rule1)) -> rule3))]
The cow chases the dog.
("cow" "chases" "dog" "+")
triple1
The dog is green.
("dog" "is" "green" "+")
triple2
The lion chases the cow.
("lion" "chases" "cow" "+")
triple3
The lion chases the lion.
("lion" "chases" "lion" "+")
((triple3) -> (rule1 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2