The cat chases the cow. The cat chases the rabbit. The cat is young. The cat likes the rabbit. The cat does not see the rabbit. The cow is big. The cow is nice. The cow sees the rabbit. The rabbit is nice. The rabbit sees the cat. If something is kind then it sees the cow. If something sees the rabbit then the rabbit is big. If something is big and it does not like the cat then the cat sees the rabbit. If something likes the cow then it chases the cat. Big things are young. If something chases the cat and the cat does not see the rabbit then the cat does not chase the rabbit.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The cat does not see the rabbit.
("cat" "sees" "rabbit" "-")
The cow is big.
("cow" "is" "big" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
If something is kind then it sees the cow.
((("something" "is" "kind" "+")) -> ("something" "sees" "cow" "+"))
If something sees the rabbit then the rabbit is big.
((("something" "sees" "rabbit" "+")) -> ("rabbit" "is" "big" "+"))
If something is big and it does not like the cat then the cat sees the rabbit.
((("something" "is" "big" "+") ("something" "likes" "cat" "~")) -> ("cat" "sees" "rabbit" "+"))
If something likes the cow then it chases the cat.
((("something" "likes" "cow" "+")) -> ("something" "chases" "cat" "+"))
Big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If something chases the cat and the cat does not see the rabbit then the cat does not chase the rabbit.
((("something" "chases" "cat" "+") ("cat" "sees" "rabbit" "~")) -> ("cat" "chases" "rabbit" "-"))
The cow is nice.
True
1
proof
[(triple7)]
("cow" "is" "nice" "+")
triple7
The cow is not nice.
False
1
inv-proof
[(triple7)]
("cow" "is" "nice" "-")
triple7
The rabbit is big.
True
2
proof
[(((triple8) -> rule2))]
("rabbit" "is" "big" "+")
((triple8) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is not big.
False
2
inv-proof
[(((triple8) -> rule2))]
("rabbit" "is" "big" "-")
((triple8) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is young.
True
3
proof
[(((((triple8) -> rule2)) -> rule5))]
("rabbit" "is" "young" "+")
((((triple8) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is not young.
False
3
inv-proof
[(((((triple8) -> rule2)) -> rule5))]
("rabbit" "is" "young" "-")
((((triple8) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit does not chase the cat.
Unknown
inv-rconc
[@1: The rabbit chases the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "chases" "cat" "-")
The cow chases the cat.
Unknown
rconc
[@1: The cow chases the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "chases" "cat" "+")
The cow does not see the cow.
Unknown
inv-rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "sees" "cow" "-")
The rabbit chases the cow.
Unknown
random
[@0: The rabbit chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "cow" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
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 chases the cow.[(triple1)] The cat chases the rabbit.[(triple2)] The cat does not see the rabbit.[(triple5)] The cat is young.[(triple3)] The cat likes the rabbit.[(triple4)] The cow is big.[(triple6)] The cow is nice.[(triple7)] The cow sees the rabbit.[(triple8)] The rabbit is nice.[(triple9)] The rabbit sees the cat.[(triple10)] @1: The cow is young.[(((triple6) -> rule5))] The rabbit is big.[(((triple8) -> rule2))] @2: The rabbit is young.[(((((triple8) -> rule2)) -> rule5))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple2
The cat does not see the rabbit.
("cat" "sees" "rabbit" "-")
triple5
The cat is young.
("cat" "is" "young" "+")
triple3
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple4
The cow is big.
("cow" "is" "big" "+")
triple6
The cow is nice.
("cow" "is" "nice" "+")
triple7
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple8
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple9
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple10
The cow is young.
("cow" "is" "young" "+")
((triple6) -> (rule5 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
((triple8) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
((((triple8) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2