Charlie is furry. Fiona is not cold. Harry is cold. Rough things are red. All cold, furry things are rough. If something is green then it is rough. Furry things are not rough. If something is cold then it is rough. All young things are not rough. If Harry is young and Harry is red then Harry is green. All smart, young things are not green.
Charlie is furry.
("Charlie" "is" "furry" "+")
Fiona is not cold.
("Fiona" "is" "cold" "-")
Harry is cold.
("Harry" "is" "cold" "+")
Rough things are red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
All cold, furry things are rough.
((("something" "is" "cold" "+") ("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
If something is green then it is rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
Furry things are not rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "-"))
If something is cold then it is rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
All young things are not rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "-"))
If Harry is young and Harry is red then Harry is green.
((("Harry" "is" "young" "+") ("Harry" "is" "red" "+")) -> ("Harry" "is" "green" "+"))
All smart, young things are not green.
((("something" "is" "smart" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "-"))
Harry is cold.
True
1
proof
[(triple3)]
("Harry" "is" "cold" "+")
triple3
Harry is not cold.
False
1
inv-proof
[(triple3)]
("Harry" "is" "cold" "-")
triple3
Harry is rough.
True
2
proof
[(((triple3) -> rule5))]
("Harry" "is" "rough" "+")
((triple3) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Charlie is rough.
False
2
inv-proof
[(((triple1) -> rule4))]
("Charlie" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Harry is red.
True
3
proof
[(((((triple3) -> rule5)) -> rule1))]
("Harry" "is" "red" "+")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not red.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule1))]
("Harry" "is" "red" "-")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "green" "-")
Charlie is red.
Unknown
rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "red" "+")
Fiona is not red.
Unknown
inv-rconc
[@2: Fiona is red.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Fiona" "is" "red" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Charlie is furry.[(triple1)] Fiona is not cold.[(triple2)] Harry is cold.[(triple3)] @1: Charlie is not rough.[(((triple1) -> rule4))] Harry is rough.[(((triple3) -> rule5))] @2: Harry is red.[(((((triple3) -> rule5)) -> rule1))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Fiona is not cold.
("Fiona" "is" "cold" "-")
triple2
Harry is cold.
("Harry" "is" "cold" "+")
triple3
Charlie is not rough.
("Charlie" "is" "rough" "-")
((triple1) -> (rule4 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple3) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2