The lion is cold. The mouse likes the squirrel. The squirrel likes the mouse. The tiger eats the mouse. If something chases the tiger then the tiger eats the lion. If something is cold then it chases the tiger. If something is red then it chases the lion. If something likes the mouse then the mouse likes the lion. If the mouse eats the tiger then the tiger eats the squirrel. If something eats the lion then it likes the mouse.
The lion is cold.
("lion" "is" "cold" "+")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
If something chases the tiger then the tiger eats the lion.
((("something" "chases" "tiger" "+")) -> ("tiger" "eats" "lion" "+"))
If something is cold then it chases the tiger.
((("something" "is" "cold" "+")) -> ("something" "chases" "tiger" "+"))
If something is red then it chases the lion.
((("something" "is" "red" "+")) -> ("something" "chases" "lion" "+"))
If something likes the mouse then the mouse likes the lion.
((("something" "likes" "mouse" "+")) -> ("mouse" "likes" "lion" "+"))
If the mouse eats the tiger then the tiger eats the squirrel.
((("mouse" "eats" "tiger" "+")) -> ("tiger" "eats" "squirrel" "+"))
If something eats the lion then it likes the mouse.
((("something" "eats" "lion" "+")) -> ("something" "likes" "mouse" "+"))
The mouse likes the squirrel.
True
1
proof
[(triple2)]
("mouse" "likes" "squirrel" "+")
triple2
The lion is not cold.
False
1
inv-proof
[(triple1)]
("lion" "is" "cold" "-")
triple1
The lion chases the tiger.
True
2
proof
[(((triple1) -> rule2))]
("lion" "chases" "tiger" "+")
((triple1) -> (rule2 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The lion does not chase the tiger.
False
2
inv-proof
[(((triple1) -> rule2))]
("lion" "chases" "tiger" "-")
((triple1) -> (rule2 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The tiger eats the lion.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("tiger" "eats" "lion" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int2
The tiger does not eat the lion.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("tiger" "eats" "lion" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int2
The tiger likes the mouse.
True
4
proof
[(((((((triple1) -> rule2)) -> rule1)) -> rule6))]
("tiger" "likes" "mouse" "+")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int3
The tiger does not like the mouse.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule1)) -> rule6))]
("tiger" "likes" "mouse" "-")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int3
The tiger does not chase the tiger.
Unknown
inv-rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "chases" "tiger" "-")
The lion likes the mouse.
Unknown
rconc
[@1: The lion likes the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "likes" "mouse" "+")
The tiger does not eat the squirrel.
Unknown
inv-rconc
[@1: The tiger eats the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "eats" "squirrel" "-")
The lion chases the lion.
Unknown
rconc
[@1: The lion chases the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "chases" "lion" "+")
The squirrel is not red.
Unknown
inv-random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "-")
The lion chases the mouse.
Unknown
random
[@0: The lion chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "mouse" "+")
The squirrel does not eat the mouse.
Unknown
inv-random
[@0: The squirrel eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "mouse" "-")
The squirrel is cold.
Unknown
random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "+")
@0: The lion is cold.[(triple1)] The mouse likes the squirrel.[(triple2)] The squirrel likes the mouse.[(triple3)] The tiger eats the mouse.[(triple4)] @1: The lion chases the tiger.[(((triple1) -> rule2))] The mouse likes the lion.[(((triple3) -> rule4) OR ((((((((triple1) -> rule2)) -> rule1)) -> rule6)) -> rule4))] @2: The tiger eats the lion.[(((((triple1) -> rule2)) -> rule1))] @3: The tiger likes the mouse.[(((((((triple1) -> rule2)) -> rule1)) -> rule6))]
The lion is cold.
("lion" "is" "cold" "+")
triple1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple2
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple3
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple4
The lion chases the tiger.
("lion" "chases" "tiger" "+")
((triple1) -> (rule2 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
((triple3) -> (rule4 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
((((((((triple1) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int3
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int4
The tiger eats the lion.
("tiger" "eats" "lion" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int2
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int3