The rabbit eats the tiger. The rabbit is big. The rabbit is kind. The rabbit is round. The rabbit is young. The rabbit needs the tiger. The rabbit sees the tiger. The tiger eats the rabbit. The tiger is big. The tiger is cold. The tiger is kind. The tiger is round. The tiger is young. The tiger needs the rabbit. The tiger sees the rabbit. If something eats the tiger then it is young. If something sees the tiger then the tiger sees the rabbit. If something sees the tiger then it is cold. If something is kind and young then it needs the rabbit. All round things are cold. If the tiger is big and the tiger is young then the tiger needs the rabbit.
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If something eats the tiger then it is young.
((("something" "eats" "tiger" "+")) -> ("something" "is" "young" "+"))
If something sees the tiger then the tiger sees the rabbit.
((("something" "sees" "tiger" "+")) -> ("tiger" "sees" "rabbit" "+"))
If something sees the tiger then it is cold.
((("something" "sees" "tiger" "+")) -> ("something" "is" "cold" "+"))
If something is kind and young then it needs the rabbit.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "needs" "rabbit" "+"))
All round things are cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If the tiger is big and the tiger is young then the tiger needs the rabbit.
((("tiger" "is" "big" "+") ("tiger" "is" "young" "+")) -> ("tiger" "needs" "rabbit" "+"))
The tiger is big.
True
1
proof
[(triple9)]
("tiger" "is" "big" "+")
triple9
The rabbit is not kind.
False
1
inv-proof
[(triple3)]
("rabbit" "is" "kind" "-")
triple3
The rabbit needs the rabbit.
True
3
proof
[(((triple3 triple5) -> rule4) OR ((triple3 ((triple1) -> rule1)) -> rule4))]
("rabbit" "needs" "rabbit" "+")
((triple3 triple5) -> (rule4 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
((triple3 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit is not cold.
False
2
inv-proof
[(((triple4) -> rule5) OR ((triple7) -> rule3))]
("rabbit" "is" "cold" "-")
((triple4) -> (rule5 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
((triple7) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit does not eat the rabbit.
Unknown
inv-random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
@0: The rabbit eats the tiger.[(triple1)] The rabbit is big.[(triple2)] The rabbit is kind.[(triple3)] The rabbit is round.[(triple4)] The rabbit is young.[(triple5 OR ((triple1) -> rule1))] The rabbit needs the tiger.[(triple6)] The rabbit sees the tiger.[(triple7)] The tiger eats the rabbit.[(triple8)] The tiger is big.[(triple9)] The tiger is cold.[(triple10 OR ((triple12) -> rule5))] The tiger is kind.[(triple11)] The tiger is round.[(triple12)] The tiger is young.[(triple13)] The tiger needs the rabbit.[(triple14 OR ((triple11 triple13) -> rule4) OR ((triple9 triple13) -> rule6))] The tiger sees the rabbit.[(triple15 OR ((triple7) -> rule2))] @1: The rabbit is cold.[(((triple4) -> rule5) OR ((triple7) -> rule3))] The rabbit needs the rabbit.[(((triple3 triple5) -> rule4) OR ((triple3 ((triple1) -> rule1)) -> rule4))]
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple1
The rabbit is big.
("rabbit" "is" "big" "+")
triple2
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple3
The rabbit is round.
("rabbit" "is" "round" "+")
triple4
The rabbit is young.
("rabbit" "is" "young" "+")
triple5
((triple1) -> (rule1 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple6
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple7
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple8
The tiger is big.
("tiger" "is" "big" "+")
triple9
The tiger is cold.
("tiger" "is" "cold" "+")
triple10
((triple12) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
triple11
The tiger is round.
("tiger" "is" "round" "+")
triple12
The tiger is young.
("tiger" "is" "young" "+")
triple13
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple14
((triple11 triple13) -> (rule4 % int1))
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int1
((triple9 triple13) -> (rule6 % int1))
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple15
((triple7) -> (rule2 % int1))
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
((triple4) -> (rule5 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
((triple7) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple3 triple5) -> (rule4 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
((triple3 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2