The lion does not chase the mouse. The lion is not big. The mouse does not chase the lion. The mouse needs the lion. The mouse sees the tiger. The squirrel does not chase the lion. The squirrel sees the lion. The tiger chases the mouse. The tiger is cold. The tiger sees the mouse. If something needs the lion then it needs the squirrel. If something needs the squirrel then it needs the mouse. If the lion is rough and the lion is red then the lion does not chase the squirrel. If something is big and it does not see the lion then it does not chase the mouse. If the tiger chases the mouse and the tiger chases the squirrel then the tiger does not see the mouse. If the mouse needs the lion then the lion needs the mouse. If something chases the mouse and the mouse needs the squirrel then the squirrel chases the tiger. If something chases the tiger and the tiger is cold then it needs the lion. If something is nice and not rough then it is not big.
The lion does not chase the mouse.
("lion" "chases" "mouse" "-")
The lion is not big.
("lion" "is" "big" "-")
The mouse does not chase the lion.
("mouse" "chases" "lion" "-")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The squirrel does not chase the lion.
("squirrel" "chases" "lion" "-")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If something needs the lion then it needs the squirrel.
((("something" "needs" "lion" "+")) -> ("something" "needs" "squirrel" "+"))
If something needs the squirrel then it needs the mouse.
((("something" "needs" "squirrel" "+")) -> ("something" "needs" "mouse" "+"))
If the lion is rough and the lion is red then the lion does not chase the squirrel.
((("lion" "is" "rough" "+") ("lion" "is" "red" "+")) -> ("lion" "chases" "squirrel" "-"))
If something is big and it does not see the lion then it does not chase the mouse.
((("something" "is" "big" "+") ("something" "sees" "lion" "~")) -> ("something" "chases" "mouse" "-"))
If the tiger chases the mouse and the tiger chases the squirrel then the tiger does not see the mouse.
((("tiger" "chases" "mouse" "+") ("tiger" "chases" "squirrel" "+")) -> ("tiger" "sees" "mouse" "-"))
If the mouse needs the lion then the lion needs the mouse.
((("mouse" "needs" "lion" "+")) -> ("lion" "needs" "mouse" "+"))
If something chases the mouse and the mouse needs the squirrel then the squirrel chases the tiger.
((("something" "chases" "mouse" "+") ("mouse" "needs" "squirrel" "+")) -> ("squirrel" "chases" "tiger" "+"))
If something chases the tiger and the tiger is cold then it needs the lion.
((("something" "chases" "tiger" "+") ("tiger" "is" "cold" "+")) -> ("something" "needs" "lion" "+"))
If something is nice and not rough then it is not big.
((("something" "is" "nice" "+") ("something" "is" "rough" "~")) -> ("something" "is" "big" "-"))
The squirrel does not chase the lion.
True
1
proof
[(triple6)]
("squirrel" "chases" "lion" "-")
triple6
The mouse does not need the lion.
False
1
inv-proof
[(triple4)]
("mouse" "needs" "lion" "-")
triple4
The mouse needs the squirrel.
True
2
proof
[(((triple4) -> rule1))]
("mouse" "needs" "squirrel" "+")
((triple4) -> (rule1 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The mouse does not need the squirrel.
False
2
inv-proof
[(((triple4) -> rule1))]
("mouse" "needs" "squirrel" "-")
((triple4) -> (rule1 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The squirrel chases the tiger.
True
4
proof
[(((triple8 ((triple4) -> rule1)) -> rule7))]
("squirrel" "chases" "tiger" "+")
((triple8 ((triple4) -> (rule1 % int2))) -> (rule7 % int1))
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The mouse does not need the mouse.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule2))]
("mouse" "needs" "mouse" "-")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The squirrel needs the lion.
True
6
proof
[(((((triple8 ((triple4) -> rule1)) -> rule7) triple9) -> rule8))]
("squirrel" "needs" "lion" "+")
((((triple8 ((triple4) -> (rule1 % int3))) -> (rule7 % int2)) triple9) -> (rule8 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3
The squirrel does not need the lion.
False
6
inv-proof
[(((((triple8 ((triple4) -> rule1)) -> rule7) triple9) -> rule8))]
("squirrel" "needs" "lion" "-")
((((triple8 ((triple4) -> (rule1 % int3))) -> (rule7 % int2)) triple9) -> (rule8 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3
The squirrel needs the squirrel.
True
7
proof
[(((((((triple8 ((triple4) -> rule1)) -> rule7) triple9) -> rule8)) -> rule1))]
("squirrel" "needs" "squirrel" "+")
((((((triple8 ((triple4) -> (rule1 % int4))) -> (rule7 % int3)) triple9) -> (rule8 % int2))) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int2
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int3
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int4
The squirrel does not need the squirrel.
False
7
inv-proof
[(((((((triple8 ((triple4) -> rule1)) -> rule7) triple9) -> rule8)) -> rule1))]
("squirrel" "needs" "squirrel" "-")
((((((triple8 ((triple4) -> (rule1 % int4))) -> (rule7 % int3)) triple9) -> (rule8 % int2))) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int2
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int3
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int4
The squirrel needs the mouse.
True
8
proof
[(((((((((triple8 ((triple4) -> rule1)) -> rule7) triple9) -> rule8)) -> rule1)) -> rule2))]
("squirrel" "needs" "mouse" "+")
((((((((triple8 ((triple4) -> (rule1 % int5))) -> (rule7 % int4)) triple9) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int2
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int3
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int4
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int5
The squirrel does not need the mouse.
False
8
inv-proof
[(((((((((triple8 ((triple4) -> rule1)) -> rule7) triple9) -> rule8)) -> rule1)) -> rule2))]
("squirrel" "needs" "mouse" "-")
((((((((triple8 ((triple4) -> (rule1 % int5))) -> (rule7 % int4)) triple9) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int2
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int3
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int4
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int5
The tiger does not need the mouse.
Unknown
inv-rconc
[@3: The tiger needs the mouse.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule8 <- FAIL)]]
("tiger" "needs" "mouse" "-")
The lion needs the lion.
Unknown
rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "needs" "lion" "+")
The lion does not need the squirrel.
Unknown
inv-rconc
[@2: The lion needs the squirrel.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("lion" "needs" "squirrel" "-")
The tiger needs the squirrel.
Unknown
rconc
[@2: The tiger needs the squirrel.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("tiger" "needs" "squirrel" "+")
The tiger does not need the lion.
Unknown
inv-rconc
[@1: The tiger needs the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "needs" "lion" "-")
The lion chases the squirrel.
Unknown
random
[@0: The lion chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "squirrel" "+")
The mouse is not red.
Unknown
inv-random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "-")
The mouse sees the squirrel.
Unknown
random
[@0: The mouse sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "squirrel" "+")
The mouse does not need the tiger.
Unknown
inv-random
[@0: The mouse needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "tiger" "-")
The tiger sees the squirrel.
Unknown
random
[@0: The tiger sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "squirrel" "+")
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The lion sees the squirrel.
Unknown
random
[@0: The lion sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "squirrel" "+")
@0: The lion does not chase the mouse.[(triple1)] The lion is not big.[(triple2)] The mouse does not chase the lion.[(triple3)] The mouse needs the lion.[(triple4)] The mouse sees the tiger.[(triple5)] The squirrel does not chase the lion.[(triple6)] The squirrel sees the lion.[(triple7)] The tiger chases the mouse.[(triple8)] The tiger is cold.[(triple9)] The tiger sees the mouse.[(triple10)] @1: The lion needs the mouse.[(((triple4) -> rule6))] The mouse needs the squirrel.[(((triple4) -> rule1))] @2: The mouse needs the mouse.[(((((triple4) -> rule1)) -> rule2))] The squirrel chases the tiger.[(((triple8 ((triple4) -> rule1)) -> rule7))] @3: The squirrel needs the lion.[(((((triple8 ((triple4) -> rule1)) -> rule7) triple9) -> rule8))] @4: The squirrel needs the squirrel.[(((((((triple8 ((triple4) -> rule1)) -> rule7) triple9) -> rule8)) -> rule1))] @5: The squirrel needs the mouse.[(((((((((triple8 ((triple4) -> rule1)) -> rule7) triple9) -> rule8)) -> rule1)) -> rule2))]
The lion does not chase the mouse.
("lion" "chases" "mouse" "-")
triple1
The lion is not big.
("lion" "is" "big" "-")
triple2
The mouse does not chase the lion.
("mouse" "chases" "lion" "-")
triple3
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple4
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple5
The squirrel does not chase the lion.
("squirrel" "chases" "lion" "-")
triple6
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple7
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple8
The tiger is cold.
("tiger" "is" "cold" "+")
triple9
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple10
The lion needs the mouse.
("lion" "needs" "mouse" "+")
((triple4) -> (rule6 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
((triple4) -> (rule1 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
((triple8 ((triple4) -> (rule1 % int2))) -> (rule7 % int1))
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
((((triple8 ((triple4) -> (rule1 % int3))) -> (rule7 % int2)) triple9) -> (rule8 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((((((triple8 ((triple4) -> (rule1 % int4))) -> (rule7 % int3)) triple9) -> (rule8 % int2))) -> (rule1 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int2
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int3
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int4
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
((((((((triple8 ((triple4) -> (rule1 % int5))) -> (rule7 % int4)) triple9) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int2
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int3
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int4
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int5