The lion chases the mouse. The lion is cold. The lion is round. The lion needs the mouse. The lion needs the squirrel. The mouse is round. The mouse needs the lion. The mouse visits the lion. The mouse does not visit the squirrel. The squirrel does not chase the lion. The squirrel is big. The squirrel visits the lion. If something needs the mouse then the mouse chases the squirrel. If the mouse is kind and the squirrel does not chase the mouse then the mouse does not visit the squirrel. If something chases the squirrel then the squirrel is kind. If something is kind and it does not chase the lion then it is big. If something is big then it does not need the lion. If something chases the squirrel and it does not visit the mouse then the mouse is not round. If something is kind then it does not visit the squirrel. If something needs the lion and it chases the squirrel then it does not visit the squirrel.
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is round.
("lion" "is" "round" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
The mouse does not visit the squirrel.
("mouse" "visits" "squirrel" "-")
The squirrel does not chase the lion.
("squirrel" "chases" "lion" "-")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If something needs the mouse then the mouse chases the squirrel.
((("something" "needs" "mouse" "+")) -> ("mouse" "chases" "squirrel" "+"))
If the mouse is kind and the squirrel does not chase the mouse then the mouse does not visit the squirrel.
((("mouse" "is" "kind" "+") ("squirrel" "chases" "mouse" "~")) -> ("mouse" "visits" "squirrel" "-"))
If something chases the squirrel then the squirrel is kind.
((("something" "chases" "squirrel" "+")) -> ("squirrel" "is" "kind" "+"))
If something is kind and it does not chase the lion then it is big.
((("something" "is" "kind" "+") ("something" "chases" "lion" "~")) -> ("something" "is" "big" "+"))
If something is big then it does not need the lion.
((("something" "is" "big" "+")) -> ("something" "needs" "lion" "-"))
If something chases the squirrel and it does not visit the mouse then the mouse is not round.
((("something" "chases" "squirrel" "+") ("something" "visits" "mouse" "~")) -> ("mouse" "is" "round" "-"))
If something is kind then it does not visit the squirrel.
((("something" "is" "kind" "+")) -> ("something" "visits" "squirrel" "-"))
If something needs the lion and it chases the squirrel then it does not visit the squirrel.
((("something" "needs" "lion" "+") ("something" "chases" "squirrel" "+")) -> ("something" "visits" "squirrel" "-"))
The lion chases the mouse.
True
1
proof
[(triple1)]
("lion" "chases" "mouse" "+")
triple1
The lion does not need the squirrel.
False
1
inv-proof
[(triple5)]
("lion" "needs" "squirrel" "-")
triple5
The squirrel does not need the lion.
True
2
proof
[(((triple11) -> rule5) OR ((((((((triple4) -> rule1)) -> rule3) triple10) -> rule4)) -> rule5))]
("squirrel" "needs" "lion" "-")
((triple11) -> (rule5 % int1))
The squirrel does not need the lion.
("squirrel" "needs" "lion" "-")
int1
((((((((triple4) -> (rule1 % int4))) -> (rule3 % int3)) triple10) -> (rule4 % int2))) -> (rule5 % int1))
The squirrel does not need the lion.
("squirrel" "needs" "lion" "-")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
int3
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int4
The mouse does not chase the squirrel.
False
2
inv-proof
[(((triple4) -> rule1))]
("mouse" "chases" "squirrel" "-")
((triple4) -> (rule1 % int1))
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int1
The squirrel is kind.
True
3
proof
[(((((triple4) -> rule1)) -> rule3))]
("squirrel" "is" "kind" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int2
The squirrel is not kind.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule3))]
("squirrel" "is" "kind" "-")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int2
The squirrel does not visit the squirrel.
True
4
proof
[(((((((triple4) -> rule1)) -> rule3)) -> rule7))]
("squirrel" "visits" "squirrel" "-")
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The squirrel does not visit the squirrel.
("squirrel" "visits" "squirrel" "-")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int3
The squirrel visits the squirrel.
False
4
inv-proof
[(((((((triple4) -> rule1)) -> rule3)) -> rule7))]
("squirrel" "visits" "squirrel" "+")
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The squirrel does not visit the squirrel.
("squirrel" "visits" "squirrel" "-")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int3
The lion is not big.
Unknown
inv-rconc
[@1: The lion is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "big" "-")
The mouse is big.
Unknown
rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "big" "+")
The squirrel is not round.
Unknown
inv-random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
The mouse does not chase the lion.
Unknown
inv-random
[@0: The mouse chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "lion" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
The mouse is not blue.
Unknown
inv-random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "-")
The squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
@0: The lion chases the mouse.[(triple1)] The lion is cold.[(triple2)] The lion is round.[(triple3)] The lion needs the mouse.[(triple4)] The lion needs the squirrel.[(triple5)] The mouse does not visit the squirrel.[(triple9 OR ((triple7 ((triple4) -> rule1)) -> rule8))] The mouse is round.[(triple6)] The mouse needs the lion.[(triple7)] The mouse visits the lion.[(triple8)] The squirrel does not chase the lion.[(triple10)] The squirrel is big.[(triple11 OR ((((((triple4) -> rule1)) -> rule3) triple10) -> rule4))] The squirrel visits the lion.[(triple12)] @1: The mouse chases the squirrel.[(((triple4) -> rule1))] The squirrel does not need the lion.[(((triple11) -> rule5) OR ((((((((triple4) -> rule1)) -> rule3) triple10) -> rule4)) -> rule5))] @2: The squirrel is kind.[(((((triple4) -> rule1)) -> rule3))] @3: The squirrel does not visit the squirrel.[(((((((triple4) -> rule1)) -> rule3)) -> rule7))]
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The lion is round.
("lion" "is" "round" "+")
triple3
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple4
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple5
The mouse does not visit the squirrel.
("mouse" "visits" "squirrel" "-")
triple9
((triple7 ((triple4) -> (rule1 % int2))) -> (rule8 % int1))
The mouse does not visit the squirrel.
("mouse" "visits" "squirrel" "-")
int1
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int2
The mouse is round.
("mouse" "is" "round" "+")
triple6
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple7
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple8
The squirrel does not chase the lion.
("squirrel" "chases" "lion" "-")
triple10
The squirrel is big.
("squirrel" "is" "big" "+")
triple11
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2)) triple10) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int3
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple12
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
((triple4) -> (rule1 % int1))
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int1
The squirrel does not need the lion.
("squirrel" "needs" "lion" "-")
((triple11) -> (rule5 % int1))
The squirrel does not need the lion.
("squirrel" "needs" "lion" "-")
int1
((((((((triple4) -> (rule1 % int4))) -> (rule3 % int3)) triple10) -> (rule4 % int2))) -> (rule5 % int1))
The squirrel does not need the lion.
("squirrel" "needs" "lion" "-")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
int3
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int4
The squirrel is kind.
("squirrel" "is" "kind" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int2
The squirrel does not visit the squirrel.
("squirrel" "visits" "squirrel" "-")
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The squirrel does not visit the squirrel.
("squirrel" "visits" "squirrel" "-")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
int3