Erin is blue. Erin is kind. Erin is quiet. Erin is rough. Erin is round. Erin is smart. Erin is white. Gary is blue. Gary is rough. Gary is round. Harry is blue. Harry is kind. Harry is quiet. Harry is rough. Harry is smart. If someone is quiet then they are blue. If someone is quiet then they are kind. If Harry is white then Harry is smart. Rough people are smart. Quiet, white people are round. All kind, round people are blue.
Erin is blue.
("Erin" "is" "blue" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is quiet then they are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
If someone is quiet then they are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
If Harry is white then Harry is smart.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "smart" "+"))
Rough people are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
Quiet, white people are round.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
All kind, round people are blue.
((("someone" "is" "kind" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
Erin is smart.
True
1
proof
[(triple6 OR ((triple4) -> rule4))]
("Erin" "is" "smart" "+")
triple6
((triple4) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Harry is not kind.
False
1
inv-proof
[(triple12 OR ((triple13) -> rule2))]
("Harry" "is" "kind" "-")
triple12
((triple13) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not round.
Unknown
inv-rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "round" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
@0: Erin is blue.[(triple1 OR ((triple3) -> rule1) OR ((triple2 triple5) -> rule6) OR ((triple2 ((triple3 triple7) -> rule5)) -> rule6) OR ((((triple3) -> rule2) triple5) -> rule6) OR ((((triple3) -> rule2) ((triple3 triple7) -> rule5)) -> rule6))] Erin is kind.[(triple2 OR ((triple3) -> rule2))] Erin is quiet.[(triple3)] Erin is rough.[(triple4)] Erin is round.[(triple5 OR ((triple3 triple7) -> rule5))] Erin is smart.[(triple6 OR ((triple4) -> rule4))] Erin is white.[(triple7)] Gary is blue.[(triple8)] Gary is rough.[(triple9)] Gary is round.[(triple10)] Harry is blue.[(triple11 OR ((triple13) -> rule1))] Harry is kind.[(triple12 OR ((triple13) -> rule2))] Harry is quiet.[(triple13)] Harry is rough.[(triple14)] Harry is smart.[(triple15 OR ((triple14) -> rule4))] @1: Gary is smart.[(((triple9) -> rule4))]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
((triple3) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple2 triple5) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple2 ((triple3 triple7) -> (rule5 % int2))) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple3) -> (rule2 % int2)) triple5) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple3) -> (rule2 % int3)) ((triple3 triple7) -> (rule5 % int2))) -> (rule6 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
triple2
((triple3) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Erin is rough.
("Erin" "is" "rough" "+")
triple4
Erin is round.
("Erin" "is" "round" "+")
triple5
((triple3 triple7) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple6
((triple4) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple7
Gary is blue.
("Gary" "is" "blue" "+")
triple8
Gary is rough.
("Gary" "is" "rough" "+")
triple9
Gary is round.
("Gary" "is" "round" "+")
triple10
Harry is blue.
("Harry" "is" "blue" "+")
triple11
((triple13) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple12
((triple13) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
Harry is rough.
("Harry" "is" "rough" "+")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple15
((triple14) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple9) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1