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