The cat eats the cow. The cat eats the lion. The cat is not kind. The cat visits the cow. The cow eats the cat. The cow eats the lion. The cow is not cold. The cow is not nice. The cow sees the cat. The cow sees the lion. The cow visits the cat. The lion eats the cat. The lion eats the cow. The lion is rough. The lion visits the cat. The lion visits the cow. If something visits the cow then it sees the cow. If something visits the cat then the cat is big. If something eats the cow and it is cold then it is rough. If something visits the cat then it is rough. If something eats the cow and the cow visits the lion then the cow does not see the cat. If something sees the cow and it is not big then it eats the cow.
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat is not kind.
("cat" "is" "kind" "-")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow eats the lion.
("cow" "eats" "lion" "+")
The cow is not cold.
("cow" "is" "cold" "-")
The cow is not nice.
("cow" "is" "nice" "-")
The cow sees the cat.
("cow" "sees" "cat" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion eats the cow.
("lion" "eats" "cow" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
If something visits the cow then it sees the cow.
((("something" "visits" "cow" "+")) -> ("something" "sees" "cow" "+"))
If something visits the cat then the cat is big.
((("something" "visits" "cat" "+")) -> ("cat" "is" "big" "+"))
If something eats the cow and it is cold then it is rough.
((("something" "eats" "cow" "+") ("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If something visits the cat then it is rough.
((("something" "visits" "cat" "+")) -> ("something" "is" "rough" "+"))
If something eats the cow and the cow visits the lion then the cow does not see the cat.
((("something" "eats" "cow" "+") ("cow" "visits" "lion" "+")) -> ("cow" "sees" "cat" "-"))
If something sees the cow and it is not big then it eats the cow.
((("something" "sees" "cow" "+") ("something" "is" "big" "~")) -> ("something" "eats" "cow" "+"))
The lion visits the cow.
True
1
proof
[(triple16)]
("lion" "visits" "cow" "+")
triple16
The cat does not eat the cow.
False
1
inv-proof
[(triple1)]
("cat" "eats" "cow" "-")
triple1
The cat sees the cow.
True
2
proof
[(((triple4) -> rule1))]
("cat" "sees" "cow" "+")
((triple4) -> (rule1 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The cow is not rough.
False
2
inv-proof
[(((triple11) -> rule4))]
("cow" "is" "rough" "-")
((triple11) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cat is not rough.
Unknown
inv-rconc
[@1: The cat is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "rough" "-")
The cow eats the cow.
Unknown
rconc
[@1: The cow eats the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "eats" "cow" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The lion is cold.
Unknown
random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "+")
@0: The cat eats the cow.[(triple1)] The cat eats the lion.[(triple2)] The cat is not kind.[(triple3)] The cat visits the cow.[(triple4)] The cow eats the cat.[(triple5)] The cow eats the lion.[(triple6)] The cow is not cold.[(triple7)] The cow is not nice.[(triple8)] The cow sees the cat.[(triple9)] The cow sees the lion.[(triple10)] The cow visits the cat.[(triple11)] The lion eats the cat.[(triple12)] The lion eats the cow.[(triple13)] The lion is rough.[(triple14 OR ((triple15) -> rule4))] The lion visits the cat.[(triple15)] The lion visits the cow.[(triple16)] @1: The cat is big.[(((triple11) -> rule2) OR ((triple15) -> rule2))] The cat sees the cow.[(((triple4) -> rule1))] The cow is rough.[(((triple11) -> rule4))] The lion sees the cow.[(((triple16) -> rule1))]
The cat eats the cow.
("cat" "eats" "cow" "+")
triple1
The cat eats the lion.
("cat" "eats" "lion" "+")
triple2
The cat is not kind.
("cat" "is" "kind" "-")
triple3
The cat visits the cow.
("cat" "visits" "cow" "+")
triple4
The cow eats the cat.
("cow" "eats" "cat" "+")
triple5
The cow eats the lion.
("cow" "eats" "lion" "+")
triple6
The cow is not cold.
("cow" "is" "cold" "-")
triple7
The cow is not nice.
("cow" "is" "nice" "-")
triple8
The cow sees the cat.
("cow" "sees" "cat" "+")
triple9
The cow sees the lion.
("cow" "sees" "lion" "+")
triple10
The cow visits the cat.
("cow" "visits" "cat" "+")
triple11
The lion eats the cat.
("lion" "eats" "cat" "+")
triple12
The lion eats the cow.
("lion" "eats" "cow" "+")
triple13
The lion is rough.
("lion" "is" "rough" "+")
triple14
((triple15) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
triple15
The lion visits the cow.
("lion" "visits" "cow" "+")
triple16
The cat is big.
("cat" "is" "big" "+")
((triple11) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
((triple15) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat sees the cow.
("cat" "sees" "cow" "+")
((triple4) -> (rule1 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
((triple11) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
((triple16) -> (rule1 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1