Bob is kind. Bob is round. Charlie is cold. Charlie is red. Dave is kind. Harry is red. Harry is round. If someone is red then they are kind. If Charlie is cold then Charlie is not nice. Smart, nice people are round.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
If someone is red then they are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
If Charlie is cold then Charlie is not nice.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "nice" "-"))
Smart, nice people are round.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
Harry is round.
True
1
proof
[(triple7)]
("Harry" "is" "round" "+")
triple7
Harry is not round.
False
1
inv-proof
[(triple7)]
("Harry" "is" "round" "-")
triple7
Charlie is kind.
True
2
proof
[(((triple4) -> rule1))]
("Charlie" "is" "kind" "+")
((triple4) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
False
2
inv-proof
[(((triple3) -> rule2))]
("Charlie" "is" "nice" "+")
((triple3) -> (rule2 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "round" "-")
Dave is round.
Unknown
rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "round" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Bob is kind.[(triple1)] Bob is round.[(triple2)] Charlie is cold.[(triple3)] Charlie is red.[(triple4)] Dave is kind.[(triple5)] Harry is red.[(triple6)] Harry is round.[(triple7)] @1: Charlie is kind.[(((triple4) -> rule1))] Charlie is not nice.[(((triple3) -> rule2))] Harry is kind.[(((triple6) -> rule1))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Harry is red.
("Harry" "is" "red" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple4) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not nice.
("Charlie" "is" "nice" "-")
((triple3) -> (rule2 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple6) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1