Charlie is kind. Charlie is not red. Dave is kind. Dave is nice. Dave is red. Fiona is furry. Fiona is quiet. Fiona is round. Harry is furry. Harry is kind. Harry is quiet. Harry is smart. If someone is kind then they are smart.
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is not red.
("Charlie" "is" "red" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is kind then they are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
Charlie is kind.
True
1
proof
[(triple1)]
("Charlie" "is" "kind" "+")
triple1
Harry is not furry.
False
1
inv-proof
[(triple9)]
("Harry" "is" "furry" "-")
triple9
Dave is smart.
True
2
proof
[(((triple3) -> rule1))]
("Dave" "is" "smart" "+")
((triple3) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Charlie is not smart.
False
2
inv-proof
[(((triple1) -> rule1))]
("Charlie" "is" "smart" "-")
((triple1) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Fiona is not smart.
Unknown
inv-rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "smart" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Charlie is kind.[(triple1)] Charlie is not red.[(triple2)] Dave is kind.[(triple3)] Dave is nice.[(triple4)] Dave is red.[(triple5)] Fiona is furry.[(triple6)] Fiona is quiet.[(triple7)] Fiona is round.[(triple8)] Harry is furry.[(triple9)] Harry is kind.[(triple10)] Harry is quiet.[(triple11)] Harry is smart.[(triple12 OR ((triple10) -> rule1))] @1: Charlie is smart.[(((triple1) -> rule1))] Dave is smart.[(((triple3) -> rule1))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Charlie is not red.
("Charlie" "is" "red" "-")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
Fiona is furry.
("Fiona" "is" "furry" "+")
triple6
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple7
Fiona is round.
("Fiona" "is" "round" "+")
triple8
Harry is furry.
("Harry" "is" "furry" "+")
triple9
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
((triple10) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple3) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1