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