The bear eats the lion. The bear is blue. The bear is round. The bear likes the lion. The bear likes the squirrel. The bear visits the lion. The lion likes the squirrel. The lion visits the bear. The lion visits the squirrel. The squirrel likes the lion. If something visits the squirrel then the squirrel likes the lion. If the lion is round then the lion is young. If something visits the squirrel and the squirrel is blue then it eats the lion. If something visits the squirrel then the squirrel likes the bear. If something is nice then it visits the bear. If something likes the bear then it is nice.
The bear eats the lion.
("bear" "eats" "lion" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear is round.
("bear" "is" "round" "+")
The bear likes the lion.
("bear" "likes" "lion" "+")
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
The bear visits the lion.
("bear" "visits" "lion" "+")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
If something visits the squirrel then the squirrel likes the lion.
((("something" "visits" "squirrel" "+")) -> ("squirrel" "likes" "lion" "+"))
If the lion is round then the lion is young.
((("lion" "is" "round" "+")) -> ("lion" "is" "young" "+"))
If something visits the squirrel and the squirrel is blue then it eats the lion.
((("something" "visits" "squirrel" "+") ("squirrel" "is" "blue" "+")) -> ("something" "eats" "lion" "+"))
If something visits the squirrel then the squirrel likes the bear.
((("something" "visits" "squirrel" "+")) -> ("squirrel" "likes" "bear" "+"))
If something is nice then it visits the bear.
((("something" "is" "nice" "+")) -> ("something" "visits" "bear" "+"))
If something likes the bear then it is nice.
((("something" "likes" "bear" "+")) -> ("something" "is" "nice" "+"))
The lion likes the squirrel.
True
1
proof
[(triple7)]
("lion" "likes" "squirrel" "+")
triple7
The lion does not visit the squirrel.
False
1
inv-proof
[(triple9)]
("lion" "visits" "squirrel" "-")
triple9
The squirrel likes the bear.
True
2
proof
[(((triple9) -> rule4))]
("squirrel" "likes" "bear" "+")
((triple9) -> (rule4 % int1))
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int1
The squirrel does not like the bear.
False
2
inv-proof
[(((triple9) -> rule4))]
("squirrel" "likes" "bear" "-")
((triple9) -> (rule4 % int1))
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int1
The squirrel is nice.
True
3
proof
[(((((triple9) -> rule4)) -> rule6))]
("squirrel" "is" "nice" "+")
((((triple9) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int2
The squirrel is not nice.
False
3
inv-proof
[(((((triple9) -> rule4)) -> rule6))]
("squirrel" "is" "nice" "-")
((((triple9) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int2
The squirrel visits the bear.
True
4
proof
[(((((((triple9) -> rule4)) -> rule6)) -> rule5))]
("squirrel" "visits" "bear" "+")
((((((triple9) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int3
The squirrel does not visit the bear.
False
4
inv-proof
[(((((((triple9) -> rule4)) -> rule6)) -> rule5))]
("squirrel" "visits" "bear" "-")
((((((triple9) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int3
The bear is not nice.
Unknown
inv-rconc
[@1: The bear is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "is" "nice" "-")
The lion is nice.
Unknown
rconc
[@1: The lion is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "is" "nice" "+")
The squirrel does not eat the lion.
Unknown
inv-rconc
[@1: The squirrel eats the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "eats" "lion" "-")
The lion is young.
Unknown
rconc
[@1: The lion is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "young" "+")
The lion is not blue.
Unknown
inv-random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "-")
The bear visits the squirrel.
Unknown
random
[@0: The bear visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "squirrel" "+")
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
The lion is round.
Unknown
random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "+")
@0: The bear eats the lion.[(triple1)] The bear is blue.[(triple2)] The bear is round.[(triple3)] The bear likes the lion.[(triple4)] The bear likes the squirrel.[(triple5)] The bear visits the lion.[(triple6)] The lion likes the squirrel.[(triple7)] The lion visits the bear.[(triple8)] The lion visits the squirrel.[(triple9)] The squirrel likes the lion.[(triple10 OR ((triple9) -> rule1))] @1: The squirrel likes the bear.[(((triple9) -> rule4))] @2: The squirrel is nice.[(((((triple9) -> rule4)) -> rule6))] @3: The squirrel visits the bear.[(((((((triple9) -> rule4)) -> rule6)) -> rule5))]
The bear eats the lion.
("bear" "eats" "lion" "+")
triple1
The bear is blue.
("bear" "is" "blue" "+")
triple2
The bear is round.
("bear" "is" "round" "+")
triple3
The bear likes the lion.
("bear" "likes" "lion" "+")
triple4
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
triple5
The bear visits the lion.
("bear" "visits" "lion" "+")
triple6
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple7
The lion visits the bear.
("lion" "visits" "bear" "+")
triple8
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple9
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
triple10
((triple9) -> (rule1 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
((triple9) -> (rule4 % int1))
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
((((triple9) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int2
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
((((((triple9) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
int3