The bear is round. Young, round people are red. All rough people are red. All young people are not rough. If someone is round then they are rough. Young, round people are green. If the bear is red and the bear is round then the bear is green.
The bear is round.
("bear" "is" "round" "+")
Young, round people are red.
((("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
All rough people are red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
All young people are not rough.
((("someone" "is" "young" "+")) -> ("someone" "is" "rough" "-"))
If someone is round then they are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
Young, round people are green.
((("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If the bear is red and the bear is round then the bear is green.
((("bear" "is" "red" "+") ("bear" "is" "round" "+")) -> ("bear" "is" "green" "+"))
The bear is round.
True
1
proof
[(triple1)]
("bear" "is" "round" "+")
triple1
The bear is not round.
False
1
inv-proof
[(triple1)]
("bear" "is" "round" "-")
triple1
The bear is rough.
True
2
proof
[(((triple1) -> rule4))]
("bear" "is" "rough" "+")
((triple1) -> (rule4 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear is not rough.
False
2
inv-proof
[(((triple1) -> rule4))]
("bear" "is" "rough" "-")
((triple1) -> (rule4 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear is red.
True
3
proof
[(((((triple1) -> rule4)) -> rule2))]
("bear" "is" "red" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear is not red.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule2))]
("bear" "is" "red" "-")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear is green.
True
5
proof
[(((((((triple1) -> rule4)) -> rule2) triple1) -> rule6))]
("bear" "is" "green" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2)) triple1) -> (rule6 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is rough.
("bear" "is" "rough" "+")
int3
The bear is not green.
False
5
inv-proof
[(((((((triple1) -> rule4)) -> rule2) triple1) -> rule6))]
("bear" "is" "green" "-")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2)) triple1) -> (rule6 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is rough.
("bear" "is" "rough" "+")
int3
The bear does not need the bear.
Unknown
inv-random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The bear is young.
Unknown
random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "+")
@0: The bear is round.[(triple1)] @1: The bear is rough.[(((triple1) -> rule4))] @2: The bear is red.[(((((triple1) -> rule4)) -> rule2))] @3: The bear is green.[(((((((triple1) -> rule4)) -> rule2) triple1) -> rule6))]
The bear is round.
("bear" "is" "round" "+")
triple1
The bear is rough.
("bear" "is" "rough" "+")
((triple1) -> (rule4 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear is red.
("bear" "is" "red" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear is green.
("bear" "is" "green" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2)) triple1) -> (rule6 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The bear is rough.
("bear" "is" "rough" "+")
int3