Anne is furry. Bob is round. Fiona is smart. Smart, round people are furry. If someone is cold and round then they are smart. If Anne is smart then Anne is round. If someone is round then they are smart. Round, kind people are rough. Round, furry people are kind.
Anne is furry.
("Anne" "is" "furry" "+")
Bob is round.
("Bob" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Smart, round people are furry.
((("someone" "is" "smart" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
If someone is cold and round then they are smart.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
If Anne is smart then Anne is round.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "round" "+"))
If someone is round then they are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
Round, kind people are rough.
((("someone" "is" "round" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
Round, furry people are kind.
((("someone" "is" "round" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Anne is not furry.
False
1
inv-proof
[(triple1)]
("Anne" "is" "furry" "-")
triple1
Bob is smart.
True
2
proof
[(((triple2) -> rule4))]
("Bob" "is" "smart" "+")
((triple2) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not smart.
False
2
inv-proof
[(((triple2) -> rule4))]
("Bob" "is" "smart" "-")
((triple2) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is furry.
True
4
proof
[(((((triple2) -> rule4) triple2) -> rule1))]
("Bob" "is" "furry" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not furry.
False
4
inv-proof
[(((((triple2) -> rule4) triple2) -> rule1))]
("Bob" "is" "furry" "-")
((((triple2) -> (rule4 % int2)) triple2) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is kind.
True
6
proof
[(((triple2 ((((triple2) -> rule4) triple2) -> rule1)) -> rule6))]
("Bob" "is" "kind" "+")
((triple2 ((((triple2) -> (rule4 % int3)) triple2) -> (rule1 % int2))) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is not kind.
False
6
inv-proof
[(((triple2 ((((triple2) -> rule4) triple2) -> rule1)) -> rule6))]
("Bob" "is" "kind" "-")
((triple2 ((((triple2) -> (rule4 % int3)) triple2) -> (rule1 % int2))) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Anne is not round.
Unknown
inv-rconc
[@2: Anne is round.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Anne" "is" "round" "-")
Anne is rough.
Unknown
rconc
[@3: Anne is rough.[CWA. Example of deepest failure = (rule5 <- rule3 <- rule2 <- FAIL)]]
("Anne" "is" "rough" "+")
Anne is not kind.
Unknown
inv-rconc
[@3: Anne is kind.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule2 <- FAIL)]]
("Anne" "is" "kind" "-")
Fiona is rough.
Unknown
rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "rough" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Anne is furry.[(triple1)] Bob is round.[(triple2)] Fiona is smart.[(triple3)] @1: Bob is smart.[(((triple2) -> rule4))] @2: Bob is furry.[(((((triple2) -> rule4) triple2) -> rule1))] @3: Bob is kind.[(((triple2 ((((triple2) -> rule4) triple2) -> rule1)) -> rule6))] @4: Bob is rough.[(((triple2 ((triple2 ((((triple2) -> rule4) triple2) -> rule1)) -> rule6)) -> rule5))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
((triple2) -> (rule4 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((triple2 ((((triple2) -> (rule4 % int3)) triple2) -> (rule1 % int2))) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
((triple2 ((triple2 ((((triple2) -> (rule4 % int4)) triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4