Bob is nice. Erin is rough. Fiona is round. If someone is round then they are smart. All round, blue people are kind. If Bob is smart then Bob is rough.
Bob is nice.
("Bob" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Fiona is round.
("Fiona" "is" "round" "+")
If someone is round then they are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
All round, blue people are kind.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If Bob is smart then Bob is rough.
((("Bob" "is" "smart" "+")) -> ("Bob" "is" "rough" "+"))
Erin is rough.
True
1
proof
[(triple2)]
("Erin" "is" "rough" "+")
triple2
Fiona is not round.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "round" "-")
triple3
Fiona is smart.
True
2
proof
[(((triple3) -> rule1))]
("Fiona" "is" "smart" "+")
((triple3) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is not smart.
False
2
inv-proof
[(((triple3) -> rule1))]
("Fiona" "is" "smart" "-")
((triple3) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Erin is not kind.
Unknown
inv-rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "kind" "-")
Bob is smart.
Unknown
rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "smart" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is nice.[(triple1)] Erin is rough.[(triple2)] Fiona is round.[(triple3)] @1: Fiona is smart.[(((triple3) -> rule1))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Erin is rough.
("Erin" "is" "rough" "+")
triple2
Fiona is round.
("Fiona" "is" "round" "+")
triple3
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple3) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1