The cat is green. The cat is nice. The cat is round. The cat sees the mouse. The cow is round. The cow visits the cat. The mouse is green. The mouse is round. The mouse needs the rabbit. The mouse sees the rabbit. The rabbit sees the cow. The rabbit visits the cow. If someone is green and they visit the rabbit then they are blue. If someone is nice and they visit the mouse then they need the cat. If someone needs the cat and they visit the cat then the cat sees the mouse. If someone visits the rabbit then they are blue. If someone sees the mouse then the mouse needs the rabbit. If someone sees the mouse then they see the cow. If someone is round and green then they visit the rabbit. If someone is round and they see the cat then the cat sees the rabbit.
The cat is green.
("cat" "is" "green" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is round.
("cat" "is" "round" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The cow is round.
("cow" "is" "round" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
If someone is green and they visit the rabbit then they are blue.
((("someone" "is" "green" "+") ("someone" "visits" "rabbit" "+")) -> ("someone" "is" "blue" "+"))
If someone is nice and they visit the mouse then they need the cat.
((("someone" "is" "nice" "+") ("someone" "visits" "mouse" "+")) -> ("someone" "needs" "cat" "+"))
If someone needs the cat and they visit the cat then the cat sees the mouse.
((("someone" "needs" "cat" "+") ("someone" "visits" "cat" "+")) -> ("cat" "sees" "mouse" "+"))
If someone visits the rabbit then they are blue.
((("someone" "visits" "rabbit" "+")) -> ("someone" "is" "blue" "+"))
If someone sees the mouse then the mouse needs the rabbit.
((("someone" "sees" "mouse" "+")) -> ("mouse" "needs" "rabbit" "+"))
If someone sees the mouse then they see the cow.
((("someone" "sees" "mouse" "+")) -> ("someone" "sees" "cow" "+"))
If someone is round and green then they visit the rabbit.
((("someone" "is" "round" "+") ("someone" "is" "green" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone is round and they see the cat then the cat sees the rabbit.
((("someone" "is" "round" "+") ("someone" "sees" "cat" "+")) -> ("cat" "sees" "rabbit" "+"))
The rabbit visits the cow.
True
1
proof
[(triple12)]
("rabbit" "visits" "cow" "+")
triple12
The cat does not see the mouse.
False
1
inv-proof
[(triple4)]
("cat" "sees" "mouse" "-")
triple4
The mouse visits the rabbit.
True
3
proof
[(((triple8 triple7) -> rule7))]
("mouse" "visits" "rabbit" "+")
((triple8 triple7) -> (rule7 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
The cat does not see the cow.
False
2
inv-proof
[(((triple4) -> rule6))]
("cat" "sees" "cow" "-")
((triple4) -> (rule6 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The cat is blue.
True
4
proof
[(((((triple3 triple1) -> rule7)) -> rule4) OR ((triple1 ((triple3 triple1) -> rule7)) -> rule1))]
("cat" "is" "blue" "+")
((((triple3 triple1) -> (rule7 % int2))) -> (rule4 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
((triple1 ((triple3 triple1) -> (rule7 % int2))) -> (rule1 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The cat is not blue.
False
4
inv-proof
[(((((triple3 triple1) -> rule7)) -> rule4) OR ((triple1 ((triple3 triple1) -> rule7)) -> rule1))]
("cat" "is" "blue" "-")
((((triple3 triple1) -> (rule7 % int2))) -> (rule4 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
((triple1 ((triple3 triple1) -> (rule7 % int2))) -> (rule1 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The rabbit does not need the cat.
Unknown
inv-rconc
[@1: The rabbit needs the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "needs" "cat" "-")
The cow visits the rabbit.
Unknown
rconc
[@1: The cow visits the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "visits" "rabbit" "+")
The rabbit is not blue.
Unknown
inv-rconc
[@2: The rabbit is blue.[CWA. Example of deepest failure = (rule4 <- rule7 <- FAIL)]]
("rabbit" "is" "blue" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
The rabbit does not visit the cat.
Unknown
inv-random
[@0: The rabbit visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "cat" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
@0: The cat is green.[(triple1)] The cat is nice.[(triple2)] The cat is round.[(triple3)] The cat sees the mouse.[(triple4)] The cow is round.[(triple5)] The cow visits the cat.[(triple6)] The mouse is green.[(triple7)] The mouse is round.[(triple8)] The mouse needs the rabbit.[(triple9 OR ((triple4) -> rule5))] The mouse sees the rabbit.[(triple10)] The rabbit sees the cow.[(triple11)] The rabbit visits the cow.[(triple12)] @1: The cat sees the cow.[(((triple4) -> rule6))] The cat visits the rabbit.[(((triple3 triple1) -> rule7))] The mouse visits the rabbit.[(((triple8 triple7) -> rule7))] @2: The cat is blue.[(((((triple3 triple1) -> rule7)) -> rule4) OR ((triple1 ((triple3 triple1) -> rule7)) -> rule1))] The mouse is blue.[(((((triple8 triple7) -> rule7)) -> rule4) OR ((triple7 ((triple8 triple7) -> rule7)) -> rule1))]
The cat is green.
("cat" "is" "green" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat is round.
("cat" "is" "round" "+")
triple3
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple4
The cow is round.
("cow" "is" "round" "+")
triple5
The cow visits the cat.
("cow" "visits" "cat" "+")
triple6
The mouse is green.
("mouse" "is" "green" "+")
triple7
The mouse is round.
("mouse" "is" "round" "+")
triple8
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple9
((triple4) -> (rule5 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple10
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple11
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple12
The cat sees the cow.
("cat" "sees" "cow" "+")
((triple4) -> (rule6 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
((triple3 triple1) -> (rule7 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
((triple8 triple7) -> (rule7 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
((((triple3 triple1) -> (rule7 % int2))) -> (rule4 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
((triple1 ((triple3 triple1) -> (rule7 % int2))) -> (rule1 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
((((triple8 triple7) -> (rule7 % int2))) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int2
((triple7 ((triple8 triple7) -> (rule7 % int2))) -> (rule1 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int2