Bob is nice. Bob is quiet. Charlie is blue. Charlie is green. Charlie is nice. Charlie is red. Charlie is round. Erin is blue. Erin is green. Erin is kind. Erin is nice. Erin is red. Harry is blue. Harry is kind. Harry is quiet. Harry is red. Blue people are round. If someone is blue then they are kind.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Blue people are round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If someone is blue then they are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
Harry is blue.
True
1
proof
[(triple13)]
("Harry" "is" "blue" "+")
triple13
Charlie is not green.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "green" "-")
triple4
Charlie is kind.
True
2
proof
[(((triple3) -> rule2))]
("Charlie" "is" "kind" "+")
((triple3) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not kind.
False
2
inv-proof
[(((triple3) -> rule2))]
("Charlie" "is" "kind" "-")
((triple3) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Bob is not kind.
Unknown
inv-rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "kind" "-")
Bob is round.
Unknown
rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "round" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Bob is nice.[(triple1)] Bob is quiet.[(triple2)] Charlie is blue.[(triple3)] Charlie is green.[(triple4)] Charlie is nice.[(triple5)] Charlie is red.[(triple6)] Charlie is round.[(triple7 OR ((triple3) -> rule1))] Erin is blue.[(triple8)] Erin is green.[(triple9)] Erin is kind.[(triple10 OR ((triple8) -> rule2))] Erin is nice.[(triple11)] Erin is red.[(triple12)] Harry is blue.[(triple13)] Harry is kind.[(triple14 OR ((triple13) -> rule2))] Harry is quiet.[(triple15)] Harry is red.[(triple16)] @1: Charlie is kind.[(((triple3) -> rule2))] Erin is round.[(((triple8) -> rule1))] Harry is round.[(((triple13) -> rule1))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
triple4
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple6
Charlie is round.
("Charlie" "is" "round" "+")
triple7
((triple3) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple8
Erin is green.
("Erin" "is" "green" "+")
triple9
Erin is kind.
("Erin" "is" "kind" "+")
triple10
((triple8) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple11
Erin is red.
("Erin" "is" "red" "+")
triple12
Harry is blue.
("Harry" "is" "blue" "+")
triple13
Harry is kind.
("Harry" "is" "kind" "+")
triple14
((triple13) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple15
Harry is red.
("Harry" "is" "red" "+")
triple16
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple3) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((triple8) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple13) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1