Anne is cold. Charlie is round. Erin is rough. Gary is cold. White, red people are round. If someone is rough and smart then they are blue. All cold people are smart. Red, smart people are cold. If Charlie is white and Charlie is round then Charlie is smart. All cold, round people are white. If someone is smart then they are cold. All white people are blue.
Anne is cold.
("Anne" "is" "cold" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is cold.
("Gary" "is" "cold" "+")
White, red people are round.
((("someone" "is" "white" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If someone is rough and smart then they are blue.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
All cold people are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Red, smart people are cold.
((("someone" "is" "red" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
If Charlie is white and Charlie is round then Charlie is smart.
((("Charlie" "is" "white" "+") ("Charlie" "is" "round" "+")) -> ("Charlie" "is" "smart" "+"))
All cold, round people are white.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
If someone is smart then they are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
All white people are blue.
((("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
Erin is rough.
True
1
proof
[(triple3)]
("Erin" "is" "rough" "+")
triple3
Gary is not cold.
False
1
inv-proof
[(triple4)]
("Gary" "is" "cold" "-")
triple4
Anne is smart.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Gary is not smart.
False
2
inv-proof
[(((triple4) -> rule3))]
("Gary" "is" "smart" "-")
((triple4) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Charlie is not cold.
Unknown
inv-rconc
[@4: Charlie is cold.[CWA. Example of deepest failure = (rule7 <- rule5 <- rule6 <- rule4 <- FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is blue.
Unknown
rconc
[@5: Charlie is blue.[CWA. Example of deepest failure = (rule8 <- rule6 <- rule7 <- rule3 <- rule4 <- FAIL)]]
("Charlie" "is" "blue" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Anne is cold.[(triple1)] Charlie is round.[(triple2)] Erin is rough.[(triple3)] Gary is cold.[(triple4)] @1: Anne is smart.[(((triple1) -> rule3))] Gary is smart.[(((triple4) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Erin is rough.
("Erin" "is" "rough" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple4) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1