The bear chases the cat. The cat is young. The lion likes the bear. The tiger is cold. If something is cold then it visits the tiger. If the bear likes the cat and the cat likes the bear then the bear likes the lion.
The bear chases the cat.
("bear" "chases" "cat" "+")
The cat is young.
("cat" "is" "young" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
If something is cold then it visits the tiger.
((("something" "is" "cold" "+")) -> ("something" "visits" "tiger" "+"))
If the bear likes the cat and the cat likes the bear then the bear likes the lion.
((("bear" "likes" "cat" "+") ("cat" "likes" "bear" "+")) -> ("bear" "likes" "lion" "+"))
The cat is young.
True
1
proof
[(triple2)]
("cat" "is" "young" "+")
triple2
The lion does not like the bear.
False
1
inv-proof
[(triple3)]
("lion" "likes" "bear" "-")
triple3
The tiger visits the tiger.
True
2
proof
[(((triple4) -> rule1))]
("tiger" "visits" "tiger" "+")
((triple4) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger does not visit the tiger.
False
2
inv-proof
[(((triple4) -> rule1))]
("tiger" "visits" "tiger" "-")
((triple4) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The lion does not visit the tiger.
Unknown
inv-rconc
[@1: The lion visits the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "visits" "tiger" "-")
The bear visits the tiger.
Unknown
rconc
[@1: The bear visits the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "visits" "tiger" "+")
The cat does not like the lion.
Unknown
inv-random
[@0: The cat likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "lion" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
@0: The bear chases the cat.[(triple1)] The cat is young.[(triple2)] The lion likes the bear.[(triple3)] The tiger is cold.[(triple4)] @1: The tiger visits the tiger.[(((triple4) -> rule1))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
The cat is young.
("cat" "is" "young" "+")
triple2
The lion likes the bear.
("lion" "likes" "bear" "+")
triple3
The tiger is cold.
("tiger" "is" "cold" "+")
triple4
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple4) -> (rule1 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1