Erin is nice. Gary is furry. Harry is rough. All green, blue people are not rough. Blue, cold people are not green. If Harry is blue and Harry is rough then Harry is cold. If Harry is smart then Harry is furry. If someone is rough then they are blue. If someone is green then they are not nice.
Erin is nice.
("Erin" "is" "nice" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Harry is rough.
("Harry" "is" "rough" "+")
All green, blue people are not rough.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "-"))
Blue, cold people are not green.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "-"))
If Harry is blue and Harry is rough then Harry is cold.
((("Harry" "is" "blue" "+") ("Harry" "is" "rough" "+")) -> ("Harry" "is" "cold" "+"))
If Harry is smart then Harry is furry.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "furry" "+"))
If someone is rough then they are blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
If someone is green then they are not nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "-"))
Gary is furry.
True
1
proof
[(triple2)]
("Gary" "is" "furry" "+")
triple2
Erin is not nice.
False
1
inv-proof
[(triple1)]
("Erin" "is" "nice" "-")
triple1
Harry is blue.
True
2
proof
[(((triple3) -> rule5))]
("Harry" "is" "blue" "+")
((triple3) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple3) -> rule5))]
("Harry" "is" "blue" "-")
((triple3) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
True
4
proof
[(((((triple3) -> rule5) triple3) -> rule3))]
("Harry" "is" "cold" "+")
((((triple3) -> (rule5 % int2)) triple3) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not cold.
False
4
inv-proof
[(((((triple3) -> rule5) triple3) -> rule3))]
("Harry" "is" "cold" "-")
((((triple3) -> (rule5 % int2)) triple3) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not green.
True
7
proof
[(((((triple3) -> rule5) ((((triple3) -> rule5) triple3) -> rule3)) -> rule2))]
("Harry" "is" "green" "-")
((((triple3) -> (rule5 % int3)) ((((triple3) -> (rule5 % int3)) triple3) -> (rule3 % int2))) -> (rule2 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is green.
False
7
inv-proof
[(((((triple3) -> rule5) ((((triple3) -> rule5) triple3) -> rule3)) -> rule2))]
("Harry" "is" "green" "+")
((((triple3) -> (rule5 % int3)) ((((triple3) -> (rule5 % int3)) triple3) -> (rule3 % int2))) -> (rule2 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "blue" "-")
Harry is furry.
Unknown
rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "furry" "+")
Erin is not blue.
Unknown
inv-rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "blue" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
@0: Erin is nice.[(triple1)] Gary is furry.[(triple2)] Harry is rough.[(triple3)] @1: Harry is blue.[(((triple3) -> rule5))] @2: Harry is cold.[(((((triple3) -> rule5) triple3) -> rule3))] @3: Harry is not green.[(((((triple3) -> rule5) ((((triple3) -> rule5) triple3) -> rule3)) -> rule2))]
Erin is nice.
("Erin" "is" "nice" "+")
triple1
Gary is furry.
("Gary" "is" "furry" "+")
triple2
Harry is rough.
("Harry" "is" "rough" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
((triple3) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((((triple3) -> (rule5 % int2)) triple3) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not green.
("Harry" "is" "green" "-")
((((triple3) -> (rule5 % int3)) ((((triple3) -> (rule5 % int3)) triple3) -> (rule3 % int2))) -> (rule2 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3