The cat eats the cow. The cat is nice. The cat sees the cow. The cow sees the lion. The lion eats the cow. The lion is not young. The lion sees the cow. If someone eats the cow and they see the cow then the cow does not visit the lion. If someone sees the cow and the cow is nice then the cow is young. If someone visits the cow and they are not cold then they do not eat the cat. If the cow does not see the lion and the cow is not rough then the cow does not eat the lion. If someone eats the cow then the cow does not see the cat. If someone visits the cow and they are rough then they are nice. If someone eats the lion then the lion is not nice. If someone eats the cow and the cow does not see the cat then they are not big.
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion eats the cow.
("lion" "eats" "cow" "+")
The lion is not young.
("lion" "is" "young" "-")
The lion sees the cow.
("lion" "sees" "cow" "+")
If someone eats the cow and they see the cow then the cow does not visit the lion.
((("someone" "eats" "cow" "+") ("someone" "sees" "cow" "+")) -> ("cow" "visits" "lion" "-"))
If someone sees the cow and the cow is nice then the cow is young.
((("someone" "sees" "cow" "+") ("cow" "is" "nice" "+")) -> ("cow" "is" "young" "+"))
If someone visits the cow and they are not cold then they do not eat the cat.
((("someone" "visits" "cow" "+") ("someone" "is" "cold" "~")) -> ("someone" "eats" "cat" "-"))
If the cow does not see the lion and the cow is not rough then the cow does not eat the lion.
((("cow" "sees" "lion" "~") ("cow" "is" "rough" "~")) -> ("cow" "eats" "lion" "-"))
If someone eats the cow then the cow does not see the cat.
((("someone" "eats" "cow" "+")) -> ("cow" "sees" "cat" "-"))
If someone visits the cow and they are rough then they are nice.
((("someone" "visits" "cow" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If someone eats the lion then the lion is not nice.
((("someone" "eats" "lion" "+")) -> ("lion" "is" "nice" "-"))
If someone eats the cow and the cow does not see the cat then they are not big.
((("someone" "eats" "cow" "+") ("cow" "sees" "cat" "~")) -> ("someone" "is" "big" "-"))
The lion sees the cow.
True
1
proof
[(triple7)]
("lion" "sees" "cow" "+")
triple7
The cat does not eat the cow.
False
1
inv-proof
[(triple1)]
("cat" "eats" "cow" "-")
triple1
The cow does not see the cat.
True
2
proof
[(((triple1) -> rule5) OR ((triple5) -> rule5))]
("cow" "sees" "cat" "-")
((triple1) -> (rule5 % int1))
The cow does not see the cat.
("cow" "sees" "cat" "-")
int1
((triple5) -> (rule5 % int1))
The cow does not see the cat.
("cow" "sees" "cat" "-")
int1
The cow sees the cat.
False
2
inv-proof
[(((triple1) -> rule5) OR ((triple5) -> rule5))]
("cow" "sees" "cat" "+")
((triple1) -> (rule5 % int1))
The cow does not see the cat.
("cow" "sees" "cat" "-")
int1
((triple5) -> (rule5 % int1))
The cow does not see the cat.
("cow" "sees" "cat" "-")
int1
The cow is not nice.
Unknown
inv-rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "is" "nice" "-")
The cow is young.
Unknown
rconc
[@2: The cow is young.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("cow" "is" "young" "+")
The cat does not eat the lion.
Unknown
inv-random
[@0: The cat eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "lion" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
@0: The cat eats the cow.[(triple1)] The cat is nice.[(triple2)] The cat sees the cow.[(triple3)] The cow sees the lion.[(triple4)] The lion eats the cow.[(triple5)] The lion is not young.[(triple6)] The lion sees the cow.[(triple7)] @1: The cow does not see the cat.[(((triple1) -> rule5) OR ((triple5) -> rule5))] The cow does not visit the lion.[(((triple1 triple3) -> rule1) OR ((triple5 triple7) -> rule1))] @2: The cat is not big.[(((triple1 ((triple1) -> rule5)) -> rule8) OR ((triple1 ((triple5) -> rule5)) -> rule8))] The lion is not big.[(((triple5 ((triple1) -> rule5)) -> rule8) OR ((triple5 ((triple5) -> rule5)) -> rule8))]
The cat eats the cow.
("cat" "eats" "cow" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat sees the cow.
("cat" "sees" "cow" "+")
triple3
The cow sees the lion.
("cow" "sees" "lion" "+")
triple4
The lion eats the cow.
("lion" "eats" "cow" "+")
triple5
The lion is not young.
("lion" "is" "young" "-")
triple6
The lion sees the cow.
("lion" "sees" "cow" "+")
triple7
The cow does not see the cat.
("cow" "sees" "cat" "-")
((triple1) -> (rule5 % int1))
The cow does not see the cat.
("cow" "sees" "cat" "-")
int1
((triple5) -> (rule5 % int1))
The cow does not see the cat.
("cow" "sees" "cat" "-")
int1
The cow does not visit the lion.
("cow" "visits" "lion" "-")
((triple1 triple3) -> (rule1 % int1))
The cow does not visit the lion.
("cow" "visits" "lion" "-")
int1
((triple5 triple7) -> (rule1 % int1))
The cow does not visit the lion.
("cow" "visits" "lion" "-")
int1
The cat is not big.
("cat" "is" "big" "-")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule8 % int1))
The cat is not big.
("cat" "is" "big" "-")
int1
The cow does not see the cat.
("cow" "sees" "cat" "-")
int2
((triple1 ((triple5) -> (rule5 % int2))) -> (rule8 % int1))
The cat is not big.
("cat" "is" "big" "-")
int1
The cow does not see the cat.
("cow" "sees" "cat" "-")
int2
The lion is not big.
("lion" "is" "big" "-")
((triple5 ((triple1) -> (rule5 % int2))) -> (rule8 % int1))
The lion is not big.
("lion" "is" "big" "-")
int1
The cow does not see the cat.
("cow" "sees" "cat" "-")
int2
((triple5 ((triple5) -> (rule5 % int2))) -> (rule8 % int1))
The lion is not big.
("lion" "is" "big" "-")
int1
The cow does not see the cat.
("cow" "sees" "cat" "-")
int2