The bear does not visit the tiger. The lion visits the squirrel. The squirrel chases the bear. The tiger sees the bear. If something chases the squirrel then it visits the lion. If something sees the lion then the lion visits the squirrel. If something sees the lion then the lion visits the squirrel. If something sees the bear then it does not visit the bear. If something is young then it chases the squirrel. If something visits the squirrel then it chases the squirrel. If something sees the tiger and the tiger chases the squirrel then the squirrel chases the tiger. If something chases the tiger and it does not see the squirrel then the squirrel does not visit the tiger.
The bear does not visit the tiger.
("bear" "visits" "tiger" "-")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
If something chases the squirrel then it visits the lion.
((("something" "chases" "squirrel" "+")) -> ("something" "visits" "lion" "+"))
If something sees the lion then the lion visits the squirrel.
((("something" "sees" "lion" "+")) -> ("lion" "visits" "squirrel" "+"))
If something sees the lion then the lion visits the squirrel.
((("something" "sees" "lion" "+")) -> ("lion" "visits" "squirrel" "+"))
If something sees the bear then it does not visit the bear.
((("something" "sees" "bear" "+")) -> ("something" "visits" "bear" "-"))
If something is young then it chases the squirrel.
((("something" "is" "young" "+")) -> ("something" "chases" "squirrel" "+"))
If something visits the squirrel then it chases the squirrel.
((("something" "visits" "squirrel" "+")) -> ("something" "chases" "squirrel" "+"))
If something sees the tiger and the tiger chases the squirrel then the squirrel chases the tiger.
((("something" "sees" "tiger" "+") ("tiger" "chases" "squirrel" "+")) -> ("squirrel" "chases" "tiger" "+"))
If something chases the tiger and it does not see the squirrel then the squirrel does not visit the tiger.
((("something" "chases" "tiger" "+") ("something" "sees" "squirrel" "~")) -> ("squirrel" "visits" "tiger" "-"))
The lion visits the squirrel.
True
1
proof
[(triple2)]
("lion" "visits" "squirrel" "+")
triple2
The lion does not visit the squirrel.
False
1
inv-proof
[(triple2)]
("lion" "visits" "squirrel" "-")
triple2
The tiger does not visit the bear.
True
2
proof
[(((triple4) -> rule4))]
("tiger" "visits" "bear" "-")
((triple4) -> (rule4 % int1))
The tiger does not visit the bear.
("tiger" "visits" "bear" "-")
int1
The tiger visits the bear.
False
2
inv-proof
[(((triple4) -> rule4))]
("tiger" "visits" "bear" "+")
((triple4) -> (rule4 % int1))
The tiger does not visit the bear.
("tiger" "visits" "bear" "-")
int1
The lion visits the lion.
True
3
proof
[(((((triple2) -> rule6)) -> rule1))]
("lion" "visits" "lion" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int2
The lion does not visit the lion.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule1))]
("lion" "visits" "lion" "-")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int2
The tiger does not chase the squirrel.
Unknown
inv-rconc
[@1: The tiger chases the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "chases" "squirrel" "-")
The squirrel chases the squirrel.
Unknown
rconc
[@1: The squirrel chases the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "chases" "squirrel" "+")
The tiger does not visit the lion.
Unknown
inv-rconc
[@2: The tiger visits the lion.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("tiger" "visits" "lion" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
The bear is not cold.
Unknown
inv-random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "-")
The lion sees the tiger.
Unknown
random
[@0: The lion sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "tiger" "+")
@0: The bear does not visit the tiger.[(triple1)] The lion visits the squirrel.[(triple2)] The squirrel chases the bear.[(triple3)] The tiger sees the bear.[(triple4)] @1: The lion chases the squirrel.[(((triple2) -> rule6))] The tiger does not visit the bear.[(((triple4) -> rule4))] @2: The lion visits the lion.[(((((triple2) -> rule6)) -> rule1))]
The bear does not visit the tiger.
("bear" "visits" "tiger" "-")
triple1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple2
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
triple3
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple4
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
((triple2) -> (rule6 % int1))
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int1
The tiger does not visit the bear.
("tiger" "visits" "bear" "-")
((triple4) -> (rule4 % int1))
The tiger does not visit the bear.
("tiger" "visits" "bear" "-")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
int2