The cat is not round. The cow chases the cat. The dog eats the cow. The lion likes the dog. If something likes the dog then the dog chases the lion. If something is red then it chases the lion. If something likes the cat then it does not eat the cow. If something chases the cow then the cow is round. If something eats the cat and it chases the cat then it is round. If something chases the lion then it chases the cow.
The cat is not round.
("cat" "is" "round" "-")
The cow chases the cat.
("cow" "chases" "cat" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
The lion likes the dog.
("lion" "likes" "dog" "+")
If something likes the dog then the dog chases the lion.
((("something" "likes" "dog" "+")) -> ("dog" "chases" "lion" "+"))
If something is red then it chases the lion.
((("something" "is" "red" "+")) -> ("something" "chases" "lion" "+"))
If something likes the cat then it does not eat the cow.
((("something" "likes" "cat" "+")) -> ("something" "eats" "cow" "-"))
If something chases the cow then the cow is round.
((("something" "chases" "cow" "+")) -> ("cow" "is" "round" "+"))
If something eats the cat and it chases the cat then it is round.
((("something" "eats" "cat" "+") ("something" "chases" "cat" "+")) -> ("something" "is" "round" "+"))
If something chases the lion then it chases the cow.
((("something" "chases" "lion" "+")) -> ("something" "chases" "cow" "+"))
The cow chases the cat.
True
1
proof
[(triple2)]
("cow" "chases" "cat" "+")
triple2
The lion does not like the dog.
False
1
inv-proof
[(triple4)]
("lion" "likes" "dog" "-")
triple4
The dog chases the lion.
True
2
proof
[(((triple4) -> rule1))]
("dog" "chases" "lion" "+")
((triple4) -> (rule1 % int1))
The dog chases the lion.
("dog" "chases" "lion" "+")
int1
The dog does not chase the lion.
False
2
inv-proof
[(((triple4) -> rule1))]
("dog" "chases" "lion" "-")
((triple4) -> (rule1 % int1))
The dog chases the lion.
("dog" "chases" "lion" "+")
int1
The dog chases the cow.
True
3
proof
[(((((triple4) -> rule1)) -> rule6))]
("dog" "chases" "cow" "+")
((((triple4) -> (rule1 % int2))) -> (rule6 % int1))
The dog chases the cow.
("dog" "chases" "cow" "+")
int1
The dog chases the lion.
("dog" "chases" "lion" "+")
int2
The dog does not chase the cow.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule6))]
("dog" "chases" "cow" "-")
((((triple4) -> (rule1 % int2))) -> (rule6 % int1))
The dog chases the cow.
("dog" "chases" "cow" "+")
int1
The dog chases the lion.
("dog" "chases" "lion" "+")
int2
The cow is round.
True
4
proof
[(((((((triple4) -> rule1)) -> rule6)) -> rule4))]
("cow" "is" "round" "+")
((((((triple4) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
int2
The dog chases the lion.
("dog" "chases" "lion" "+")
int3
The cow is not round.
False
4
inv-proof
[(((((((triple4) -> rule1)) -> rule6)) -> rule4))]
("cow" "is" "round" "-")
((((((triple4) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
int2
The dog chases the lion.
("dog" "chases" "lion" "+")
int3
The lion does not chase the cow.
Unknown
inv-rconc
[@2: The lion chases the cow.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("lion" "chases" "cow" "-")
The cow chases the lion.
Unknown
rconc
[@1: The cow chases the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "chases" "lion" "+")
The cat does not chase the lion.
Unknown
inv-rconc
[@1: The cat chases the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "chases" "lion" "-")
The cat chases the cow.
Unknown
rconc
[@2: The cat chases the cow.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("cat" "chases" "cow" "+")
The cat is not kind.
Unknown
inv-random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "-")
The dog likes the cow.
Unknown
random
[@0: The dog likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "cow" "+")
The lion does not chase the dog.
Unknown
inv-random
[@0: The lion chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "dog" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
@0: The cat is not round.[(triple1)] The cow chases the cat.[(triple2)] The dog eats the cow.[(triple3)] The lion likes the dog.[(triple4)] @1: The dog chases the lion.[(((triple4) -> rule1))] @2: The dog chases the cow.[(((((triple4) -> rule1)) -> rule6))] @3: The cow is round.[(((((((triple4) -> rule1)) -> rule6)) -> rule4))]
The cat is not round.
("cat" "is" "round" "-")
triple1
The cow chases the cat.
("cow" "chases" "cat" "+")
triple2
The dog eats the cow.
("dog" "eats" "cow" "+")
triple3
The lion likes the dog.
("lion" "likes" "dog" "+")
triple4
The dog chases the lion.
("dog" "chases" "lion" "+")
((triple4) -> (rule1 % int1))
The dog chases the lion.
("dog" "chases" "lion" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
((((triple4) -> (rule1 % int2))) -> (rule6 % int1))
The dog chases the cow.
("dog" "chases" "cow" "+")
int1
The dog chases the lion.
("dog" "chases" "lion" "+")
int2
The cow is round.
("cow" "is" "round" "+")
((((((triple4) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
int2
The dog chases the lion.
("dog" "chases" "lion" "+")
int3