The cat eats the rabbit. The cat sees the rabbit. The cat visits the rabbit. The rabbit eats the cat. The rabbit is green. The rabbit is rough. The rabbit sees the cat. If something visits the rabbit then the rabbit sees the cat. If something visits the rabbit then the rabbit eats the cat. If something sees the cat then it eats the cat.
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
If something visits the rabbit then the rabbit sees the cat.
((("something" "visits" "rabbit" "+")) -> ("rabbit" "sees" "cat" "+"))
If something visits the rabbit then the rabbit eats the cat.
((("something" "visits" "rabbit" "+")) -> ("rabbit" "eats" "cat" "+"))
If something sees the cat then it eats the cat.
((("something" "sees" "cat" "+")) -> ("something" "eats" "cat" "+"))
The rabbit eats the cat.
True
1
proof
[(triple4 OR ((triple3) -> rule2) OR ((triple7) -> rule3) OR ((((triple3) -> rule1)) -> rule3))]
("rabbit" "eats" "cat" "+")
triple4
((triple3) -> (rule2 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
((triple7) -> (rule3 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The rabbit does not see the cat.
False
1
inv-proof
[(triple7 OR ((triple3) -> rule1))]
("rabbit" "sees" "cat" "-")
triple7
((triple3) -> (rule1 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The cat does not eat the cat.
Unknown
inv-rconc
[@1: The cat eats the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "eats" "cat" "-")
The rabbit visits the cat.
Unknown
random
[@0: The rabbit visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "cat" "+")
@0: The cat eats the rabbit.[(triple1)] The cat sees the rabbit.[(triple2)] The cat visits the rabbit.[(triple3)] The rabbit eats the cat.[(triple4 OR ((triple3) -> rule2) OR ((triple7) -> rule3) OR ((((triple3) -> rule1)) -> rule3))] The rabbit is green.[(triple5)] The rabbit is rough.[(triple6)] The rabbit sees the cat.[(triple7 OR ((triple3) -> rule1))]
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple1
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple2
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple3
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
triple4
((triple3) -> (rule2 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
((triple7) -> (rule3 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
triple5
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple6
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple7
((triple3) -> (rule1 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1