The rabbit is young. All young people are red. All rough people are big. If someone is red then they are big. Red people are young. If someone is red and kind then they are big. Rough, red people are big.
The rabbit is young.
("rabbit" "is" "young" "+")
All young people are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
All rough people are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
If someone is red then they are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
Red people are young.
((("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone is red and kind then they are big.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
Rough, red people are big.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
The rabbit is young.
True
1
proof
[(triple1)]
("rabbit" "is" "young" "+")
triple1
The rabbit is not young.
False
1
inv-proof
[(triple1)]
("rabbit" "is" "young" "-")
triple1
The rabbit is red.
True
2
proof
[(((triple1) -> rule1))]
("rabbit" "is" "red" "+")
((triple1) -> (rule1 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is not red.
False
2
inv-proof
[(((triple1) -> rule1))]
("rabbit" "is" "red" "-")
((triple1) -> (rule1 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is big.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("rabbit" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit is not big.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("rabbit" "is" "big" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
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 rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
The rabbit is not rough.
Unknown
inv-random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
@0: The rabbit is young.[(triple1)] @1: The rabbit is red.[(((triple1) -> rule1))] @2: The rabbit is big.[(((((triple1) -> rule1)) -> rule3))]
The rabbit is young.
("rabbit" "is" "young" "+")
triple1
The rabbit is red.
("rabbit" "is" "red" "+")
((triple1) -> (rule1 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2