Bob is kind. Charlie is not furry. Erin is big. Fiona is blue. Kind people are not cold. All kind, young people are blue. If someone is young and not cold then they are smart.
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Erin is big.
("Erin" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Kind people are not cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "-"))
All kind, young people are blue.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
If someone is young and not cold then they are smart.
((("someone" "is" "young" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "smart" "+"))
Fiona is blue.
True
1
proof
[(triple4)]
("Fiona" "is" "blue" "+")
triple4
Charlie is furry.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "furry" "+")
triple2
Bob is not cold.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "cold" "-")
((triple1) -> (rule1 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Bob is cold.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "cold" "+")
((triple1) -> (rule1 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Erin is not blue.
Unknown
inv-rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "blue" "-")
Fiona is smart.
Unknown
rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "smart" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
@0: Bob is kind.[(triple1)] Charlie is not furry.[(triple2)] Erin is big.[(triple3)] Fiona is blue.[(triple4)] @1: Bob is not cold.[(((triple1) -> rule1))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple2
Erin is big.
("Erin" "is" "big" "+")
triple3
Fiona is blue.
("Fiona" "is" "blue" "+")
triple4
Bob is not cold.
("Bob" "is" "cold" "-")
((triple1) -> (rule1 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1