The bear does not chase the lion. The bear is cold. The bear is rough. The bear sees the lion. The bear visits the lion. The lion is young. The lion sees the bear. If something chases the lion then the lion visits the bear. If something is young then it chases the lion. If the bear is not red then the bear sees the lion. If something sees the lion then the lion is not red. If the lion sees the bear and the bear chases the lion then the lion is rough. If the lion visits the bear then the lion is not round. If something is round and it does not visit the lion then it does not visit the bear. If something chases the lion and it does not see the lion then it visits the bear.
The bear does not chase the lion.
("bear" "chases" "lion" "-")
The bear is cold.
("bear" "is" "cold" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear sees the lion.
("bear" "sees" "lion" "+")
The bear visits the lion.
("bear" "visits" "lion" "+")
The lion is young.
("lion" "is" "young" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
If something chases the lion then the lion visits the bear.
((("something" "chases" "lion" "+")) -> ("lion" "visits" "bear" "+"))
If something is young then it chases the lion.
((("something" "is" "young" "+")) -> ("something" "chases" "lion" "+"))
If the bear is not red then the bear sees the lion.
((("bear" "is" "red" "~")) -> ("bear" "sees" "lion" "+"))
If something sees the lion then the lion is not red.
((("something" "sees" "lion" "+")) -> ("lion" "is" "red" "-"))
If the lion sees the bear and the bear chases the lion then the lion is rough.
((("lion" "sees" "bear" "+") ("bear" "chases" "lion" "+")) -> ("lion" "is" "rough" "+"))
If the lion visits the bear then the lion is not round.
((("lion" "visits" "bear" "+")) -> ("lion" "is" "round" "-"))
If something is round and it does not visit the lion then it does not visit the bear.
((("something" "is" "round" "+") ("something" "visits" "lion" "~")) -> ("something" "visits" "bear" "-"))
If something chases the lion and it does not see the lion then it visits the bear.
((("something" "chases" "lion" "+") ("something" "sees" "lion" "~")) -> ("something" "visits" "bear" "+"))
The bear is cold.
True
1
proof
[(triple2)]
("bear" "is" "cold" "+")
triple2
The bear is not cold.
False
1
inv-proof
[(triple2)]
("bear" "is" "cold" "-")
triple2
The lion chases the lion.
True
2
proof
[(((triple6) -> rule2))]
("lion" "chases" "lion" "+")
((triple6) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion does not chase the lion.
False
2
inv-proof
[(((triple6) -> rule2))]
("lion" "chases" "lion" "-")
((triple6) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion visits the bear.
True
3
proof
[(((((triple6) -> rule2)) -> rule1))]
("lion" "visits" "bear" "+")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion does not visit the bear.
False
3
inv-proof
[(((((triple6) -> rule2)) -> rule1))]
("lion" "visits" "bear" "-")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion is not round.
True
4
proof
[(((((((triple6) -> rule2)) -> rule1)) -> rule6))]
("lion" "is" "round" "-")
((((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The lion is not round.
("lion" "is" "round" "-")
int1
The lion visits the bear.
("lion" "visits" "bear" "+")
int2
The lion chases the lion.
("lion" "chases" "lion" "+")
int3
The lion is round.
False
4
inv-proof
[(((((((triple6) -> rule2)) -> rule1)) -> rule6))]
("lion" "is" "round" "+")
((((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The lion is not round.
("lion" "is" "round" "-")
int1
The lion visits the bear.
("lion" "visits" "bear" "+")
int2
The lion chases the lion.
("lion" "chases" "lion" "+")
int3
The bear does not visit the bear.
Unknown
inv-rconc
[@1: The bear visits the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "visits" "bear" "-")
The lion is rough.
Unknown
rconc
[@1: The lion is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "is" "rough" "+")
The bear does not chase the bear.
Unknown
inv-random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "-")
The bear is round.
Unknown
random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "+")
The lion is not cold.
Unknown
inv-random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "-")
The bear is red.
Unknown
random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "+")
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 lion chases the bear.
Unknown
random
[@0: The lion chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "bear" "+")
@0: The bear does not chase the lion.[(triple1)] The bear is cold.[(triple2)] The bear is rough.[(triple3)] The bear sees the lion.[(triple4)] The bear visits the lion.[(triple5)] The lion is young.[(triple6)] The lion sees the bear.[(triple7)] @1: The lion chases the lion.[(((triple6) -> rule2))] The lion is not red.[(((triple4) -> rule4))] @2: The lion visits the bear.[(((((triple6) -> rule2)) -> rule1))] @3: The lion is not round.[(((((((triple6) -> rule2)) -> rule1)) -> rule6))]
The bear does not chase the lion.
("bear" "chases" "lion" "-")
triple1
The bear is cold.
("bear" "is" "cold" "+")
triple2
The bear is rough.
("bear" "is" "rough" "+")
triple3
The bear sees the lion.
("bear" "sees" "lion" "+")
triple4
The bear visits the lion.
("bear" "visits" "lion" "+")
triple5
The lion is young.
("lion" "is" "young" "+")
triple6
The lion sees the bear.
("lion" "sees" "bear" "+")
triple7
The lion chases the lion.
("lion" "chases" "lion" "+")
((triple6) -> (rule2 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion is not red.
("lion" "is" "red" "-")
((triple4) -> (rule4 % int1))
The lion is not red.
("lion" "is" "red" "-")
int1
The lion visits the bear.
("lion" "visits" "bear" "+")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion is not round.
("lion" "is" "round" "-")
((((((triple6) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The lion is not round.
("lion" "is" "round" "-")
int1
The lion visits the bear.
("lion" "visits" "bear" "+")
int2
The lion chases the lion.
("lion" "chases" "lion" "+")
int3