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