Bob is nice. Erin is white. Fiona is nice. Harry is kind. White things are not round. All nice things are round. All smart, kind things are not red. Smart things are white. If Harry is kind and Harry is nice then Harry is round. If something is round and not white then it is young.
Bob is nice.
("Bob" "is" "nice" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Harry is kind.
("Harry" "is" "kind" "+")
White things are not round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "-"))
All nice things are round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
All smart, kind things are not red.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "-"))
Smart things are white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If Harry is kind and Harry is nice then Harry is round.
((("Harry" "is" "kind" "+") ("Harry" "is" "nice" "+")) -> ("Harry" "is" "round" "+"))
If something is round and not white then it is young.
((("something" "is" "round" "+") ("something" "is" "white" "~")) -> ("something" "is" "young" "+"))
Erin is white.
True
1
proof
[(triple2)]
("Erin" "is" "white" "+")
triple2
Harry is not kind.
False
1
inv-proof
[(triple4)]
("Harry" "is" "kind" "-")
triple4
Fiona is round.
True
2
proof
[(((triple3) -> rule2))]
("Fiona" "is" "round" "+")
((triple3) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "round" "-")
((triple1) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Harry is not young.
Unknown
inv-rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "young" "-")
Harry is white.
Unknown
rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "white" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
@0: Bob is nice.[(triple1)] Erin is white.[(triple2)] Fiona is nice.[(triple3)] Harry is kind.[(triple4)] @1: Bob is round.[(((triple1) -> rule2))] Erin is not round.[(((triple2) -> rule1))] Fiona is round.[(((triple3) -> rule2))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Erin is white.
("Erin" "is" "white" "+")
triple2
Fiona is nice.
("Fiona" "is" "nice" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Erin is not round.
("Erin" "is" "round" "-")
((triple2) -> (rule1 % int1))
Erin is not round.
("Erin" "is" "round" "-")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((triple3) -> (rule2 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1