Anne is cold. Anne is young. Charlie is cold. Charlie is furry. Dave is cold. Dave is rough. Gary is rough. Young, cold things are smart. All cold, furry things are young.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Young, cold things are smart.
((("something" "is" "young" "+") ("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
All cold, furry things are young.
((("something" "is" "cold" "+") ("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
Charlie is furry.
True
1
proof
[(triple4)]
("Charlie" "is" "furry" "+")
triple4
Gary is not rough.
False
1
inv-proof
[(triple7)]
("Gary" "is" "rough" "-")
triple7
Anne is smart.
True
3
proof
[(((triple2 triple1) -> rule1))]
("Anne" "is" "smart" "+")
((triple2 triple1) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Charlie is not young.
False
3
inv-proof
[(((triple3 triple4) -> rule2))]
("Charlie" "is" "young" "-")
((triple3 triple4) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is smart.
True
5
proof
[(((((triple3 triple4) -> rule2) triple3) -> rule1))]
("Charlie" "is" "smart" "+")
((((triple3 triple4) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not smart.
False
5
inv-proof
[(((((triple3 triple4) -> rule2) triple3) -> rule1))]
("Charlie" "is" "smart" "-")
((((triple3 triple4) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Dave is not young.
Unknown
inv-rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "young" "-")
Gary is smart.
Unknown
rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "smart" "+")
Dave is not smart.
Unknown
inv-rconc
[@2: Dave is smart.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Dave" "is" "smart" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Anne is cold.[(triple1)] Anne is young.[(triple2)] Charlie is cold.[(triple3)] Charlie is furry.[(triple4)] Dave is cold.[(triple5)] Dave is rough.[(triple6)] Gary is rough.[(triple7)] @1: Anne is smart.[(((triple2 triple1) -> rule1))] Charlie is young.[(((triple3 triple4) -> rule2))] @2: Charlie is smart.[(((((triple3 triple4) -> rule2) triple3) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Charlie is furry.
("Charlie" "is" "furry" "+")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
triple5
Dave is rough.
("Dave" "is" "rough" "+")
triple6
Gary is rough.
("Gary" "is" "rough" "+")
triple7
Anne is smart.
("Anne" "is" "smart" "+")
((triple2 triple1) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple3 triple4) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple3 triple4) -> (rule2 % int2)) triple3) -> (rule1 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2