The cat is nice. The rabbit does not like the cat. The squirrel does not like the tiger. The tiger is cold. If someone needs the rabbit then they visit the rabbit. If someone is cold then they visit the rabbit. If someone is young and they need the rabbit then the rabbit visits the tiger. If someone visits the rabbit then they visit the cat. If the tiger visits the squirrel then the squirrel visits the rabbit. If someone is cold and they visit the squirrel then the squirrel visits the tiger. If someone visits the rabbit and they are young then the rabbit is young. If someone is young then they do not need the tiger.
The cat is nice.
("cat" "is" "nice" "+")
The rabbit does not like the cat.
("rabbit" "likes" "cat" "-")
The squirrel does not like the tiger.
("squirrel" "likes" "tiger" "-")
The tiger is cold.
("tiger" "is" "cold" "+")
If someone needs the rabbit then they visit the rabbit.
((("someone" "needs" "rabbit" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone is cold then they visit the rabbit.
((("someone" "is" "cold" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone is young and they need the rabbit then the rabbit visits the tiger.
((("someone" "is" "young" "+") ("someone" "needs" "rabbit" "+")) -> ("rabbit" "visits" "tiger" "+"))
If someone visits the rabbit then they visit the cat.
((("someone" "visits" "rabbit" "+")) -> ("someone" "visits" "cat" "+"))
If the tiger visits the squirrel then the squirrel visits the rabbit.
((("tiger" "visits" "squirrel" "+")) -> ("squirrel" "visits" "rabbit" "+"))
If someone is cold and they visit the squirrel then the squirrel visits the tiger.
((("someone" "is" "cold" "+") ("someone" "visits" "squirrel" "+")) -> ("squirrel" "visits" "tiger" "+"))
If someone visits the rabbit and they are young then the rabbit is young.
((("someone" "visits" "rabbit" "+") ("someone" "is" "young" "+")) -> ("rabbit" "is" "young" "+"))
If someone is young then they do not need the tiger.
((("someone" "is" "young" "+")) -> ("someone" "needs" "tiger" "-"))
The squirrel does not like the tiger.
True
1
proof
[(triple3)]
("squirrel" "likes" "tiger" "-")
triple3
The cat is not nice.
False
1
inv-proof
[(triple1)]
("cat" "is" "nice" "-")
triple1
The tiger visits the rabbit.
True
2
proof
[(((triple4) -> rule2))]
("tiger" "visits" "rabbit" "+")
((triple4) -> (rule2 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The tiger does not visit the rabbit.
False
2
inv-proof
[(((triple4) -> rule2))]
("tiger" "visits" "rabbit" "-")
((triple4) -> (rule2 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The tiger visits the cat.
True
3
proof
[(((((triple4) -> rule2)) -> rule4))]
("tiger" "visits" "cat" "+")
((((triple4) -> (rule2 % int2))) -> (rule4 % int1))
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2
The tiger does not visit the cat.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule4))]
("tiger" "visits" "cat" "-")
((((triple4) -> (rule2 % int2))) -> (rule4 % int1))
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2
The rabbit does not visit the tiger.
Unknown
inv-rconc
[@1: The rabbit visits the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "visits" "tiger" "-")
The squirrel visits the rabbit.
Unknown
rconc
[@1: The squirrel visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "visits" "rabbit" "+")
The cat does not visit the cat.
Unknown
inv-rconc
[@2: The cat visits the cat.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("cat" "visits" "cat" "-")
The tiger is young.
Unknown
random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "+")
The rabbit is not cold.
Unknown
inv-random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
@0: The cat is nice.[(triple1)] The rabbit does not like the cat.[(triple2)] The squirrel does not like the tiger.[(triple3)] The tiger is cold.[(triple4)] @1: The tiger visits the rabbit.[(((triple4) -> rule2))] @2: The tiger visits the cat.[(((((triple4) -> rule2)) -> rule4))]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The rabbit does not like the cat.
("rabbit" "likes" "cat" "-")
triple2
The squirrel does not like the tiger.
("squirrel" "likes" "tiger" "-")
triple3
The tiger is cold.
("tiger" "is" "cold" "+")
triple4
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
((triple4) -> (rule2 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
((((triple4) -> (rule2 % int2))) -> (rule4 % int1))
The tiger visits the cat.
("tiger" "visits" "cat" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2