The cat likes the cow. The cow likes the tiger. The dog is young. The tiger is young. If someone eats the cow then the cow chases the cat. If someone likes the tiger then they are young. If someone eats the cat and the cat likes the cow then they chase the tiger. If someone is green then they chase the tiger. If someone is young and they chase the tiger then they chase the cat. If the tiger is cold then the tiger is round. If someone likes the cow then the cow eats the cat. If someone is cold then they chase the cat.
The cat likes the cow.
("cat" "likes" "cow" "+")
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The dog is young.
("dog" "is" "young" "+")
The tiger is young.
("tiger" "is" "young" "+")
If someone eats the cow then the cow chases the cat.
((("someone" "eats" "cow" "+")) -> ("cow" "chases" "cat" "+"))
If someone likes the tiger then they are young.
((("someone" "likes" "tiger" "+")) -> ("someone" "is" "young" "+"))
If someone eats the cat and the cat likes the cow then they chase the tiger.
((("someone" "eats" "cat" "+") ("cat" "likes" "cow" "+")) -> ("someone" "chases" "tiger" "+"))
If someone is green then they chase the tiger.
((("someone" "is" "green" "+")) -> ("someone" "chases" "tiger" "+"))
If someone is young and they chase the tiger then they chase the cat.
((("someone" "is" "young" "+") ("someone" "chases" "tiger" "+")) -> ("someone" "chases" "cat" "+"))
If the tiger is cold then the tiger is round.
((("tiger" "is" "cold" "+")) -> ("tiger" "is" "round" "+"))
If someone likes the cow then the cow eats the cat.
((("someone" "likes" "cow" "+")) -> ("cow" "eats" "cat" "+"))
If someone is cold then they chase the cat.
((("someone" "is" "cold" "+")) -> ("someone" "chases" "cat" "+"))
The cat likes the cow.
True
1
proof
[(triple1)]
("cat" "likes" "cow" "+")
triple1
The dog is not young.
False
1
inv-proof
[(triple3)]
("dog" "is" "young" "-")
triple3
The cow is young.
True
2
proof
[(((triple2) -> rule2))]
("cow" "is" "young" "+")
((triple2) -> (rule2 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow is not young.
False
2
inv-proof
[(((triple2) -> rule2))]
("cow" "is" "young" "-")
((triple2) -> (rule2 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow chases the tiger.
True
4
proof
[(((((triple1) -> rule7) triple1) -> rule3))]
("cow" "chases" "tiger" "+")
((((triple1) -> (rule7 % int2)) triple1) -> (rule3 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The cow eats the cat.
("cow" "eats" "cat" "+")
int2
The cow does not chase the tiger.
False
4
inv-proof
[(((((triple1) -> rule7) triple1) -> rule3))]
("cow" "chases" "tiger" "-")
((((triple1) -> (rule7 % int2)) triple1) -> (rule3 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The cow eats the cat.
("cow" "eats" "cat" "+")
int2
The cow chases the cat.
True
7
proof
[(((((triple2) -> rule2) ((((triple1) -> rule7) triple1) -> rule3)) -> rule5))]
("cow" "chases" "cat" "+")
((((triple2) -> (rule2 % int4)) ((((triple1) -> (rule7 % int3)) triple1) -> (rule3 % int2))) -> (rule5 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int2
The cow eats the cat.
("cow" "eats" "cat" "+")
int3
The cow is young.
("cow" "is" "young" "+")
int4
The cow does not chase the cat.
False
7
inv-proof
[(((((triple2) -> rule2) ((((triple1) -> rule7) triple1) -> rule3)) -> rule5))]
("cow" "chases" "cat" "-")
((((triple2) -> (rule2 % int4)) ((((triple1) -> (rule7 % int3)) triple1) -> (rule3 % int2))) -> (rule5 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int2
The cow eats the cat.
("cow" "eats" "cat" "+")
int3
The cow is young.
("cow" "is" "young" "+")
int4
The dog does not chase the tiger.
Unknown
inv-rconc
[@1: The dog chases the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "chases" "tiger" "-")
The tiger chases the tiger.
Unknown
rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "chases" "tiger" "+")
The cat does not chase the cat.
Unknown
inv-rconc
[@2: The cat chases the cat.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("cat" "chases" "cat" "-")
The cat is young.
Unknown
rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "young" "+")
The tiger does not like the cow.
Unknown
inv-random
[@0: The tiger likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "cow" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
The dog does not eat the cat.
Unknown
inv-random
[@0: The dog eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "cat" "-")
The dog is kind.
Unknown
random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "+")
@0: The cat likes the cow.[(triple1)] The cow likes the tiger.[(triple2)] The dog is young.[(triple3)] The tiger is young.[(triple4)] @1: The cow eats the cat.[(((triple1) -> rule7))] The cow is young.[(((triple2) -> rule2))] @2: The cow chases the tiger.[(((((triple1) -> rule7) triple1) -> rule3))] @3: The cow chases the cat.[(((((triple2) -> rule2) ((((triple1) -> rule7) triple1) -> rule3)) -> rule5))]
The cat likes the cow.
("cat" "likes" "cow" "+")
triple1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple2
The dog is young.
("dog" "is" "young" "+")
triple3
The tiger is young.
("tiger" "is" "young" "+")
triple4
The cow eats the cat.
("cow" "eats" "cat" "+")
((triple1) -> (rule7 % int1))
The cow eats the cat.
("cow" "eats" "cat" "+")
int1
The cow is young.
("cow" "is" "young" "+")
((triple2) -> (rule2 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
((((triple1) -> (rule7 % int2)) triple1) -> (rule3 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The cow eats the cat.
("cow" "eats" "cat" "+")
int2
The cow chases the cat.
("cow" "chases" "cat" "+")
((((triple2) -> (rule2 % int4)) ((((triple1) -> (rule7 % int3)) triple1) -> (rule3 % int2))) -> (rule5 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int2
The cow eats the cat.
("cow" "eats" "cat" "+")
int3
The cow is young.
("cow" "is" "young" "+")
int4