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