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