The bear is rough. The bear is round. The cat is rough. The cat does not like the bear. The cat visits the bear. The cat does not visit the squirrel. The lion does not like the squirrel. The squirrel likes the bear. The squirrel sees the cat. The squirrel visits the bear. If someone visits the lion then they visit the cat. If someone likes the bear then they visit the cat. If someone visits the cat then they see the bear. If someone visits the cat then the cat is blue. If someone is rough then they like the lion. If the bear sees the cat then the bear likes the cat. If the cat is round and the cat sees the lion then the cat likes the bear. If someone is blue then they visit the lion. If someone visits the lion and they are blue then the lion likes the cat.
The bear is rough.
("bear" "is" "rough" "+")
The bear is round.
("bear" "is" "round" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat does not like the bear.
("cat" "likes" "bear" "-")
The cat visits the bear.
("cat" "visits" "bear" "+")
The cat does not visit the squirrel.
("cat" "visits" "squirrel" "-")
The lion does not like the squirrel.
("lion" "likes" "squirrel" "-")
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
If someone visits the lion then they visit the cat.
((("someone" "visits" "lion" "+")) -> ("someone" "visits" "cat" "+"))
If someone likes the bear then they visit the cat.
((("someone" "likes" "bear" "+")) -> ("someone" "visits" "cat" "+"))
If someone visits the cat then they see the bear.
((("someone" "visits" "cat" "+")) -> ("someone" "sees" "bear" "+"))
If someone visits the cat then the cat is blue.
((("someone" "visits" "cat" "+")) -> ("cat" "is" "blue" "+"))
If someone is rough then they like the lion.
((("someone" "is" "rough" "+")) -> ("someone" "likes" "lion" "+"))
If the bear sees the cat then the bear likes the cat.
((("bear" "sees" "cat" "+")) -> ("bear" "likes" "cat" "+"))
If the cat is round and the cat sees the lion then the cat likes the bear.
((("cat" "is" "round" "+") ("cat" "sees" "lion" "+")) -> ("cat" "likes" "bear" "+"))
If someone is blue then they visit the lion.
((("someone" "is" "blue" "+")) -> ("someone" "visits" "lion" "+"))
If someone visits the lion and they are blue then the lion likes the cat.
((("someone" "visits" "lion" "+") ("someone" "is" "blue" "+")) -> ("lion" "likes" "cat" "+"))
The bear is round.
True
1
proof
[(triple2)]
("bear" "is" "round" "+")
triple2
The bear is not rough.
False
1
inv-proof
[(triple1)]
("bear" "is" "rough" "-")
triple1
The bear likes the lion.
True
2
proof
[(((triple1) -> rule5))]
("bear" "likes" "lion" "+")
((triple1) -> (rule5 % int1))
The bear likes the lion.
("bear" "likes" "lion" "+")
int1
The bear does not like the lion.
False
2
inv-proof
[(((triple1) -> rule5))]
("bear" "likes" "lion" "-")
((triple1) -> (rule5 % int1))
The bear likes the lion.
("bear" "likes" "lion" "+")
int1
The cat is blue.
True
3
proof
[(((((triple8) -> rule2)) -> rule4))]
("cat" "is" "blue" "+")
((((triple8) -> (rule2 % int2))) -> (rule4 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int2
The cat is not blue.
False
3
inv-proof
[(((((triple8) -> rule2)) -> rule4))]
("cat" "is" "blue" "-")
((((triple8) -> (rule2 % int2))) -> (rule4 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int2
The cat visits the lion.
True
4
proof
[(((((((triple8) -> rule2)) -> rule4)) -> rule8))]
("cat" "visits" "lion" "+")
((((((triple8) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int3
The cat does not visit the lion.
False
4
inv-proof
[(((((((triple8) -> rule2)) -> rule4)) -> rule8))]
("cat" "visits" "lion" "-")
((((((triple8) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int3
The cat visits the cat.
True
5
proof
[(((((((((triple8) -> rule2)) -> rule4)) -> rule8)) -> rule1))]
("cat" "visits" "cat" "+")
((((((((triple8) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int4
The lion does not like the cat.
False
8
inv-proof
[(((((((((triple8) -> rule2)) -> rule4)) -> rule8) ((((triple8) -> rule2)) -> rule4)) -> rule9))]
("lion" "likes" "cat" "-")
((((((((triple8) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) ((((triple8) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule9 % int1))
The lion likes the cat.
("lion" "likes" "cat" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int4
The cat sees the bear.
True
6
proof
[(((((((((((triple8) -> rule2)) -> rule4)) -> rule8)) -> rule1)) -> rule3))]
("cat" "sees" "bear" "+")
((((((((((triple8) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cat sees the bear.
("cat" "sees" "bear" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat visits the lion.
("cat" "visits" "lion" "+")
int3
The cat is blue.
("cat" "is" "blue" "+")
int4
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int5
The cat does not see the bear.
False
6
inv-proof
[(((((((((((triple8) -> rule2)) -> rule4)) -> rule8)) -> rule1)) -> rule3))]
("cat" "sees" "bear" "-")
((((((((((triple8) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cat sees the bear.
("cat" "sees" "bear" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat visits the lion.
("cat" "visits" "lion" "+")
int3
The cat is blue.
("cat" "is" "blue" "+")
int4
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int5
The bear does not visit the lion.
Unknown
inv-rconc
[@1: The bear visits the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "visits" "lion" "-")
The lion visits the lion.
Unknown
rconc
[@1: The lion visits the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "visits" "lion" "+")
The bear does not like the cat.
Unknown
inv-rconc
[@1: The bear likes the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "likes" "cat" "-")
The bear visits the cat.
Unknown
rconc
[@2: The bear visits the cat.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("bear" "visits" "cat" "+")
The lion does not visit the cat.
Unknown
inv-rconc
[@2: The lion visits the cat.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("lion" "visits" "cat" "-")
The bear sees the bear.
Unknown
rconc
[@3: The bear sees the bear.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule8 <- FAIL)]]
("bear" "sees" "bear" "+")
The bear does not like the squirrel.
Unknown
inv-random
[@0: The bear likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "squirrel" "-")
The cat sees the lion.
Unknown
random
[@0: The cat sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "lion" "+")
The lion is not rough.
Unknown
inv-random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "-")
The lion sees the squirrel.
Unknown
random
[@0: The lion sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "squirrel" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The cat sees the squirrel.
Unknown
random
[@0: The cat sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "squirrel" "+")
@0: The bear is rough.[(triple1)] The bear is round.[(triple2)] The cat does not like the bear.[(triple4)] The cat does not visit the squirrel.[(triple6)] The cat is rough.[(triple3)] The cat visits the bear.[(triple5)] The lion does not like the squirrel.[(triple7)] The squirrel likes the bear.[(triple8)] The squirrel sees the cat.[(triple9)] The squirrel visits the bear.[(triple10)] @1: The bear likes the lion.[(((triple1) -> rule5))] The cat likes the lion.[(((triple3) -> rule5))] The squirrel visits the cat.[(((triple8) -> rule2))] @2: The cat is blue.[(((((triple8) -> rule2)) -> rule4))] The squirrel sees the bear.[(((((triple8) -> rule2)) -> rule3))] @3: The cat visits the lion.[(((((((triple8) -> rule2)) -> rule4)) -> rule8))] @4: The cat visits the cat.[(((((((((triple8) -> rule2)) -> rule4)) -> rule8)) -> rule1))] The lion likes the cat.[(((((((((triple8) -> rule2)) -> rule4)) -> rule8) ((((triple8) -> rule2)) -> rule4)) -> rule9))] @5: The cat sees the bear.[(((((((((((triple8) -> rule2)) -> rule4)) -> rule8)) -> rule1)) -> rule3))]
The bear is rough.
("bear" "is" "rough" "+")
triple1
The bear is round.
("bear" "is" "round" "+")
triple2
The cat does not like the bear.
("cat" "likes" "bear" "-")
triple4
The cat does not visit the squirrel.
("cat" "visits" "squirrel" "-")
triple6
The cat is rough.
("cat" "is" "rough" "+")
triple3
The cat visits the bear.
("cat" "visits" "bear" "+")
triple5
The lion does not like the squirrel.
("lion" "likes" "squirrel" "-")
triple7
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
triple8
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple9
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
triple10
The bear likes the lion.
("bear" "likes" "lion" "+")
((triple1) -> (rule5 % int1))
The bear likes the lion.
("bear" "likes" "lion" "+")
int1
The cat likes the lion.
("cat" "likes" "lion" "+")
((triple3) -> (rule5 % int1))
The cat likes the lion.
("cat" "likes" "lion" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
((triple8) -> (rule2 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
((((triple8) -> (rule2 % int2))) -> (rule4 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int2
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
((((triple8) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int2
The cat visits the lion.
("cat" "visits" "lion" "+")
((((((triple8) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int3
The cat visits the cat.
("cat" "visits" "cat" "+")
((((((((triple8) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int4
The lion likes the cat.
("lion" "likes" "cat" "+")
((((((((triple8) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule8 % int2)) ((((triple8) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule9 % int1))
The lion likes the cat.
("lion" "likes" "cat" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int4
The cat sees the bear.
("cat" "sees" "bear" "+")
((((((((((triple8) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cat sees the bear.
("cat" "sees" "bear" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat visits the lion.
("cat" "visits" "lion" "+")
int3
The cat is blue.
("cat" "is" "blue" "+")
int4
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int5