Erin is rough. Gary is cold. Harry is rough. If someone is rough then they are not round. All kind, red people are rough. All cold people are rough. If Harry is round and Harry is smart then Harry is kind. If someone is round then they are smart. Round, rough people are not smart.
Erin is rough.
("Erin" "is" "rough" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If someone is rough then they are not round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "-"))
All kind, red people are rough.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
All cold people are rough.
((("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
If Harry is round and Harry is smart then Harry is kind.
((("Harry" "is" "round" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "kind" "+"))
If someone is round then they are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
Round, rough people are not smart.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "-"))
Erin is rough.
True
1
proof
[(triple1)]
("Erin" "is" "rough" "+")
triple1
Harry is not rough.
False
1
inv-proof
[(triple3)]
("Harry" "is" "rough" "-")
triple3
Gary is rough.
True
2
proof
[(((triple2) -> rule3))]
("Gary" "is" "rough" "+")
((triple2) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not rough.
False
2
inv-proof
[(((triple2) -> rule3))]
("Gary" "is" "rough" "-")
((triple2) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not round.
True
3
proof
[(((((triple2) -> rule3)) -> rule1))]
("Gary" "is" "round" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is round.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1))]
("Gary" "is" "round" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "smart" "-")
Erin is smart.
Unknown
rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "smart" "+")
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "kind" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Erin is rough.[(triple1)] Gary is cold.[(triple2)] Harry is rough.[(triple3)] @1: Erin is not round.[(((triple1) -> rule1))] Gary is rough.[(((triple2) -> rule3))] Harry is not round.[(((triple3) -> rule1))] @2: Gary is not round.[(((((triple2) -> rule3)) -> rule1))]
Erin is rough.
("Erin" "is" "rough" "+")
triple1
Gary is cold.
("Gary" "is" "cold" "+")
triple2
Harry is rough.
("Harry" "is" "rough" "+")
triple3
Erin is not round.
("Erin" "is" "round" "-")
((triple1) -> (rule1 % int1))
Erin is not round.
("Erin" "is" "round" "-")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple2) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Harry is not round.
("Harry" "is" "round" "-")
((triple3) -> (rule1 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
Gary is not round.
("Gary" "is" "round" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2