Bob is kind. Charlie is furry. Fiona is furry. Harry is round. If something is round then it is kind. All kind things are smart. All young, kind things are smart. Young things are not smart. If something is green then it is nice. Kind things are nice. All nice things are round. Smart things are not furry.
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Harry is round.
("Harry" "is" "round" "+")
If something is round then it is kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
All kind things are smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
All young, kind things are smart.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "smart" "+"))
Young things are not smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "-"))
If something is green then it is nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
Kind things are nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
All nice things are round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
Smart things are not furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "-"))
Harry is round.
True
1
proof
[(triple4)]
("Harry" "is" "round" "+")
triple4
Charlie is not furry.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "furry" "-")
triple2
Bob is nice.
True
2
proof
[(((triple1) -> rule6))]
("Bob" "is" "nice" "+")
((triple1) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not smart.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "smart" "-")
((triple1) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not furry.
True
3
proof
[(((((triple1) -> rule2)) -> rule8))]
("Bob" "is" "furry" "-")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is furry.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule8))]
("Bob" "is" "furry" "+")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Harry is not furry.
True
4
proof
[(((((((triple4) -> rule1)) -> rule2)) -> rule8))]
("Harry" "is" "furry" "-")
((((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is furry.
False
4
inv-proof
[(((((((triple4) -> rule1)) -> rule2)) -> rule8))]
("Harry" "is" "furry" "+")
((((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Fiona is not smart.
Unknown
inv-rconc
[@4: Fiona is smart.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule7 <- rule5 <- FAIL)]]
("Fiona" "is" "smart" "-")
Charlie is smart.
Unknown
rconc
[@4: Charlie is smart.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule7 <- rule5 <- FAIL)]]
("Charlie" "is" "smart" "+")
Charlie is not nice.
Unknown
inv-rconc
[@4: Charlie is nice.[CWA. Example of deepest failure = (rule6 <- rule1 <- rule7 <- rule5 <- FAIL)]]
("Charlie" "is" "nice" "-")
Fiona is kind.
Unknown
rconc
[@3: Fiona is kind.[CWA. Example of deepest failure = (rule1 <- rule7 <- rule5 <- FAIL)]]
("Fiona" "is" "kind" "+")
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is kind.[(triple1)] Charlie is furry.[(triple2)] Fiona is furry.[(triple3)] Harry is round.[(triple4)] @1: Bob is nice.[(((triple1) -> rule6))] Bob is smart.[(((triple1) -> rule2))] Harry is kind.[(((triple4) -> rule1))] @2: Bob is not furry.[(((((triple1) -> rule2)) -> rule8))] Bob is round.[(((((triple1) -> rule6)) -> rule7))] Harry is nice.[(((((triple4) -> rule1)) -> rule6))] Harry is smart.[(((((triple4) -> rule1)) -> rule2))] @3: Harry is not furry.[(((((((triple4) -> rule1)) -> rule2)) -> rule8))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
Harry is round.
("Harry" "is" "round" "+")
triple4
Bob is nice.
("Bob" "is" "nice" "+")
((triple1) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple4) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Bob is not furry.
("Bob" "is" "furry" "-")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((((triple1) -> (rule6 % int2))) -> (rule7 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((triple4) -> (rule1 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not furry.
("Harry" "is" "furry" "-")
((((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3