The rabbit chases the tiger. The rabbit is big. The rabbit is green. The rabbit is not nice. The rabbit is round. The rabbit needs the tiger. The rabbit sees the tiger. The tiger chases the rabbit. The tiger is young. The tiger does not need the rabbit. If something chases the tiger then the tiger does not need the rabbit. If something sees the rabbit and it is round then the rabbit chases the tiger. If something chases the tiger and it does not chase the rabbit then it needs the rabbit. If something is nice then it does not need the rabbit. If the rabbit needs the tiger and the tiger does not chase the rabbit then the rabbit sees the tiger. If the tiger chases the rabbit and the rabbit sees the tiger then the tiger is not big. If the rabbit chases the tiger and the tiger is not big then the tiger is green. If something is nice and it needs the tiger then the tiger is green.
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is not nice.
("rabbit" "is" "nice" "-")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger does not need the rabbit.
("tiger" "needs" "rabbit" "-")
If something chases the tiger then the tiger does not need the rabbit.
((("something" "chases" "tiger" "+")) -> ("tiger" "needs" "rabbit" "-"))
If something sees the rabbit and it is round then the rabbit chases the tiger.
((("something" "sees" "rabbit" "+") ("something" "is" "round" "+")) -> ("rabbit" "chases" "tiger" "+"))
If something chases the tiger and it does not chase the rabbit then it needs the rabbit.
((("something" "chases" "tiger" "+") ("something" "chases" "rabbit" "~")) -> ("something" "needs" "rabbit" "+"))
If something is nice then it does not need the rabbit.
((("something" "is" "nice" "+")) -> ("something" "needs" "rabbit" "-"))
If the rabbit needs the tiger and the tiger does not chase the rabbit then the rabbit sees the tiger.
((("rabbit" "needs" "tiger" "+") ("tiger" "chases" "rabbit" "~")) -> ("rabbit" "sees" "tiger" "+"))
If the tiger chases the rabbit and the rabbit sees the tiger then the tiger is not big.
((("tiger" "chases" "rabbit" "+") ("rabbit" "sees" "tiger" "+")) -> ("tiger" "is" "big" "-"))
If the rabbit chases the tiger and the tiger is not big then the tiger is green.
((("rabbit" "chases" "tiger" "+") ("tiger" "is" "big" "~")) -> ("tiger" "is" "green" "+"))
If something is nice and it needs the tiger then the tiger is green.
((("something" "is" "nice" "+") ("something" "needs" "tiger" "+")) -> ("tiger" "is" "green" "+"))
The rabbit is green.
True
1
proof
[(triple3)]
("rabbit" "is" "green" "+")
triple3
The rabbit does not see the tiger.
False
1
inv-proof
[(triple7)]
("rabbit" "sees" "tiger" "-")
triple7
The tiger is not big.
True
3
proof
[(((triple8 triple7) -> rule6))]
("tiger" "is" "big" "-")
((triple8 triple7) -> (rule6 % int1))
The tiger is not big.
("tiger" "is" "big" "-")
int1
The tiger is big.
False
3
inv-proof
[(((triple8 triple7) -> rule6))]
("tiger" "is" "big" "+")
((triple8 triple7) -> (rule6 % int1))
The tiger is not big.
("tiger" "is" "big" "-")
int1
The tiger is green.
True
5
proof
[(((triple1 ((triple8 triple7) -> rule6)) -> rule7))]
("tiger" "is" "green" "+")
((triple1 ((triple8 triple7) -> (rule6 % int2))) -> (rule7 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is not big.
("tiger" "is" "big" "-")
int2
The tiger is not green.
False
5
inv-proof
[(((triple1 ((triple8 triple7) -> rule6)) -> rule7))]
("tiger" "is" "green" "-")
((triple1 ((triple8 triple7) -> (rule6 % int2))) -> (rule7 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is not big.
("tiger" "is" "big" "-")
int2
The rabbit does not need the rabbit.
Unknown
inv-rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "needs" "rabbit" "-")
The rabbit is young.
Unknown
random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "+")
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
The tiger is not nice.
Unknown
inv-random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "-")
The tiger sees the rabbit.
Unknown
random
[@0: The tiger sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "rabbit" "+")
@0: The rabbit chases the tiger.[(triple1)] The rabbit is big.[(triple2)] The rabbit is green.[(triple3)] The rabbit is not nice.[(triple4)] The rabbit is round.[(triple5)] The rabbit needs the tiger.[(triple6)] The rabbit sees the tiger.[(triple7)] The tiger chases the rabbit.[(triple8)] The tiger does not need the rabbit.[(triple10 OR ((triple1) -> rule1))] The tiger is young.[(triple9)] @1: The tiger is not big.[(((triple8 triple7) -> rule6))] @2: The tiger is green.[(((triple1 ((triple8 triple7) -> rule6)) -> rule7))]
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple1
The rabbit is big.
("rabbit" "is" "big" "+")
triple2
The rabbit is green.
("rabbit" "is" "green" "+")
triple3
The rabbit is not nice.
("rabbit" "is" "nice" "-")
triple4
The rabbit is round.
("rabbit" "is" "round" "+")
triple5
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple6
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple7
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple8
The tiger does not need the rabbit.
("tiger" "needs" "rabbit" "-")
triple10
((triple1) -> (rule1 % int1))
The tiger does not need the rabbit.
("tiger" "needs" "rabbit" "-")
int1
The tiger is young.
("tiger" "is" "young" "+")
triple9
The tiger is not big.
("tiger" "is" "big" "-")
((triple8 triple7) -> (rule6 % int1))
The tiger is not big.
("tiger" "is" "big" "-")
int1
The tiger is green.
("tiger" "is" "green" "+")
((triple1 ((triple8 triple7) -> (rule6 % int2))) -> (rule7 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is not big.
("tiger" "is" "big" "-")
int2