The cow chases the mouse. The cow visits the squirrel. The lion chases the mouse. The lion is blue. The lion is kind. The lion visits the mouse. The mouse chases the lion. The mouse visits the cow. The squirrel chases the cow. The squirrel chases the mouse. The squirrel is blue. The squirrel is nice. If the mouse sees the squirrel and the mouse chases the squirrel then the squirrel is blue. If the mouse visits the lion then the mouse visits the cow. If someone chases the cow then the cow is kind. All blue people are big. If someone sees the squirrel then they visit the mouse. If someone is kind and they chase the mouse then the mouse sees the squirrel.
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
If the mouse sees the squirrel and the mouse chases the squirrel then the squirrel is blue.
((("mouse" "sees" "squirrel" "+") ("mouse" "chases" "squirrel" "+")) -> ("squirrel" "is" "blue" "+"))
If the mouse visits the lion then the mouse visits the cow.
((("mouse" "visits" "lion" "+")) -> ("mouse" "visits" "cow" "+"))
If someone chases the cow then the cow is kind.
((("someone" "chases" "cow" "+")) -> ("cow" "is" "kind" "+"))
All blue people are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
If someone sees the squirrel then they visit the mouse.
((("someone" "sees" "squirrel" "+")) -> ("someone" "visits" "mouse" "+"))
If someone is kind and they chase the mouse then the mouse sees the squirrel.
((("someone" "is" "kind" "+") ("someone" "chases" "mouse" "+")) -> ("mouse" "sees" "squirrel" "+"))
The squirrel chases the cow.
True
1
proof
[(triple9)]
("squirrel" "chases" "cow" "+")
triple9
The mouse does not visit the cow.
False
1
inv-proof
[(triple8)]
("mouse" "visits" "cow" "-")
triple8
The mouse sees the squirrel.
True
3
proof
[(((triple5 triple3) -> rule6) OR ((((triple9) -> rule3) triple1) -> rule6))]
("mouse" "sees" "squirrel" "+")
((triple5 triple3) -> (rule6 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
((((triple9) -> (rule3 % int2)) triple1) -> (rule6 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The cow is not kind.
False
2
inv-proof
[(((triple9) -> rule3))]
("cow" "is" "kind" "-")
((triple9) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The mouse visits the mouse.
True
4
proof
[(((((triple5 triple3) -> rule6)) -> rule5) OR ((((((triple9) -> rule3) triple1) -> rule6)) -> rule5))]
("mouse" "visits" "mouse" "+")
((((triple5 triple3) -> (rule6 % int2))) -> (rule5 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
((((((triple9) -> (rule3 % int3)) triple1) -> (rule6 % int2))) -> (rule5 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
The mouse does not visit the mouse.
False
4
inv-proof
[(((((triple5 triple3) -> rule6)) -> rule5) OR ((((((triple9) -> rule3) triple1) -> rule6)) -> rule5))]
("mouse" "visits" "mouse" "-")
((((triple5 triple3) -> (rule6 % int2))) -> (rule5 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
((((((triple9) -> (rule3 % int3)) triple1) -> (rule6 % int2))) -> (rule5 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3
The mouse is not big.
Unknown
inv-rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "big" "-")
The cow visits the mouse.
Unknown
rconc
[@1: The cow visits the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "visits" "mouse" "+")
The cow is not big.
Unknown
inv-rconc
[@1: The cow is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "is" "big" "-")
The lion chases the cow.
Unknown
random
[@0: The lion chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "cow" "+")
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
@0: The cow chases the mouse.[(triple1)] The cow visits the squirrel.[(triple2)] The lion chases the mouse.[(triple3)] The lion is blue.[(triple4)] The lion is kind.[(triple5)] The lion visits the mouse.[(triple6)] The mouse chases the lion.[(triple7)] The mouse visits the cow.[(triple8)] The squirrel chases the cow.[(triple9)] The squirrel chases the mouse.[(triple10)] The squirrel is blue.[(triple11)] The squirrel is nice.[(triple12)] @1: The cow is kind.[(((triple9) -> rule3))] The lion is big.[(((triple4) -> rule4))] The mouse sees the squirrel.[(((triple5 triple3) -> rule6) OR ((((triple9) -> rule3) triple1) -> rule6))] The squirrel is big.[(((triple11) -> rule4))] @2: The mouse visits the mouse.[(((((triple5 triple3) -> rule6)) -> rule5) OR ((((((triple9) -> rule3) triple1) -> rule6)) -> rule5))]
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
triple2
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple3
The lion is blue.
("lion" "is" "blue" "+")
triple4
The lion is kind.
("lion" "is" "kind" "+")
triple5
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple6
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple7
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple8
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
triple9
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
triple10
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple11
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple12
The cow is kind.
("cow" "is" "kind" "+")
((triple9) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The lion is big.
("lion" "is" "big" "+")
((triple4) -> (rule4 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
((triple5 triple3) -> (rule6 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
((((triple9) -> (rule3 % int2)) triple1) -> (rule6 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
((triple11) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((((triple5 triple3) -> (rule6 % int2))) -> (rule5 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
((((((triple9) -> (rule3 % int3)) triple1) -> (rule6 % int2))) -> (rule5 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int2
The cow is kind.
("cow" "is" "kind" "+")
int3