Erin is not blue. Erin is cold. Erin is green. Erin is nice. Erin is not quiet. Erin is not red. Erin is rough. Gary is blue. Gary is cold. Gary is green. Gary is red. Gary is rough. Harry is not blue. Harry is green. Harry is nice. Harry is quiet. All rough, blue people are green. Blue, nice people are green. All quiet people are nice. All green people are rough. If Harry is red then Harry is blue. If someone is nice and not blue then they are cold.
Erin is not blue.
("Erin" "is" "blue" "-")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is not quiet.
("Erin" "is" "quiet" "-")
Erin is not red.
("Erin" "is" "red" "-")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is not blue.
("Harry" "is" "blue" "-")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
All rough, blue people are green.
((("someone" "is" "rough" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
Blue, nice people are green.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
All quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
All green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If Harry is red then Harry is blue.
((("Harry" "is" "red" "+")) -> ("Harry" "is" "blue" "+"))
If someone is nice and not blue then they are cold.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "cold" "+"))
Gary is blue.
True
1
proof
[(triple8)]
("Gary" "is" "blue" "+")
triple8
Gary is not rough.
False
1
inv-proof
[(triple12 OR ((triple10) -> rule4))]
("Gary" "is" "rough" "-")
triple12
((triple10) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Harry is rough.
True
2
proof
[(((triple14) -> rule4))]
("Harry" "is" "rough" "+")
((triple14) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not cold.
False
3
inv-proof
[(((triple15 triple13) -> rule6) OR ((((triple16) -> rule3) triple13) -> rule6))]
("Harry" "is" "cold" "-")
((triple15 triple13) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple16) -> (rule3 % int2)) triple13) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "nice" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Erin is cold.[(triple2 OR ((triple4 triple1) -> rule6))] Erin is green.[(triple3)] Erin is nice.[(triple4)] Erin is not blue.[(triple1)] Erin is not quiet.[(triple5)] Erin is not red.[(triple6)] Erin is rough.[(triple7 OR ((triple3) -> rule4))] Gary is blue.[(triple8)] Gary is cold.[(triple9)] Gary is green.[(triple10 OR ((triple12 triple8) -> rule1))] Gary is red.[(triple11)] Gary is rough.[(triple12 OR ((triple10) -> rule4))] Harry is green.[(triple14)] Harry is nice.[(triple15 OR ((triple16) -> rule3))] Harry is not blue.[(triple13)] Harry is quiet.[(triple16)] @1: Harry is cold.[(((triple15 triple13) -> rule6) OR ((((triple16) -> rule3) triple13) -> rule6))] Harry is rough.[(((triple14) -> rule4))]
Erin is cold.
("Erin" "is" "cold" "+")
triple2
((triple4 triple1) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Erin is not blue.
("Erin" "is" "blue" "-")
triple1
Erin is not quiet.
("Erin" "is" "quiet" "-")
triple5
Erin is not red.
("Erin" "is" "red" "-")
triple6
Erin is rough.
("Erin" "is" "rough" "+")
triple7
((triple3) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple8
Gary is cold.
("Gary" "is" "cold" "+")
triple9
Gary is green.
("Gary" "is" "green" "+")
triple10
((triple12 triple8) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
triple11
Gary is rough.
("Gary" "is" "rough" "+")
triple12
((triple10) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple14
Harry is nice.
("Harry" "is" "nice" "+")
triple15
((triple16) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not blue.
("Harry" "is" "blue" "-")
triple13
Harry is quiet.
("Harry" "is" "quiet" "+")
triple16
Harry is cold.
("Harry" "is" "cold" "+")
((triple15 triple13) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple16) -> (rule3 % int2)) triple13) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((triple14) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1