The cat sees the tiger. The lion chases the tiger. The lion is kind. The lion sees the cat. The tiger chases the cat. The tiger eats the lion. The tiger is green. The tiger is nice. The tiger is red. The tiger is young. The tiger sees the cat. The tiger sees the lion. If someone chases the lion then the lion sees the tiger. If someone sees the cat then they see the lion. If someone sees the lion and they chase the cat then the lion is nice. If the tiger sees the lion then the lion is nice. If someone sees the tiger then they chase the lion. If someone eats the lion then the lion chases the cat.
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If someone chases the lion then the lion sees the tiger.
((("someone" "chases" "lion" "+")) -> ("lion" "sees" "tiger" "+"))
If someone sees the cat then they see the lion.
((("someone" "sees" "cat" "+")) -> ("someone" "sees" "lion" "+"))
If someone sees the lion and they chase the cat then the lion is nice.
((("someone" "sees" "lion" "+") ("someone" "chases" "cat" "+")) -> ("lion" "is" "nice" "+"))
If the tiger sees the lion then the lion is nice.
((("tiger" "sees" "lion" "+")) -> ("lion" "is" "nice" "+"))
If someone sees the tiger then they chase the lion.
((("someone" "sees" "tiger" "+")) -> ("someone" "chases" "lion" "+"))
If someone eats the lion then the lion chases the cat.
((("someone" "eats" "lion" "+")) -> ("lion" "chases" "cat" "+"))
The lion is kind.
True
1
proof
[(triple3)]
("lion" "is" "kind" "+")
triple3
The tiger is not red.
False
1
inv-proof
[(triple9)]
("tiger" "is" "red" "-")
triple9
The cat chases the lion.
True
2
proof
[(((triple1) -> rule5))]
("cat" "chases" "lion" "+")
((triple1) -> (rule5 % int1))
The cat chases the lion.
("cat" "chases" "lion" "+")
int1
The cat does not chase the lion.
False
2
inv-proof
[(((triple1) -> rule5))]
("cat" "chases" "lion" "-")
((triple1) -> (rule5 % int1))
The cat chases the lion.
("cat" "chases" "lion" "+")
int1
The lion sees the tiger.
True
3
proof
[(((((triple1) -> rule5)) -> rule1))]
("lion" "sees" "tiger" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The cat chases the lion.
("cat" "chases" "lion" "+")
int2
The lion does not see the tiger.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule1))]
("lion" "sees" "tiger" "-")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The cat chases the lion.
("cat" "chases" "lion" "+")
int2
The lion chases the lion.
True
4
proof
[(((((((triple1) -> rule5)) -> rule1)) -> rule5))]
("lion" "chases" "lion" "+")
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The cat chases the lion.
("cat" "chases" "lion" "+")
int3
The lion does not chase the lion.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule1)) -> rule5))]
("lion" "chases" "lion" "-")
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The cat chases the lion.
("cat" "chases" "lion" "+")
int3
The tiger does not chase the lion.
Unknown
inv-rconc
[@1: The tiger chases the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "chases" "lion" "-")
The cat sees the lion.
Unknown
rconc
[@1: The cat sees the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "sees" "lion" "+")
The tiger does not eat the cat.
Unknown
inv-random
[@0: The tiger eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "cat" "-")
The cat eats the lion.
Unknown
random
[@0: The cat eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "lion" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The cat is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
@0: The cat sees the tiger.[(triple1)] The lion chases the tiger.[(triple2)] The lion is kind.[(triple3)] The lion sees the cat.[(triple4)] The tiger chases the cat.[(triple5)] The tiger eats the lion.[(triple6)] The tiger is green.[(triple7)] The tiger is nice.[(triple8)] The tiger is red.[(triple9)] The tiger is young.[(triple10)] The tiger sees the cat.[(triple11)] The tiger sees the lion.[(triple12 OR ((triple11) -> rule2))] @1: The cat chases the lion.[(((triple1) -> rule5))] The lion chases the cat.[(((triple6) -> rule6))] The lion is nice.[(((triple12) -> rule4) OR ((triple12 triple5) -> rule3) OR ((((triple11) -> rule2)) -> rule4) OR ((((triple11) -> rule2) triple5) -> rule3) OR ((((triple4) -> rule2) ((triple6) -> rule6)) -> rule3))] The lion sees the lion.[(((triple4) -> rule2))] @2: The lion sees the tiger.[(((((triple1) -> rule5)) -> rule1))] @3: The lion chases the lion.[(((((((triple1) -> rule5)) -> rule1)) -> rule5))]
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple1
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple2
The lion is kind.
("lion" "is" "kind" "+")
triple3
The lion sees the cat.
("lion" "sees" "cat" "+")
triple4
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple5
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple6
The tiger is green.
("tiger" "is" "green" "+")
triple7
The tiger is nice.
("tiger" "is" "nice" "+")
triple8
The tiger is red.
("tiger" "is" "red" "+")
triple9
The tiger is young.
("tiger" "is" "young" "+")
triple10
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple11
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple12
((triple11) -> (rule2 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The cat chases the lion.
("cat" "chases" "lion" "+")
((triple1) -> (rule5 % int1))
The cat chases the lion.
("cat" "chases" "lion" "+")
int1
The lion chases the cat.
("lion" "chases" "cat" "+")
((triple6) -> (rule6 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
((triple12) -> (rule4 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
((triple12 triple5) -> (rule3 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
((((triple11) -> (rule2 % int2))) -> (rule4 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int2
((((triple11) -> (rule2 % int2)) triple5) -> (rule3 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int2
((((triple4) -> (rule2 % int3)) ((triple6) -> (rule6 % int2))) -> (rule3 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion chases the cat.
("lion" "chases" "cat" "+")
int2
The lion sees the lion.
("lion" "sees" "lion" "+")
int3
The lion sees the lion.
("lion" "sees" "lion" "+")
((triple4) -> (rule2 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The cat chases the lion.
("cat" "chases" "lion" "+")
int2
The lion chases the lion.
("lion" "chases" "lion" "+")
((((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The cat chases the lion.
("cat" "chases" "lion" "+")
int3