Charlie is rough. Erin is cold. Gary is round. All furry people are not blue. If someone is rough then they are not furry. If Charlie is furry then Charlie is rough. If someone is rough and not furry then they are not round. Round, smart people are not quiet. If someone is quiet and not rough then they are cold. All furry people are not cold. If Erin is furry and Erin is not quiet then Erin is not blue.
Charlie is rough.
("Charlie" "is" "rough" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Gary is round.
("Gary" "is" "round" "+")
All furry people are not blue.
((("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "-"))
If someone is rough then they are not furry.
((("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "-"))
If Charlie is furry then Charlie is rough.
((("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "rough" "+"))
If someone is rough and not furry then they are not round.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "round" "-"))
Round, smart people are not quiet.
((("someone" "is" "round" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "-"))
If someone is quiet and not rough then they are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "cold" "+"))
All furry people are not cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "-"))
If Erin is furry and Erin is not quiet then Erin is not blue.
((("Erin" "is" "furry" "+") ("Erin" "is" "quiet" "~")) -> ("Erin" "is" "blue" "-"))
Gary is round.
True
1
proof
[(triple3)]
("Gary" "is" "round" "+")
triple3
Erin is not cold.
False
1
inv-proof
[(triple2)]
("Erin" "is" "cold" "-")
triple2
Charlie is not furry.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "furry" "-")
((triple1) -> (rule2 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is furry.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is not round.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule4))]
("Charlie" "is" "round" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is not furry.
("Charlie" "is" "furry" "-")
int2
Charlie is round.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule4))]
("Charlie" "is" "round" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is not furry.
("Charlie" "is" "furry" "-")
int2
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "cold" "-")
Gary is cold.
Unknown
rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "cold" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Charlie is rough.[(triple1)] Erin is cold.[(triple2)] Gary is round.[(triple3)] @1: Charlie is not furry.[(((triple1) -> rule2))] @2: Charlie is not round.[(((triple1 ((triple1) -> rule2)) -> rule4))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Gary is round.
("Gary" "is" "round" "+")
triple3
Charlie is not furry.
("Charlie" "is" "furry" "-")
((triple1) -> (rule2 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is not round.
("Charlie" "is" "round" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is not furry.
("Charlie" "is" "furry" "-")
int2