Anne is young. Bob is green. Erin is smart. Harry is young. If Harry is green then Harry is furry. If something is smart and young then it is kind. All kind things are smart. All kind, big things are green. If Harry is furry and Harry is kind then Harry is young. All smart things are big.
Anne is young.
("Anne" "is" "young" "+")
Bob is green.
("Bob" "is" "green" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is green then Harry is furry.
((("Harry" "is" "green" "+")) -> ("Harry" "is" "furry" "+"))
If something is smart and young then it is kind.
((("something" "is" "smart" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
All kind things are smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
All kind, big things are green.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If Harry is furry and Harry is kind then Harry is young.
((("Harry" "is" "furry" "+") ("Harry" "is" "kind" "+")) -> ("Harry" "is" "young" "+"))
All smart things are big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
Bob is green.
True
1
proof
[(triple2)]
("Bob" "is" "green" "+")
triple2
Anne is not young.
False
1
inv-proof
[(triple1)]
("Anne" "is" "young" "-")
triple1
Erin is big.
True
2
proof
[(((triple3) -> rule6))]
("Erin" "is" "big" "+")
((triple3) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not big.
False
2
inv-proof
[(((triple3) -> rule6))]
("Erin" "is" "big" "-")
((triple3) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is not kind.
Unknown
inv-rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "kind" "-")
Anne is kind.
Unknown
rconc
[@2: Anne is kind.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Anne" "is" "kind" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is young.[(triple1)] Bob is green.[(triple2)] Erin is smart.[(triple3)] Harry is young.[(triple4)] @1: Erin is big.[(((triple3) -> rule6))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Harry is young.
("Harry" "is" "young" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
((triple3) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1