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