Charlie is green. Erin is furry. Gary is rough. All rough people are green. If someone is furry and green then they are blue. Green people are not smart.
Charlie is green.
("Charlie" "is" "green" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Gary is rough.
("Gary" "is" "rough" "+")
All rough people are green.
((("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
If someone is furry and green then they are blue.
((("someone" "is" "furry" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
Green people are not smart.
((("someone" "is" "green" "+")) -> ("someone" "is" "smart" "-"))
Erin is furry.
True
1
proof
[(triple2)]
("Erin" "is" "furry" "+")
triple2
Charlie is not green.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "green" "-")
triple1
Gary is green.
True
2
proof
[(((triple3) -> rule1))]
("Gary" "is" "green" "+")
((triple3) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Charlie is smart.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Gary is not smart.
True
3
proof
[(((((triple3) -> rule1)) -> rule3))]
("Gary" "is" "smart" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Gary is not smart.
("Gary" "is" "smart" "-")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is smart.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule3))]
("Gary" "is" "smart" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Gary is not smart.
("Gary" "is" "smart" "-")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Erin is not green.
Unknown
inv-rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "green" "-")
Gary is blue.
Unknown
rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "blue" "+")
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "blue" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
@0: Charlie is green.[(triple1)] Erin is furry.[(triple2)] Gary is rough.[(triple3)] @1: Charlie is not smart.[(((triple1) -> rule3))] Gary is green.[(((triple3) -> rule1))] @2: Gary is not smart.[(((((triple3) -> rule1)) -> rule3))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
Gary is rough.
("Gary" "is" "rough" "+")
triple3
Charlie is not smart.
("Charlie" "is" "smart" "-")
((triple1) -> (rule3 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple3) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not smart.
("Gary" "is" "smart" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Gary is not smart.
("Gary" "is" "smart" "-")
int1
Gary is green.
("Gary" "is" "green" "+")
int2