Bob is big. Bob is furry. Bob is white. Erin is furry. Erin is rough. Harry is furry. Harry is quiet. If something is young then it is big. If something is kind and quiet then it is white. White things are rough. If something is furry then it is kind. Young, rough things are kind. All big, quiet things are furry.
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is white.
("Bob" "is" "white" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If something is young then it is big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
If something is kind and quiet then it is white.
((("something" "is" "kind" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
White things are rough.
((("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
If something is furry then it is kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
Young, rough things are kind.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
All big, quiet things are furry.
((("something" "is" "big" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
Harry is furry.
True
1
proof
[(triple6)]
("Harry" "is" "furry" "+")
triple6
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Harry is kind.
True
2
proof
[(((triple6) -> rule4))]
("Harry" "is" "kind" "+")
((triple6) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Bob is not rough.
False
2
inv-proof
[(((triple3) -> rule3))]
("Bob" "is" "rough" "-")
((triple3) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Harry is white.
True
4
proof
[(((((triple6) -> rule4) triple7) -> rule2))]
("Harry" "is" "white" "+")
((((triple6) -> (rule4 % int2)) triple7) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not white.
False
4
inv-proof
[(((((triple6) -> rule4) triple7) -> rule2))]
("Harry" "is" "white" "-")
((((triple6) -> (rule4 % int2)) triple7) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
True
5
proof
[(((((((triple6) -> rule4) triple7) -> rule2)) -> rule3))]
("Harry" "is" "rough" "+")
((((((triple6) -> (rule4 % int3)) triple7) -> (rule2 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is not rough.
False
5
inv-proof
[(((((((triple6) -> rule4) triple7) -> rule2)) -> rule3))]
("Harry" "is" "rough" "-")
((((((triple6) -> (rule4 % int3)) triple7) -> (rule2 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "white" "-")
Erin is big.
Unknown
rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "big" "+")
Harry is not big.
Unknown
inv-rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "big" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Bob is big.[(triple1)] Bob is furry.[(triple2)] Bob is white.[(triple3)] Erin is furry.[(triple4)] Erin is rough.[(triple5)] Harry is furry.[(triple6)] Harry is quiet.[(triple7)] @1: Bob is kind.[(((triple2) -> rule4))] Bob is rough.[(((triple3) -> rule3))] Erin is kind.[(((triple4) -> rule4))] Harry is kind.[(((triple6) -> rule4))] @2: Harry is white.[(((((triple6) -> rule4) triple7) -> rule2))] @3: Harry is rough.[(((((((triple6) -> rule4) triple7) -> rule2)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Erin is furry.
("Erin" "is" "furry" "+")
triple4
Erin is rough.
("Erin" "is" "rough" "+")
triple5
Harry is furry.
("Harry" "is" "furry" "+")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
Bob is kind.
("Bob" "is" "kind" "+")
((triple2) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((triple3) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple4) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple6) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((((triple6) -> (rule4 % int2)) triple7) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((((((triple6) -> (rule4 % int3)) triple7) -> (rule2 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3