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