Charlie is cold. Charlie is furry. Charlie is round. Charlie is not smart. Erin is furry. Erin is not red. Erin is white. Furry, white things are smart. Smart, cold things are furry. If something is smart then it is cold. All smart, red things are cold. All smart, round things are not red. Young things are white.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is not smart.
("Charlie" "is" "smart" "-")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is not red.
("Erin" "is" "red" "-")
Erin is white.
("Erin" "is" "white" "+")
Furry, white things are smart.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
Smart, cold things are furry.
((("something" "is" "smart" "+") ("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
If something is smart then it is cold.
((("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
All smart, red things are cold.
((("something" "is" "smart" "+") ("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
All smart, round things are not red.
((("something" "is" "smart" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "-"))
Young things are white.
((("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
Erin is furry.
True
1
proof
[(triple5)]
("Erin" "is" "furry" "+")
triple5
Charlie is not furry.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "furry" "-")
triple2
Erin is smart.
True
3
proof
[(((triple5 triple7) -> rule1))]
("Erin" "is" "smart" "+")
((triple5 triple7) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not smart.
False
3
inv-proof
[(((triple5 triple7) -> rule1))]
("Erin" "is" "smart" "-")
((triple5 triple7) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "white" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
@0: Charlie is cold.[(triple1)] Charlie is furry.[(triple2)] Charlie is not smart.[(triple4)] Charlie is round.[(triple3)] Erin is furry.[(triple5)] Erin is not red.[(triple6)] Erin is white.[(triple7)] @1: Erin is smart.[(((triple5 triple7) -> rule1))] @2: Erin is cold.[(((((triple5 triple7) -> rule1)) -> rule3))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple4
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Erin is furry.
("Erin" "is" "furry" "+")
triple5
Erin is not red.
("Erin" "is" "red" "-")
triple6
Erin is white.
("Erin" "is" "white" "+")
triple7
Erin is smart.
("Erin" "is" "smart" "+")
((triple5 triple7) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((((triple5 triple7) -> (rule1 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2