Bob is smart. Dave is not smart. Erin is quiet. Harry is cold. Cold people are big. All young, kind people are big. If someone is big then they are kind. All kind people are furry. Furry people are quiet. If Erin is big and Erin is not quiet then Erin is smart.
Bob is smart.
("Bob" "is" "smart" "+")
Dave is not smart.
("Dave" "is" "smart" "-")
Erin is quiet.
("Erin" "is" "quiet" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Cold people are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
All young, kind people are big.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If someone is big then they are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
All kind people are furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
Furry people are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If Erin is big and Erin is not quiet then Erin is smart.
((("Erin" "is" "big" "+") ("Erin" "is" "quiet" "~")) -> ("Erin" "is" "smart" "+"))
Harry is cold.
True
1
proof
[(triple4)]
("Harry" "is" "cold" "+")
triple4
Dave is smart.
False
1
inv-proof
[(triple2)]
("Dave" "is" "smart" "+")
triple2
Harry is big.
True
2
proof
[(((triple4) -> rule1))]
("Harry" "is" "big" "+")
((triple4) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple4) -> rule1))]
("Harry" "is" "big" "-")
((triple4) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
True
3
proof
[(((((triple4) -> rule1)) -> rule3))]
("Harry" "is" "kind" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not kind.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule3))]
("Harry" "is" "kind" "-")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is furry.
True
4
proof
[(((((((triple4) -> rule1)) -> rule3)) -> rule4))]
("Harry" "is" "furry" "+")
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is not furry.
False
4
inv-proof
[(((((((triple4) -> rule1)) -> rule3)) -> rule4))]
("Harry" "is" "furry" "-")
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Bob is not quiet.
Unknown
inv-rconc
[@4: Bob is quiet.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule3 <- rule1 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is big.
Unknown
rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "big" "+")
Dave is not kind.
Unknown
inv-rconc
[@2: Dave is kind.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Dave" "is" "kind" "-")
Bob is furry.
Unknown
rconc
[@3: Bob is furry.[CWA. Example of deepest failure = (rule4 <- rule3 <- rule1 <- FAIL)]]
("Bob" "is" "furry" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Bob is smart.[(triple1)] Dave is not smart.[(triple2)] Erin is quiet.[(triple3)] Harry is cold.[(triple4)] @1: Harry is big.[(((triple4) -> rule1))] @2: Harry is kind.[(((((triple4) -> rule1)) -> rule3))] @3: Harry is furry.[(((((((triple4) -> rule1)) -> rule3)) -> rule4))] @4: Harry is quiet.[(((((((((triple4) -> rule1)) -> rule3)) -> rule4)) -> rule5))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Dave is not smart.
("Dave" "is" "smart" "-")
triple2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple3
Harry is cold.
("Harry" "is" "cold" "+")
triple4
Harry is big.
("Harry" "is" "big" "+")
((triple4) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
((((((((triple4) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4