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