Erin is not green. Erin is rough. Fiona is big. Fiona is rough. Gary is white. Harry is blue. Harry is furry. If Gary is not furry then Gary is rough. Blue things are not white. Rough things are blue. Green, furry things are red. If something is white and not rough then it is red. If something is white and not furry then it is not red.
Erin is not green.
("Erin" "is" "green" "-")
Erin is rough.
("Erin" "is" "rough" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
If Gary is not furry then Gary is rough.
((("Gary" "is" "furry" "~")) -> ("Gary" "is" "rough" "+"))
Blue things are not white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "-"))
Rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
Green, furry things are red.
((("something" "is" "green" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
If something is white and not rough then it is red.
((("something" "is" "white" "+") ("something" "is" "rough" "~")) -> ("something" "is" "red" "+"))
If something is white and not furry then it is not red.
((("something" "is" "white" "+") ("something" "is" "furry" "~")) -> ("something" "is" "red" "-"))
Harry is blue.
True
1
proof
[(triple6)]
("Harry" "is" "blue" "+")
triple6
Erin is green.
False
1
inv-proof
[(triple1)]
("Erin" "is" "green" "+")
triple1
Erin is blue.
True
2
proof
[(((triple2) -> rule3))]
("Erin" "is" "blue" "+")
((triple2) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Harry is white.
False
2
inv-proof
[(((triple6) -> rule2))]
("Harry" "is" "white" "+")
((triple6) -> (rule2 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Erin is not white.
True
3
proof
[(((((triple2) -> rule3)) -> rule2))]
("Erin" "is" "white" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is white.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2))]
("Erin" "is" "white" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Fiona is not red.
Unknown
inv-rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "red" "-")
Harry is red.
Unknown
rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "red" "+")
Gary is not blue.
Unknown
inv-rconc
[@2: Gary is blue.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Gary" "is" "blue" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Erin is not green.[(triple1)] Erin is rough.[(triple2)] Fiona is big.[(triple3)] Fiona is rough.[(triple4)] Gary is white.[(triple5)] Harry is blue.[(triple6)] Harry is furry.[(triple7)] @1: Erin is blue.[(((triple2) -> rule3))] Fiona is blue.[(((triple4) -> rule3))] Harry is not white.[(((triple6) -> rule2))] @2: Erin is not white.[(((((triple2) -> rule3)) -> rule2))] Fiona is not white.[(((((triple4) -> rule3)) -> rule2))]
Erin is not green.
("Erin" "is" "green" "-")
triple1
Erin is rough.
("Erin" "is" "rough" "+")
triple2
Fiona is big.
("Fiona" "is" "big" "+")
triple3
Fiona is rough.
("Fiona" "is" "rough" "+")
triple4
Gary is white.
("Gary" "is" "white" "+")
triple5
Harry is blue.
("Harry" "is" "blue" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Erin is blue.
("Erin" "is" "blue" "+")
((triple2) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple4) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Harry is not white.
("Harry" "is" "white" "-")
((triple6) -> (rule2 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Erin is not white.
("Erin" "is" "white" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Fiona is not white.
("Fiona" "is" "white" "-")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is not white.
("Fiona" "is" "white" "-")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2