The cat is not rough. The rabbit is nice. The squirrel is green. The tiger is nice. If someone is rough then they eat the squirrel. If someone is cold then they chase the squirrel. If the cat is young then the cat is rough. If someone eats the tiger then they see the tiger. If someone chases the rabbit then the rabbit chases the cat. If someone chases the tiger and they are not green then the tiger sees the cat. If the tiger eats the squirrel then the tiger sees the squirrel. All nice people are rough.
The cat is not rough.
("cat" "is" "rough" "-")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
If someone is rough then they eat the squirrel.
((("someone" "is" "rough" "+")) -> ("someone" "eats" "squirrel" "+"))
If someone is cold then they chase the squirrel.
((("someone" "is" "cold" "+")) -> ("someone" "chases" "squirrel" "+"))
If the cat is young then the cat is rough.
((("cat" "is" "young" "+")) -> ("cat" "is" "rough" "+"))
If someone eats the tiger then they see the tiger.
((("someone" "eats" "tiger" "+")) -> ("someone" "sees" "tiger" "+"))
If someone chases the rabbit then the rabbit chases the cat.
((("someone" "chases" "rabbit" "+")) -> ("rabbit" "chases" "cat" "+"))
If someone chases the tiger and they are not green then the tiger sees the cat.
((("someone" "chases" "tiger" "+") ("someone" "is" "green" "~")) -> ("tiger" "sees" "cat" "+"))
If the tiger eats the squirrel then the tiger sees the squirrel.
((("tiger" "eats" "squirrel" "+")) -> ("tiger" "sees" "squirrel" "+"))
All nice people are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
The rabbit is nice.
True
1
proof
[(triple2)]
("rabbit" "is" "nice" "+")
triple2
The tiger is not nice.
False
1
inv-proof
[(triple4)]
("tiger" "is" "nice" "-")
triple4
The tiger is rough.
True
2
proof
[(((triple4) -> rule8))]
("tiger" "is" "rough" "+")
((triple4) -> (rule8 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is not rough.
False
2
inv-proof
[(((triple4) -> rule8))]
("tiger" "is" "rough" "-")
((triple4) -> (rule8 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The rabbit eats the squirrel.
True
3
proof
[(((((triple2) -> rule8)) -> rule1))]
("rabbit" "eats" "squirrel" "+")
((((triple2) -> (rule8 % int2))) -> (rule1 % int1))
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The tiger does not eat the squirrel.
False
3
inv-proof
[(((((triple4) -> rule8)) -> rule1))]
("tiger" "eats" "squirrel" "-")
((((triple4) -> (rule8 % int2))) -> (rule1 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger sees the squirrel.
True
4
proof
[(((((((triple4) -> rule8)) -> rule1)) -> rule7))]
("tiger" "sees" "squirrel" "+")
((((((triple4) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int2
The tiger is rough.
("tiger" "is" "rough" "+")
int3
The tiger does not see the squirrel.
False
4
inv-proof
[(((((((triple4) -> rule8)) -> rule1)) -> rule7))]
("tiger" "sees" "squirrel" "-")
((((((triple4) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int2
The tiger is rough.
("tiger" "is" "rough" "+")
int3
The cat does not see the tiger.
Unknown
inv-rconc
[@1: The cat sees the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "sees" "tiger" "-")
The squirrel chases the squirrel.
Unknown
rconc
[@1: The squirrel chases the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "chases" "squirrel" "+")
The cat does not eat the squirrel.
Unknown
inv-rconc
[@1: The cat eats the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "eats" "squirrel" "-")
The tiger chases the squirrel.
Unknown
rconc
[@1: The tiger chases the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "chases" "squirrel" "+")
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
The tiger does not see the rabbit.
Unknown
inv-random
[@0: The tiger sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "rabbit" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
@0: The cat is not rough.[(triple1)] The rabbit is nice.[(triple2)] The squirrel is green.[(triple3)] The tiger is nice.[(triple4)] @1: The rabbit is rough.[(((triple2) -> rule8))] The tiger is rough.[(((triple4) -> rule8))] @2: The rabbit eats the squirrel.[(((((triple2) -> rule8)) -> rule1))] The tiger eats the squirrel.[(((((triple4) -> rule8)) -> rule1))] @3: The tiger sees the squirrel.[(((((((triple4) -> rule8)) -> rule1)) -> rule7))]
The cat is not rough.
("cat" "is" "rough" "-")
triple1
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple2
The squirrel is green.
("squirrel" "is" "green" "+")
triple3
The tiger is nice.
("tiger" "is" "nice" "+")
triple4
The rabbit is rough.
("rabbit" "is" "rough" "+")
((triple2) -> (rule8 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
((triple4) -> (rule8 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
((((triple2) -> (rule8 % int2))) -> (rule1 % int1))
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
((((triple4) -> (rule8 % int2))) -> (rule1 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
((((((triple4) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int2
The tiger is rough.
("tiger" "is" "rough" "+")
int3