The cat eats the cow. The cat eats the rabbit. The cat visits the rabbit. The cow is green. The cow visits the cat. The lion eats the cat. The lion eats the rabbit. The lion is big. The rabbit eats the cow. The rabbit sees the lion. If the lion eats the cat and the cat is rough then the lion sees the cow. If something is nice then it is big. If the cat eats the cow then the cat is rough.
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The cow is green.
("cow" "is" "green" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion is big.
("lion" "is" "big" "+")
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If the lion eats the cat and the cat is rough then the lion sees the cow.
((("lion" "eats" "cat" "+") ("cat" "is" "rough" "+")) -> ("lion" "sees" "cow" "+"))
If something is nice then it is big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If the cat eats the cow then the cat is rough.
((("cat" "eats" "cow" "+")) -> ("cat" "is" "rough" "+"))
The cat eats the cow.
True
1
proof
[(triple1)]
("cat" "eats" "cow" "+")
triple1
The cat does not eat the rabbit.
False
1
inv-proof
[(triple2)]
("cat" "eats" "rabbit" "-")
triple2
The rabbit is not big.
Unknown
inv-rconc
[@1: The rabbit is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "big" "-")
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 eats the cow.[(triple1)] The cat eats the rabbit.[(triple2)] The cat visits the rabbit.[(triple3)] The cow is green.[(triple4)] The cow visits the cat.[(triple5)] The lion eats the cat.[(triple6)] The lion eats the rabbit.[(triple7)] The lion is big.[(triple8)] The rabbit eats the cow.[(triple9)] The rabbit sees the lion.[(triple10)] @1: The cat is rough.[(((triple1) -> rule3))] @2: The lion sees the cow.[(((triple6 ((triple1) -> rule3)) -> rule1))]
The cat eats the cow.
("cat" "eats" "cow" "+")
triple1
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple2
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple3
The cow is green.
("cow" "is" "green" "+")
triple4
The cow visits the cat.
("cow" "visits" "cat" "+")
triple5
The lion eats the cat.
("lion" "eats" "cat" "+")
triple6
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple7
The lion is big.
("lion" "is" "big" "+")
triple8
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
triple9
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple10
The cat is rough.
("cat" "is" "rough" "+")
((triple1) -> (rule3 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
((triple6 ((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The cat is rough.
("cat" "is" "rough" "+")
int2