The lion is big. The lion is nice. The lion needs the mouse. The lion visits the squirrel. The mouse is not rough. The mouse sees the lion. The mouse sees the squirrel. The mouse sees the tiger. The mouse visits the squirrel. The squirrel is nice. The squirrel is not rough. The squirrel does not see the mouse. The squirrel visits the tiger. The tiger is big. The tiger is green. The tiger is nice. If something visits the mouse and the mouse is big then the mouse needs the tiger. If the squirrel sees the mouse then the mouse needs the tiger. If the mouse sees the squirrel and the squirrel visits the lion then the squirrel is big. If something visits the lion then it does not see the squirrel. If something needs the lion then it is nice. If the lion visits the mouse then the lion is green. If something is nice then it sees the tiger. If something sees the tiger and the tiger is green then the tiger visits the lion.
The lion is big.
("lion" "is" "big" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The mouse is not rough.
("mouse" "is" "rough" "-")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is not rough.
("squirrel" "is" "rough" "-")
The squirrel does not see the mouse.
("squirrel" "sees" "mouse" "-")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
If something visits the mouse and the mouse is big then the mouse needs the tiger.
((("something" "visits" "mouse" "+") ("mouse" "is" "big" "+")) -> ("mouse" "needs" "tiger" "+"))
If the squirrel sees the mouse then the mouse needs the tiger.
((("squirrel" "sees" "mouse" "+")) -> ("mouse" "needs" "tiger" "+"))
If the mouse sees the squirrel and the squirrel visits the lion then the squirrel is big.
((("mouse" "sees" "squirrel" "+") ("squirrel" "visits" "lion" "+")) -> ("squirrel" "is" "big" "+"))
If something visits the lion then it does not see the squirrel.
((("something" "visits" "lion" "+")) -> ("something" "sees" "squirrel" "-"))
If something needs the lion then it is nice.
((("something" "needs" "lion" "+")) -> ("something" "is" "nice" "+"))
If the lion visits the mouse then the lion is green.
((("lion" "visits" "mouse" "+")) -> ("lion" "is" "green" "+"))
If something is nice then it sees the tiger.
((("something" "is" "nice" "+")) -> ("something" "sees" "tiger" "+"))
If something sees the tiger and the tiger is green then the tiger visits the lion.
((("something" "sees" "tiger" "+") ("tiger" "is" "green" "+")) -> ("tiger" "visits" "lion" "+"))
The squirrel is not rough.
True
1
proof
[(triple11)]
("squirrel" "is" "rough" "-")
triple11
The lion does not visit the squirrel.
False
1
inv-proof
[(triple4)]
("lion" "visits" "squirrel" "-")
triple4
The mouse does not need the tiger.
Unknown
inv-rconc
[@1: The mouse needs the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "needs" "tiger" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
@0: The lion is big.[(triple1)] The lion is nice.[(triple2)] The lion needs the mouse.[(triple3)] The lion visits the squirrel.[(triple4)] The mouse is not rough.[(triple5)] The mouse sees the lion.[(triple6)] The mouse sees the squirrel.[(triple7)] The mouse sees the tiger.[(triple8)] The mouse visits the squirrel.[(triple9)] The squirrel does not see the mouse.[(triple12)] The squirrel is nice.[(triple10)] The squirrel is not rough.[(triple11)] The squirrel visits the tiger.[(triple13)] The tiger is big.[(triple14)] The tiger is green.[(triple15)] The tiger is nice.[(triple16)] @1: The lion sees the tiger.[(((triple2) -> rule7))] The squirrel sees the tiger.[(((triple10) -> rule7))] The tiger sees the tiger.[(((triple16) -> rule7))] The tiger visits the lion.[(((triple8 triple15) -> rule8) OR ((((triple10) -> rule7) triple15) -> rule8) OR ((((triple16) -> rule7) triple15) -> rule8) OR ((((triple2) -> rule7) triple15) -> rule8))] @2: The tiger does not see the squirrel.[(((((triple8 triple15) -> rule8)) -> rule4) OR ((((((triple10) -> rule7) triple15) -> rule8)) -> rule4) OR ((((((triple16) -> rule7) triple15) -> rule8)) -> rule4) OR ((((((triple2) -> rule7) triple15) -> rule8)) -> rule4))]
The lion is big.
("lion" "is" "big" "+")
triple1
The lion is nice.
("lion" "is" "nice" "+")
triple2
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple3
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple4
The mouse is not rough.
("mouse" "is" "rough" "-")
triple5
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple6
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple7
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple8
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple9
The squirrel does not see the mouse.
("squirrel" "sees" "mouse" "-")
triple12
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple10
The squirrel is not rough.
("squirrel" "is" "rough" "-")
triple11
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple13
The tiger is big.
("tiger" "is" "big" "+")
triple14
The tiger is green.
("tiger" "is" "green" "+")
triple15
The tiger is nice.
("tiger" "is" "nice" "+")
triple16
The lion sees the tiger.
("lion" "sees" "tiger" "+")
((triple2) -> (rule7 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
((triple10) -> (rule7 % int1))
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((triple16) -> (rule7 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
((triple8 triple15) -> (rule8 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
((((triple10) -> (rule7 % int2)) triple15) -> (rule8 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int2
((((triple16) -> (rule7 % int2)) triple15) -> (rule8 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int2
((((triple2) -> (rule7 % int2)) triple15) -> (rule8 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The tiger does not see the squirrel.
("tiger" "sees" "squirrel" "-")
((((triple8 triple15) -> (rule8 % int2))) -> (rule4 % int1))
The tiger does not see the squirrel.
("tiger" "sees" "squirrel" "-")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int2
((((((triple10) -> (rule7 % int3)) triple15) -> (rule8 % int2))) -> (rule4 % int1))
The tiger does not see the squirrel.
("tiger" "sees" "squirrel" "-")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int2
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int3
((((((triple16) -> (rule7 % int3)) triple15) -> (rule8 % int2))) -> (rule4 % int1))
The tiger does not see the squirrel.
("tiger" "sees" "squirrel" "-")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int2
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int3
((((((triple2) -> (rule7 % int3)) triple15) -> (rule8 % int2))) -> (rule4 % int1))
The tiger does not see the squirrel.
("tiger" "sees" "squirrel" "-")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3