The cat does not eat the cow. The cow is round. The cow likes the cat. The cow likes the tiger. The cow sees the cat. The tiger eats the cow. The tiger is big. The tiger is round. The tiger is not young. The tiger likes the cat. The tiger likes the cow. The tiger sees the cat. If someone eats the cow then the cow sees the tiger. If someone likes the tiger and they are big then the tiger sees the cow. If the tiger does not like the cat then the tiger is round. If someone eats the cow then they see the cat. If someone is kind then they do not eat the tiger. If someone is green and they like the tiger then they do not eat the cow. If the tiger eats the cat and the cat does not like the tiger then the cat does not like the cow. If the cow eats the cat then the cow is young.
The cat does not eat the cow.
("cat" "eats" "cow" "-")
The cow is round.
("cow" "is" "round" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger is not young.
("tiger" "is" "young" "-")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If someone eats the cow then the cow sees the tiger.
((("someone" "eats" "cow" "+")) -> ("cow" "sees" "tiger" "+"))
If someone likes the tiger and they are big then the tiger sees the cow.
((("someone" "likes" "tiger" "+") ("someone" "is" "big" "+")) -> ("tiger" "sees" "cow" "+"))
If the tiger does not like the cat then the tiger is round.
((("tiger" "likes" "cat" "~")) -> ("tiger" "is" "round" "+"))
If someone eats the cow then they see the cat.
((("someone" "eats" "cow" "+")) -> ("someone" "sees" "cat" "+"))
If someone is kind then they do not eat the tiger.
((("someone" "is" "kind" "+")) -> ("someone" "eats" "tiger" "-"))
If someone is green and they like the tiger then they do not eat the cow.
((("someone" "is" "green" "+") ("someone" "likes" "tiger" "+")) -> ("someone" "eats" "cow" "-"))
If the tiger eats the cat and the cat does not like the tiger then the cat does not like the cow.
((("tiger" "eats" "cat" "+") ("cat" "likes" "tiger" "~")) -> ("cat" "likes" "cow" "-"))
If the cow eats the cat then the cow is young.
((("cow" "eats" "cat" "+")) -> ("cow" "is" "young" "+"))
The tiger is not young.
True
1
proof
[(triple9)]
("tiger" "is" "young" "-")
triple9
The tiger does not eat the cow.
False
1
inv-proof
[(triple6)]
("tiger" "eats" "cow" "-")
triple6
The cow sees the tiger.
True
2
proof
[(((triple6) -> rule1))]
("cow" "sees" "tiger" "+")
((triple6) -> (rule1 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The cow does not see the tiger.
False
2
inv-proof
[(((triple6) -> rule1))]
("cow" "sees" "tiger" "-")
((triple6) -> (rule1 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The cat does not see the cat.
Unknown
inv-rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "sees" "cat" "-")
The cow is young.
Unknown
rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "is" "young" "+")
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The cat sees the cow.
Unknown
random
[@0: The cat sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cow" "+")
@0: The cat does not eat the cow.[(triple1)] The cow is round.[(triple2)] The cow likes the cat.[(triple3)] The cow likes the tiger.[(triple4)] The cow sees the cat.[(triple5)] The tiger eats the cow.[(triple6)] The tiger is big.[(triple7)] The tiger is not young.[(triple9)] The tiger is round.[(triple8)] The tiger likes the cat.[(triple10)] The tiger likes the cow.[(triple11)] The tiger sees the cat.[(triple12 OR ((triple6) -> rule4))] @1: The cow sees the tiger.[(((triple6) -> rule1))]
The cat does not eat the cow.
("cat" "eats" "cow" "-")
triple1
The cow is round.
("cow" "is" "round" "+")
triple2
The cow likes the cat.
("cow" "likes" "cat" "+")
triple3
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple4
The cow sees the cat.
("cow" "sees" "cat" "+")
triple5
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple6
The tiger is big.
("tiger" "is" "big" "+")
triple7
The tiger is not young.
("tiger" "is" "young" "-")
triple9
The tiger is round.
("tiger" "is" "round" "+")
triple8
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple10
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple11
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple12
((triple6) -> (rule4 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
((triple6) -> (rule1 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1