Anne is smart. Erin is kind. Gary is round. If something is green and young then it is big. All big things are young. Green things are young. If Anne is green then Anne is smart. If something is smart and big then it is green. All green things are round. If something is smart then it is kind. If something is young and rough then it is smart.
Anne is smart.
("Anne" "is" "smart" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Gary is round.
("Gary" "is" "round" "+")
If something is green and young then it is big.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
All big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
Green things are young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If Anne is green then Anne is smart.
((("Anne" "is" "green" "+")) -> ("Anne" "is" "smart" "+"))
If something is smart and big then it is green.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
All green things are round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
If something is smart then it is kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
If something is young and rough then it is smart.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
Gary is round.
True
1
proof
[(triple3)]
("Gary" "is" "round" "+")
triple3
Erin is not kind.
False
1
inv-proof
[(triple2)]
("Erin" "is" "kind" "-")
triple2
Anne is kind.
True
2
proof
[(((triple1) -> rule7))]
("Anne" "is" "kind" "+")
((triple1) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not kind.
False
2
inv-proof
[(((triple1) -> rule7))]
("Anne" "is" "kind" "-")
((triple1) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not big.
Unknown
inv-rconc
[@2: Anne is big.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Anne" "is" "big" "-")
Anne is young.
Unknown
rconc
[@3: Anne is young.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule5 <- FAIL)]]
("Anne" "is" "young" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
@0: Anne is smart.[(triple1)] Erin is kind.[(triple2)] Gary is round.[(triple3)] @1: Anne is kind.[(((triple1) -> rule7))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Gary is round.
("Gary" "is" "round" "+")
triple3
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1