Charlie is not cold. Dave is big. Fiona is rough. Harry is furry. All rough, furry people are green. Smart, furry people are green. If Harry is rough and Harry is furry then Harry is big. Furry people are smart. Cold, blue people are not big. All blue people are not cold. All cold, smart people are not blue. If someone is big then they are not rough.
Charlie is not cold.
("Charlie" "is" "cold" "-")
Dave is big.
("Dave" "is" "big" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Harry is furry.
("Harry" "is" "furry" "+")
All rough, furry people are green.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
Smart, furry people are green.
((("someone" "is" "smart" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
If Harry is rough and Harry is furry then Harry is big.
((("Harry" "is" "rough" "+") ("Harry" "is" "furry" "+")) -> ("Harry" "is" "big" "+"))
Furry people are smart.
((("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
Cold, blue people are not big.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "big" "-"))
All blue people are not cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "-"))
All cold, smart people are not blue.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "-"))
If someone is big then they are not rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "-"))
Charlie is not cold.
True
1
proof
[(triple1)]
("Charlie" "is" "cold" "-")
triple1
Fiona is not rough.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "rough" "-")
triple3
Dave is not rough.
True
2
proof
[(((triple2) -> rule8))]
("Dave" "is" "rough" "-")
((triple2) -> (rule8 % int1))
Dave is not rough.
("Dave" "is" "rough" "-")
int1
Harry is not smart.
False
2
inv-proof
[(((triple4) -> rule4))]
("Harry" "is" "smart" "-")
((triple4) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is green.
True
4
proof
[(((((triple4) -> rule4) triple4) -> rule2))]
("Harry" "is" "green" "+")
((((triple4) -> (rule4 % int2)) triple4) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not green.
False
4
inv-proof
[(((((triple4) -> rule4) triple4) -> rule2))]
("Harry" "is" "green" "-")
((((triple4) -> (rule4 % int2)) triple4) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "green" "-")
Fiona is green.
Unknown
rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "green" "+")
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "smart" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Charlie is not cold.[(triple1)] Dave is big.[(triple2)] Fiona is rough.[(triple3)] Harry is furry.[(triple4)] @1: Dave is not rough.[(((triple2) -> rule8))] Harry is smart.[(((triple4) -> rule4))] @2: Harry is green.[(((((triple4) -> rule4) triple4) -> rule2))]
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
Dave is not rough.
("Dave" "is" "rough" "-")
((triple2) -> (rule8 % int1))
Dave is not rough.
("Dave" "is" "rough" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple4) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((((triple4) -> (rule4 % int2)) triple4) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2