The cow chases the mouse. The cow is green. The lion chases the cow. The lion sees the cow. The mouse chases the cow. The mouse chases the lion. The mouse chases the rabbit. The mouse is kind. The mouse is round. The mouse sees the lion. The rabbit is blue. The rabbit is green. The rabbit is kind. The rabbit sees the mouse. The rabbit visits the lion. The rabbit visits the mouse. If something is kind then it visits the rabbit. If something chases the lion then it does not visit the mouse. If something sees the rabbit and it is green then the rabbit does not see the lion. If something chases the mouse then it does not visit the lion. If something chases the mouse and it sees the mouse then the mouse chases the lion. If something sees the rabbit then it is green. If something chases the cow and it does not visit the mouse then the cow is cold. If something is cold then it chases the rabbit.
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow is green.
("cow" "is" "green" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If something is kind then it visits the rabbit.
((("something" "is" "kind" "+")) -> ("something" "visits" "rabbit" "+"))
If something chases the lion then it does not visit the mouse.
((("something" "chases" "lion" "+")) -> ("something" "visits" "mouse" "-"))
If something sees the rabbit and it is green then the rabbit does not see the lion.
((("something" "sees" "rabbit" "+") ("something" "is" "green" "+")) -> ("rabbit" "sees" "lion" "-"))
If something chases the mouse then it does not visit the lion.
((("something" "chases" "mouse" "+")) -> ("something" "visits" "lion" "-"))
If something chases the mouse and it sees the mouse then the mouse chases the lion.
((("something" "chases" "mouse" "+") ("something" "sees" "mouse" "+")) -> ("mouse" "chases" "lion" "+"))
If something sees the rabbit then it is green.
((("something" "sees" "rabbit" "+")) -> ("something" "is" "green" "+"))
If something chases the cow and it does not visit the mouse then the cow is cold.
((("something" "chases" "cow" "+") ("something" "visits" "mouse" "~")) -> ("cow" "is" "cold" "+"))
If something is cold then it chases the rabbit.
((("something" "is" "cold" "+")) -> ("something" "chases" "rabbit" "+"))
The mouse chases the cow.
True
1
proof
[(triple5)]
("mouse" "chases" "cow" "+")
triple5
The lion does not see the cow.
False
1
inv-proof
[(triple4)]
("lion" "sees" "cow" "-")
triple4
The mouse does not visit the mouse.
True
2
proof
[(((triple6) -> rule2))]
("mouse" "visits" "mouse" "-")
((triple6) -> (rule2 % int1))
The mouse does not visit the mouse.
("mouse" "visits" "mouse" "-")
int1
The mouse visits the mouse.
False
2
inv-proof
[(((triple6) -> rule2))]
("mouse" "visits" "mouse" "+")
((triple6) -> (rule2 % int1))
The mouse does not visit the mouse.
("mouse" "visits" "mouse" "-")
int1
The cow is cold.
True
4
proof
[(((triple5 ((triple6) -> rule2)) -> rule7))]
("cow" "is" "cold" "+")
((triple5 ((triple6) -> (rule2 % int2))) -> (rule7 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The mouse does not visit the mouse.
("mouse" "visits" "mouse" "-")
int2
The cow is not cold.
False
4
inv-proof
[(((triple5 ((triple6) -> rule2)) -> rule7))]
("cow" "is" "cold" "-")
((triple5 ((triple6) -> (rule2 % int2))) -> (rule7 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The mouse does not visit the mouse.
("mouse" "visits" "mouse" "-")
int2
The cow chases the rabbit.
True
5
proof
[(((((triple5 ((triple6) -> rule2)) -> rule7)) -> rule8))]
("cow" "chases" "rabbit" "+")
((((triple5 ((triple6) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The mouse does not visit the mouse.
("mouse" "visits" "mouse" "-")
int3
The cow does not chase the rabbit.
False
5
inv-proof
[(((((triple5 ((triple6) -> rule2)) -> rule7)) -> rule8))]
("cow" "chases" "rabbit" "-")
((((triple5 ((triple6) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The mouse does not visit the mouse.
("mouse" "visits" "mouse" "-")
int3
The lion does not chase the rabbit.
Unknown
inv-rconc
[@1: The lion chases the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "chases" "rabbit" "-")
The lion visits the rabbit.
Unknown
rconc
[@1: The lion visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "visits" "rabbit" "+")
The mouse is not green.
Unknown
inv-rconc
[@1: The mouse is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "green" "-")
The cow visits the rabbit.
Unknown
rconc
[@1: The cow visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "visits" "rabbit" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The cow is round.
Unknown
random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "+")
The rabbit is not round.
Unknown
inv-random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "-")
The cow visits the mouse.
Unknown
random
[@0: The cow visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "mouse" "+")
@0: The cow chases the mouse.[(triple1)] The cow is green.[(triple2)] The lion chases the cow.[(triple3)] The lion sees the cow.[(triple4)] The mouse chases the cow.[(triple5)] The mouse chases the lion.[(triple6)] The mouse chases the rabbit.[(triple7)] The mouse is kind.[(triple8)] The mouse is round.[(triple9)] The mouse sees the lion.[(triple10)] The rabbit is blue.[(triple11)] The rabbit is green.[(triple12)] The rabbit is kind.[(triple13)] The rabbit sees the mouse.[(triple14)] The rabbit visits the lion.[(triple15)] The rabbit visits the mouse.[(triple16)] @1: The cow does not visit the lion.[(((triple1) -> rule4))] The mouse does not visit the mouse.[(((triple6) -> rule2))] The mouse visits the rabbit.[(((triple8) -> rule1))] The rabbit visits the rabbit.[(((triple13) -> rule1))] @2: The cow is cold.[(((triple5 ((triple6) -> rule2)) -> rule7))] @3: The cow chases the rabbit.[(((((triple5 ((triple6) -> rule2)) -> rule7)) -> rule8))]
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple1
The cow is green.
("cow" "is" "green" "+")
triple2
The lion chases the cow.
("lion" "chases" "cow" "+")
triple3
The lion sees the cow.
("lion" "sees" "cow" "+")
triple4
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple5
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple6
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple7
The mouse is kind.
("mouse" "is" "kind" "+")
triple8
The mouse is round.
("mouse" "is" "round" "+")
triple9
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple10
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple11
The rabbit is green.
("rabbit" "is" "green" "+")
triple12
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple13
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple14
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple15
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple16
The cow does not visit the lion.
("cow" "visits" "lion" "-")
((triple1) -> (rule4 % int1))
The cow does not visit the lion.
("cow" "visits" "lion" "-")
int1
The mouse does not visit the mouse.
("mouse" "visits" "mouse" "-")
((triple6) -> (rule2 % int1))
The mouse does not visit the mouse.
("mouse" "visits" "mouse" "-")
int1
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
((triple8) -> (rule1 % int1))
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple13) -> (rule1 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
((triple5 ((triple6) -> (rule2 % int2))) -> (rule7 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The mouse does not visit the mouse.
("mouse" "visits" "mouse" "-")
int2
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
((((triple5 ((triple6) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The mouse does not visit the mouse.
("mouse" "visits" "mouse" "-")
int3