The lion does not chase the mouse. The lion is blue. The lion is green. The lion is nice. The lion is not round. The lion is not young. The mouse chases the lion. The mouse is blue. The mouse is young. The squirrel chases the lion. The squirrel is round. The squirrel needs the mouse. The tiger chases the squirrel. The tiger is round. The tiger does not need the lion. The tiger needs the mouse. If something is round and it chases the squirrel then it does not eat the lion. If something needs the mouse and it is not round then the mouse does not need the squirrel. If something eats the squirrel then the squirrel chases the tiger. If the lion chases the mouse and the mouse does not need the lion then the lion does not need the tiger. If something needs the mouse then it is nice. If the squirrel is green and the squirrel is not nice then the squirrel needs the tiger. If something is round and it does not eat the lion then it needs the tiger. If something needs the tiger and it is round then it does not chase the lion.
The lion does not chase the mouse.
("lion" "chases" "mouse" "-")
The lion is blue.
("lion" "is" "blue" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is not round.
("lion" "is" "round" "-")
The lion is not young.
("lion" "is" "young" "-")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is young.
("mouse" "is" "young" "+")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger does not need the lion.
("tiger" "needs" "lion" "-")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
If something is round and it chases the squirrel then it does not eat the lion.
((("something" "is" "round" "+") ("something" "chases" "squirrel" "+")) -> ("something" "eats" "lion" "-"))
If something needs the mouse and it is not round then the mouse does not need the squirrel.
((("something" "needs" "mouse" "+") ("something" "is" "round" "~")) -> ("mouse" "needs" "squirrel" "-"))
If something eats the squirrel then the squirrel chases the tiger.
((("something" "eats" "squirrel" "+")) -> ("squirrel" "chases" "tiger" "+"))
If the lion chases the mouse and the mouse does not need the lion then the lion does not need the tiger.
((("lion" "chases" "mouse" "+") ("mouse" "needs" "lion" "~")) -> ("lion" "needs" "tiger" "-"))
If something needs the mouse then it is nice.
((("something" "needs" "mouse" "+")) -> ("something" "is" "nice" "+"))
If the squirrel is green and the squirrel is not nice then the squirrel needs the tiger.
((("squirrel" "is" "green" "+") ("squirrel" "is" "nice" "~")) -> ("squirrel" "needs" "tiger" "+"))
If something is round and it does not eat the lion then it needs the tiger.
((("something" "is" "round" "+") ("something" "eats" "lion" "~")) -> ("something" "needs" "tiger" "+"))
If something needs the tiger and it is round then it does not chase the lion.
((("something" "needs" "tiger" "+") ("something" "is" "round" "+")) -> ("something" "chases" "lion" "-"))
The squirrel is round.
True
1
proof
[(triple11)]
("squirrel" "is" "round" "+")
triple11
The tiger needs the lion.
False
1
inv-proof
[(triple15)]
("tiger" "needs" "lion" "+")
triple15
The tiger is nice.
True
2
proof
[(((triple16) -> rule5))]
("tiger" "is" "nice" "+")
((triple16) -> (rule5 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The squirrel is not nice.
False
2
inv-proof
[(((triple12) -> rule5))]
("squirrel" "is" "nice" "-")
((triple12) -> (rule5 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The tiger needs the tiger.
True
5
proof
[(((triple14 ((triple14 triple13) -> rule1)) -> rule7))]
("tiger" "needs" "tiger" "+")
((triple14 ((triple14 triple13) -> (rule1 % int2))) -> (rule7 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger does not eat the lion.
("tiger" "eats" "lion" "-")
int2
The tiger does not need the tiger.
False
5
inv-proof
[(((triple14 ((triple14 triple13) -> rule1)) -> rule7))]
("tiger" "needs" "tiger" "-")
((triple14 ((triple14 triple13) -> (rule1 % int2))) -> (rule7 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger does not eat the lion.
("tiger" "eats" "lion" "-")
int2
The tiger does not chase the lion.
True
7
proof
[(((((triple14 ((triple14 triple13) -> rule1)) -> rule7) triple14) -> rule8))]
("tiger" "chases" "lion" "-")
((((triple14 ((triple14 triple13) -> (rule1 % int3))) -> (rule7 % int2)) triple14) -> (rule8 % int1))
The tiger does not chase the lion.
("tiger" "chases" "lion" "-")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger does not eat the lion.
("tiger" "eats" "lion" "-")
int3
The tiger chases the lion.
False
7
inv-proof
[(((((triple14 ((triple14 triple13) -> rule1)) -> rule7) triple14) -> rule8))]
("tiger" "chases" "lion" "+")
((((triple14 ((triple14 triple13) -> (rule1 % int3))) -> (rule7 % int2)) triple14) -> (rule8 % int1))
The tiger does not chase the lion.
("tiger" "chases" "lion" "-")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger does not eat the lion.
("tiger" "eats" "lion" "-")
int3
The squirrel does not chase the tiger.
Unknown
inv-rconc
[@1: The squirrel chases the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "chases" "tiger" "-")
The mouse is nice.
Unknown
rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "nice" "+")
The squirrel does not need the tiger.
Unknown
inv-rconc
[@1: The squirrel needs the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "needs" "tiger" "-")
The mouse needs the tiger.
Unknown
rconc
[@1: The mouse needs the tiger.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "needs" "tiger" "+")
The mouse is not green.
Unknown
inv-random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "-")
The mouse is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "-")
The mouse needs the lion.
Unknown
random
[@0: The mouse needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "lion" "+")
@0: The lion does not chase the mouse.[(triple1)] The lion is blue.[(triple2)] The lion is green.[(triple3)] The lion is nice.[(triple4)] The lion is not round.[(triple5)] The lion is not young.[(triple6)] The mouse chases the lion.[(triple7)] The mouse is blue.[(triple8)] The mouse is young.[(triple9)] The squirrel chases the lion.[(triple10)] The squirrel is round.[(triple11)] The squirrel needs the mouse.[(triple12)] The tiger chases the squirrel.[(triple13)] The tiger does not need the lion.[(triple15)] The tiger is round.[(triple14)] The tiger needs the mouse.[(triple16)] @1: The squirrel is nice.[(((triple12) -> rule5))] The tiger does not eat the lion.[(((triple14 triple13) -> rule1))] The tiger is nice.[(((triple16) -> rule5))] @2: The tiger needs the tiger.[(((triple14 ((triple14 triple13) -> rule1)) -> rule7))] @3: The tiger does not chase the lion.[(((((triple14 ((triple14 triple13) -> rule1)) -> rule7) triple14) -> rule8))]
The lion does not chase the mouse.
("lion" "chases" "mouse" "-")
triple1
The lion is blue.
("lion" "is" "blue" "+")
triple2
The lion is green.
("lion" "is" "green" "+")
triple3
The lion is nice.
("lion" "is" "nice" "+")
triple4
The lion is not round.
("lion" "is" "round" "-")
triple5
The lion is not young.
("lion" "is" "young" "-")
triple6
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple7
The mouse is blue.
("mouse" "is" "blue" "+")
triple8
The mouse is young.
("mouse" "is" "young" "+")
triple9
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple10
The squirrel is round.
("squirrel" "is" "round" "+")
triple11
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple12
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple13
The tiger does not need the lion.
("tiger" "needs" "lion" "-")
triple15
The tiger is round.
("tiger" "is" "round" "+")
triple14
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple16
The squirrel is nice.
("squirrel" "is" "nice" "+")
((triple12) -> (rule5 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The tiger does not eat the lion.
("tiger" "eats" "lion" "-")
((triple14 triple13) -> (rule1 % int1))
The tiger does not eat the lion.
("tiger" "eats" "lion" "-")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
((triple16) -> (rule5 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((triple14 ((triple14 triple13) -> (rule1 % int2))) -> (rule7 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger does not eat the lion.
("tiger" "eats" "lion" "-")
int2
The tiger does not chase the lion.
("tiger" "chases" "lion" "-")
((((triple14 ((triple14 triple13) -> (rule1 % int3))) -> (rule7 % int2)) triple14) -> (rule8 % int1))
The tiger does not chase the lion.
("tiger" "chases" "lion" "-")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger does not eat the lion.
("tiger" "eats" "lion" "-")
int3