The cat chases the rabbit. The rabbit likes the tiger. The squirrel is nice. The tiger does not need the rabbit. If something chases the cat then it is rough. If something likes the tiger then the tiger is nice.
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The tiger does not need the rabbit.
("tiger" "needs" "rabbit" "-")
If something chases the cat then it is rough.
((("something" "chases" "cat" "+")) -> ("something" "is" "rough" "+"))
If something likes the tiger then the tiger is nice.
((("something" "likes" "tiger" "+")) -> ("tiger" "is" "nice" "+"))
The cat chases the rabbit.
True
1
proof
[(triple1)]
("cat" "chases" "rabbit" "+")
triple1
The cat does not chase the rabbit.
False
1
inv-proof
[(triple1)]
("cat" "chases" "rabbit" "-")
triple1
The tiger is nice.
True
2
proof
[(((triple2) -> rule2))]
("tiger" "is" "nice" "+")
((triple2) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is not nice.
False
2
inv-proof
[(((triple2) -> rule2))]
("tiger" "is" "nice" "-")
((triple2) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is not rough.
Unknown
inv-rconc
[@1: The tiger is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "rough" "-")
The rabbit is rough.
Unknown
rconc
[@1: The rabbit is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "rough" "+")
The squirrel does not need the cat.
Unknown
inv-random
[@0: The squirrel needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "cat" "-")
The cat is blue.
Unknown
random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "+")
@0: The cat chases the rabbit.[(triple1)] The rabbit likes the tiger.[(triple2)] The squirrel is nice.[(triple3)] The tiger does not need the rabbit.[(triple4)] @1: The tiger is nice.[(((triple2) -> rule2))]
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple1
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple2
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple3
The tiger does not need the rabbit.
("tiger" "needs" "rabbit" "-")
triple4
The tiger is nice.
("tiger" "is" "nice" "+")
((triple2) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1