The rabbit is round. All green things are young. Round things are green. All big things are green. If the rabbit is green then the rabbit is round. All young things are not blue. If something is round and not young then it is not blue.
The rabbit is round.
("rabbit" "is" "round" "+")
All green things are young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
Round things are green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
All big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If the rabbit is green then the rabbit is round.
((("rabbit" "is" "green" "+")) -> ("rabbit" "is" "round" "+"))
All young things are not blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "-"))
If something is round and not young then it is not blue.
((("something" "is" "round" "+") ("something" "is" "young" "~")) -> ("something" "is" "blue" "-"))
The rabbit is round.
True
1
proof
[(triple1)]
("rabbit" "is" "round" "+")
triple1
The rabbit is not round.
False
1
inv-proof
[(triple1)]
("rabbit" "is" "round" "-")
triple1
The rabbit is green.
True
2
proof
[(((triple1) -> rule2))]
("rabbit" "is" "green" "+")
((triple1) -> (rule2 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is not green.
False
2
inv-proof
[(((triple1) -> rule2))]
("rabbit" "is" "green" "-")
((triple1) -> (rule2 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is young.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("rabbit" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit is not young.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("rabbit" "is" "young" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit is not blue.
True
4
proof
[(((((((triple1) -> rule2)) -> rule1)) -> rule5))]
("rabbit" "is" "blue" "-")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit is not blue.
("rabbit" "is" "blue" "-")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The rabbit is blue.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule1)) -> rule5))]
("rabbit" "is" "blue" "+")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit is not blue.
("rabbit" "is" "blue" "-")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
@0: The rabbit is round.[(triple1)] @1: The rabbit is green.[(((triple1) -> rule2))] @2: The rabbit is young.[(((((triple1) -> rule2)) -> rule1))] @3: The rabbit is not blue.[(((((((triple1) -> rule2)) -> rule1)) -> rule5))]
The rabbit is round.
("rabbit" "is" "round" "+")
triple1
The rabbit is green.
("rabbit" "is" "green" "+")
((triple1) -> (rule2 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit is not blue.
("rabbit" "is" "blue" "-")
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit is not blue.
("rabbit" "is" "blue" "-")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3