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