Anne is round. Fiona is young. Harry is kind. Green, round people are smart. Kind people are smart. If Harry is smart then Harry is young. If someone is young then they are smart. All round, big people are kind. If someone is big and green then they are round.
Anne is round.
("Anne" "is" "round" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Green, round people are smart.
((("someone" "is" "green" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
Kind people are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If Harry is smart then Harry is young.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "young" "+"))
If someone is young then they are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
All round, big people are kind.
((("someone" "is" "round" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
If someone is big and green then they are round.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
Harry is kind.
True
1
proof
[(triple3)]
("Harry" "is" "kind" "+")
triple3
Fiona is not young.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "young" "-")
triple2
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 not round.
Unknown
inv-rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "round" "-")
Anne is kind.
Unknown
rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "kind" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
@0: Anne is round.[(triple1)] Fiona is young.[(triple2)] Harry is kind.[(triple3)] @1: Fiona is smart.[(((triple2) -> rule4))] Harry is smart.[(((triple3) -> rule2))] @2: Harry is young.[(((((triple3) -> rule2)) -> rule3))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Fiona is young.
("Fiona" "is" "young" "+")
triple2
Harry is kind.
("Harry" "is" "kind" "+")
triple3
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple2) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple3) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2