Anne is green. Charlie is not rough. Gary is young. If someone is big then they are young. Quiet people are young. All green people are big. Rough, green people are white. Furry people are not rough. If someone is white and not young then they are not furry. If someone is rough then they are not furry. All rough, young people are furry.
Anne is green.
("Anne" "is" "green" "+")
Charlie is not rough.
("Charlie" "is" "rough" "-")
Gary is young.
("Gary" "is" "young" "+")
If someone is big then they are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
Quiet people are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
All green people are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
Rough, green people are white.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
Furry people are not rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "-"))
If someone is white and not young then they are not furry.
((("someone" "is" "white" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "furry" "-"))
If someone is rough then they are not furry.
((("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "-"))
All rough, young people are furry.
((("someone" "is" "rough" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
Anne is green.
True
1
proof
[(triple1)]
("Anne" "is" "green" "+")
triple1
Gary is not young.
False
1
inv-proof
[(triple3)]
("Gary" "is" "young" "-")
triple3
Anne is big.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "big" "+")
((triple1) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "big" "-")
((triple1) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is young.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Anne" "is" "young" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not young.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Anne" "is" "young" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "white" "-")
Charlie is young.
Unknown
rconc
[@2: Charlie is young.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Charlie" "is" "young" "+")
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "big" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Anne is green.[(triple1)] Charlie is not rough.[(triple2)] Gary is young.[(triple3)] @1: Anne is big.[(((triple1) -> rule3))] @2: Anne is young.[(((((triple1) -> rule3)) -> rule1))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Charlie is not rough.
("Charlie" "is" "rough" "-")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2