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