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