Anne is furry. Anne is round. Anne is white. Dave is smart. Erin is kind. Erin is white. Harry is big. Harry is kind. Harry is rough. Harry is smart. All smart, kind things are rough. Smart things are kind.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All smart, kind things are rough.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
Smart things are kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
Erin is white.
True
1
proof
[(triple6)]
("Erin" "is" "white" "+")
triple6
Harry is not rough.
False
1
inv-proof
[(triple9 OR ((triple10 triple8) -> rule1) OR ((triple10 ((triple10) -> rule2)) -> rule1))]
("Harry" "is" "rough" "-")
triple9
((triple10 triple8) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple10 ((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Dave is kind.
True
2
proof
[(((triple4) -> rule2))]
("Dave" "is" "kind" "+")
((triple4) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not kind.
False
2
inv-proof
[(((triple4) -> rule2))]
("Dave" "is" "kind" "-")
((triple4) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
True
4
proof
[(((triple4 ((triple4) -> rule2)) -> rule1))]
("Dave" "is" "rough" "+")
((triple4 ((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not rough.
False
4
inv-proof
[(((triple4 ((triple4) -> rule2)) -> rule1))]
("Dave" "is" "rough" "-")
((triple4 ((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "kind" "-")
Erin is rough.
Unknown
rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "rough" "+")
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "rough" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
@0: Anne is furry.[(triple1)] Anne is round.[(triple2)] Anne is white.[(triple3)] Dave is smart.[(triple4)] Erin is kind.[(triple5)] Erin is white.[(triple6)] Harry is big.[(triple7)] Harry is kind.[(triple8 OR ((triple10) -> rule2))] Harry is rough.[(triple9 OR ((triple10 triple8) -> rule1) OR ((triple10 ((triple10) -> rule2)) -> rule1))] Harry is smart.[(triple10)] @1: Dave is kind.[(((triple4) -> rule2))] @2: Dave is rough.[(((triple4 ((triple4) -> rule2)) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
triple4
Erin is kind.
("Erin" "is" "kind" "+")
triple5
Erin is white.
("Erin" "is" "white" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Harry is kind.
("Harry" "is" "kind" "+")
triple8
((triple10) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple9
((triple10 triple8) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple10 ((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Dave is kind.
("Dave" "is" "kind" "+")
((triple4) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple4 ((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2