The dog is blue. The dog is kind. The dog likes the tiger. The dog needs the lion. The lion is cold. The lion is young. The lion likes the tiger. The lion needs the dog. The lion does not see the dog. The tiger is young. The tiger likes the dog. The tiger does not see the lion. If someone is cold then they see the tiger. If the lion sees the tiger then the tiger sees the dog.
The dog is blue.
("dog" "is" "blue" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is young.
("lion" "is" "young" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The lion does not see the dog.
("lion" "sees" "dog" "-")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger does not see the lion.
("tiger" "sees" "lion" "-")
If someone is cold then they see the tiger.
((("someone" "is" "cold" "+")) -> ("someone" "sees" "tiger" "+"))
If the lion sees the tiger then the tiger sees the dog.
((("lion" "sees" "tiger" "+")) -> ("tiger" "sees" "dog" "+"))
The tiger does not see the lion.
True
1
proof
[(triple12)]
("tiger" "sees" "lion" "-")
triple12
The lion is not young.
False
1
inv-proof
[(triple6)]
("lion" "is" "young" "-")
triple6
The lion sees the tiger.
True
2
proof
[(((triple5) -> rule1))]
("lion" "sees" "tiger" "+")
((triple5) -> (rule1 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion does not see the tiger.
False
2
inv-proof
[(((triple5) -> rule1))]
("lion" "sees" "tiger" "-")
((triple5) -> (rule1 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The tiger sees the dog.
True
3
proof
[(((((triple5) -> rule1)) -> rule2))]
("tiger" "sees" "dog" "+")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The tiger does not see the dog.
False
3
inv-proof
[(((((triple5) -> rule1)) -> rule2))]
("tiger" "sees" "dog" "-")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The dog does not see the tiger.
Unknown
inv-rconc
[@1: The dog sees the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "sees" "tiger" "-")
The tiger sees the tiger.
Unknown
rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "sees" "tiger" "+")
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
The tiger is not kind.
Unknown
inv-random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "-")
The dog likes the lion.
Unknown
random
[@0: The dog likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "lion" "+")
@0: The dog is blue.[(triple1)] The dog is kind.[(triple2)] The dog likes the tiger.[(triple3)] The dog needs the lion.[(triple4)] The lion does not see the dog.[(triple9)] The lion is cold.[(triple5)] The lion is young.[(triple6)] The lion likes the tiger.[(triple7)] The lion needs the dog.[(triple8)] The tiger does not see the lion.[(triple12)] The tiger is young.[(triple10)] The tiger likes the dog.[(triple11)] @1: The lion sees the tiger.[(((triple5) -> rule1))] @2: The tiger sees the dog.[(((((triple5) -> rule1)) -> rule2))]
The dog is blue.
("dog" "is" "blue" "+")
triple1
The dog is kind.
("dog" "is" "kind" "+")
triple2
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple3
The dog needs the lion.
("dog" "needs" "lion" "+")
triple4
The lion does not see the dog.
("lion" "sees" "dog" "-")
triple9
The lion is cold.
("lion" "is" "cold" "+")
triple5
The lion is young.
("lion" "is" "young" "+")
triple6
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple7
The lion needs the dog.
("lion" "needs" "dog" "+")
triple8
The tiger does not see the lion.
("tiger" "sees" "lion" "-")
triple12
The tiger is young.
("tiger" "is" "young" "+")
triple10
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple11
The lion sees the tiger.
("lion" "sees" "tiger" "+")
((triple5) -> (rule1 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2