The cat is blue. The cat is cold. The cat needs the tiger. The cat sees the tiger. The cat does not visit the tiger. The tiger is blue. The tiger is green. The tiger is kind. The tiger is red. The tiger needs the cat. The tiger sees the cat. The tiger visits the cat. All red people are green. If someone visits the tiger and they are green then the tiger sees the cat. If the tiger is red then the tiger is green. If someone needs the tiger and they see the tiger then the tiger needs the cat. If the cat needs the tiger then the tiger is red. If someone is red and they do not see the cat then they visit the cat.
The cat is blue.
("cat" "is" "blue" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The cat does not visit the tiger.
("cat" "visits" "tiger" "-")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
All red people are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
If someone visits the tiger and they are green then the tiger sees the cat.
((("someone" "visits" "tiger" "+") ("someone" "is" "green" "+")) -> ("tiger" "sees" "cat" "+"))
If the tiger is red then the tiger is green.
((("tiger" "is" "red" "+")) -> ("tiger" "is" "green" "+"))
If someone needs the tiger and they see the tiger then the tiger needs the cat.
((("someone" "needs" "tiger" "+") ("someone" "sees" "tiger" "+")) -> ("tiger" "needs" "cat" "+"))
If the cat needs the tiger then the tiger is red.
((("cat" "needs" "tiger" "+")) -> ("tiger" "is" "red" "+"))
If someone is red and they do not see the cat then they visit the cat.
((("someone" "is" "red" "+") ("someone" "sees" "cat" "~")) -> ("someone" "visits" "cat" "+"))
The tiger is green.
True
1
proof
[(triple7 OR ((triple9) -> rule1) OR ((triple9) -> rule3) OR ((((triple3) -> rule5)) -> rule1) OR ((((triple3) -> rule5)) -> rule3))]
("tiger" "is" "green" "+")
triple7
((triple9) -> (rule1 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((triple9) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The cat does not see the tiger.
False
1
inv-proof
[(triple4)]
("cat" "sees" "tiger" "-")
triple4
The cat is not green.
Unknown
inv-rconc
[@1: The cat is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "green" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The cat does not visit the tiger.[(triple5)] The cat is blue.[(triple1)] The cat is cold.[(triple2)] The cat needs the tiger.[(triple3)] The cat sees the tiger.[(triple4)] The tiger is blue.[(triple6)] The tiger is green.[(triple7 OR ((triple9) -> rule1) OR ((triple9) -> rule3) OR ((((triple3) -> rule5)) -> rule1) OR ((((triple3) -> rule5)) -> rule3))] The tiger is kind.[(triple8)] The tiger is red.[(triple9 OR ((triple3) -> rule5))] The tiger needs the cat.[(triple10 OR ((triple3 triple4) -> rule4))] The tiger sees the cat.[(triple11)] The tiger visits the cat.[(triple12)]
The cat does not visit the tiger.
("cat" "visits" "tiger" "-")
triple5
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple3
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple4
The tiger is blue.
("tiger" "is" "blue" "+")
triple6
The tiger is green.
("tiger" "is" "green" "+")
triple7
((triple9) -> (rule1 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((triple9) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
triple8
The tiger is red.
("tiger" "is" "red" "+")
triple9
((triple3) -> (rule5 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple10
((triple3 triple4) -> (rule4 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple11
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple12