Bob is furry. Bob is nice. Erin is big. Erin is furry. Erin is green. Erin is red. Harry is big. Harry is furry. Harry is not nice. Harry is not quiet. If Bob is quiet then Bob is big. Kind, red people are nice. If someone is quiet and not green then they are kind. All red people are kind. All nice people are quiet. All furry, green people are big.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is red.
("Erin" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is not nice.
("Harry" "is" "nice" "-")
Harry is not quiet.
("Harry" "is" "quiet" "-")
If Bob is quiet then Bob is big.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "big" "+"))
Kind, red people are nice.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If someone is quiet and not green then they are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "kind" "+"))
All red people are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
All nice people are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
All furry, green people are big.
((("someone" "is" "furry" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
Harry is not quiet.
True
1
proof
[(triple10)]
("Harry" "is" "quiet" "-")
triple10
Erin is not big.
False
1
inv-proof
[(triple3 OR ((triple4 triple5) -> rule6))]
("Erin" "is" "big" "-")
triple3
((triple4 triple5) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is kind.
True
2
proof
[(((triple6) -> rule4))]
("Erin" "is" "kind" "+")
((triple6) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not kind.
False
2
inv-proof
[(((triple6) -> rule4))]
("Erin" "is" "kind" "-")
((triple6) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
True
4
proof
[(((((triple6) -> rule4) triple6) -> rule2))]
("Erin" "is" "nice" "+")
((((triple6) -> (rule4 % int2)) triple6) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not nice.
False
4
inv-proof
[(((((triple6) -> rule4) triple6) -> rule2))]
("Erin" "is" "nice" "-")
((((triple6) -> (rule4 % int2)) triple6) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is quiet.
True
5
proof
[(((((((triple6) -> rule4) triple6) -> rule2)) -> rule5))]
("Erin" "is" "quiet" "+")
((((((triple6) -> (rule4 % int3)) triple6) -> (rule2 % int2))) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is not quiet.
False
5
inv-proof
[(((((((triple6) -> rule4) triple6) -> rule2)) -> rule5))]
("Erin" "is" "quiet" "-")
((((((triple6) -> (rule4 % int3)) triple6) -> (rule2 % int2))) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Bob is not kind.
Unknown
inv-rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "kind" "-")
Harry is kind.
Unknown
rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "kind" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is furry.[(triple1)] Bob is nice.[(triple2)] Erin is big.[(triple3 OR ((triple4 triple5) -> rule6))] Erin is furry.[(triple4)] Erin is green.[(triple5)] Erin is red.[(triple6)] Harry is big.[(triple7)] Harry is furry.[(triple8)] Harry is not nice.[(triple9)] Harry is not quiet.[(triple10)] @1: Bob is quiet.[(((triple2) -> rule5))] Erin is kind.[(((triple6) -> rule4))] @2: Bob is big.[(((((triple2) -> rule5)) -> rule1))] Erin is nice.[(((((triple6) -> rule4) triple6) -> rule2))] @3: Erin is quiet.[(((((((triple6) -> rule4) triple6) -> rule2)) -> rule5))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Erin is big.
("Erin" "is" "big" "+")
triple3
((triple4 triple5) -> (rule6 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
triple4
Erin is green.
("Erin" "is" "green" "+")
triple5
Erin is red.
("Erin" "is" "red" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Harry is furry.
("Harry" "is" "furry" "+")
triple8
Harry is not nice.
("Harry" "is" "nice" "-")
triple9
Harry is not quiet.
("Harry" "is" "quiet" "-")
triple10
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple6) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((triple6) -> (rule4 % int2)) triple6) -> (rule2 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((((((triple6) -> (rule4 % int3)) triple6) -> (rule2 % int2))) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3