Bob is nice. Bob is red. Bob is round. Dave is furry. Dave is not round. Fiona is blue. Fiona is furry. Fiona is round. Harry is big. Harry is round. All blue, big things are furry. If something is red then it is furry. If Harry is not big then Harry is quiet. Big things are round. All big things are blue. If Dave is round and Dave is furry then Dave is not red. If something is big and furry then it is quiet. If something is big then it is not nice.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is not round.
("Dave" "is" "round" "-")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is round.
("Harry" "is" "round" "+")
All blue, big things are furry.
((("something" "is" "blue" "+") ("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
If something is red then it is furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
If Harry is not big then Harry is quiet.
((("Harry" "is" "big" "~")) -> ("Harry" "is" "quiet" "+"))
Big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
All big things are blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If Dave is round and Dave is furry then Dave is not red.
((("Dave" "is" "round" "+") ("Dave" "is" "furry" "+")) -> ("Dave" "is" "red" "-"))
If something is big and furry then it is quiet.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
If something is big then it is not nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "-"))
Dave is furry.
True
1
proof
[(triple4)]
("Dave" "is" "furry" "+")
triple4
Bob is not red.
False
1
inv-proof
[(triple2)]
("Bob" "is" "red" "-")
triple2
Harry is blue.
True
2
proof
[(((triple9) -> rule5))]
("Harry" "is" "blue" "+")
((triple9) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is nice.
False
2
inv-proof
[(((triple9) -> rule8))]
("Harry" "is" "nice" "+")
((triple9) -> (rule8 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is furry.
True
4
proof
[(((((triple9) -> rule5) triple9) -> rule1))]
("Harry" "is" "furry" "+")
((((triple9) -> (rule5 % int2)) triple9) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not furry.
False
4
inv-proof
[(((((triple9) -> rule5) triple9) -> rule1))]
("Harry" "is" "furry" "-")
((((triple9) -> (rule5 % int2)) triple9) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
True
6
proof
[(((triple9 ((((triple9) -> rule5) triple9) -> rule1)) -> rule7))]
("Harry" "is" "quiet" "+")
((triple9 ((((triple9) -> (rule5 % int3)) triple9) -> (rule1 % int2))) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is not quiet.
False
6
inv-proof
[(((triple9 ((((triple9) -> rule5) triple9) -> rule1)) -> rule7))]
("Harry" "is" "quiet" "-")
((triple9 ((((triple9) -> (rule5 % int3)) triple9) -> (rule1 % int2))) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "quiet" "-")
Fiona is quiet.
Unknown
rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "quiet" "+")
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "blue" "-")
Dave is quiet.
Unknown
rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "quiet" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Bob is nice.[(triple1)] Bob is red.[(triple2)] Bob is round.[(triple3)] Dave is furry.[(triple4)] Dave is not round.[(triple5)] Fiona is blue.[(triple6)] Fiona is furry.[(triple7)] Fiona is round.[(triple8)] Harry is big.[(triple9)] Harry is round.[(triple10 OR ((triple9) -> rule4))] @1: Bob is furry.[(((triple2) -> rule2))] Harry is blue.[(((triple9) -> rule5))] Harry is not nice.[(((triple9) -> rule8))] @2: Harry is furry.[(((((triple9) -> rule5) triple9) -> rule1))] @3: Harry is quiet.[(((triple9 ((((triple9) -> rule5) triple9) -> rule1)) -> rule7))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Dave is not round.
("Dave" "is" "round" "-")
triple5
Fiona is blue.
("Fiona" "is" "blue" "+")
triple6
Fiona is furry.
("Fiona" "is" "furry" "+")
triple7
Fiona is round.
("Fiona" "is" "round" "+")
triple8
Harry is big.
("Harry" "is" "big" "+")
triple9
Harry is round.
("Harry" "is" "round" "+")
triple10
((triple9) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple9) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not nice.
("Harry" "is" "nice" "-")
((triple9) -> (rule8 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((((triple9) -> (rule5 % int2)) triple9) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple9 ((((triple9) -> (rule5 % int3)) triple9) -> (rule1 % int2))) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3