Bob is quiet. Charlie is blue. Fiona is blue. Harry is kind. If something is kind then it is furry. All round, green things are not big. Kind, furry things are round. If Bob is kind then Bob is big. If Harry is quiet then Harry is green. If Fiona is not kind and Fiona is not round then Fiona is big. If something is big then it is blue. If something is round then it is blue.
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If something is kind then it is furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
All round, green things are not big.
((("something" "is" "round" "+") ("something" "is" "green" "+")) -> ("something" "is" "big" "-"))
Kind, furry things are round.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
If Bob is kind then Bob is big.
((("Bob" "is" "kind" "+")) -> ("Bob" "is" "big" "+"))
If Harry is quiet then Harry is green.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "green" "+"))
If Fiona is not kind and Fiona is not round then Fiona is big.
((("Fiona" "is" "kind" "~") ("Fiona" "is" "round" "~")) -> ("Fiona" "is" "big" "+"))
If something is big then it is blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If something is round then it is blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Bob is quiet.
True
1
proof
[(triple1)]
("Bob" "is" "quiet" "+")
triple1
Fiona is not blue.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "blue" "-")
triple3
Harry is furry.
True
2
proof
[(((triple4) -> rule1))]
("Harry" "is" "furry" "+")
((triple4) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple4) -> rule1))]
("Harry" "is" "furry" "-")
((triple4) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is round.
True
4
proof
[(((triple4 ((triple4) -> rule1)) -> rule3))]
("Harry" "is" "round" "+")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not round.
False
4
inv-proof
[(((triple4 ((triple4) -> rule1)) -> rule3))]
("Harry" "is" "round" "-")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
True
5
proof
[(((((triple4 ((triple4) -> rule1)) -> rule3)) -> rule8))]
("Harry" "is" "blue" "+")
((((triple4 ((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is not blue.
False
5
inv-proof
[(((((triple4 ((triple4) -> rule1)) -> rule3)) -> rule8))]
("Harry" "is" "blue" "-")
((((triple4 ((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Bob is not furry.
Unknown
inv-rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "furry" "-")
Fiona is furry.
Unknown
rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "furry" "+")
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "big" "-")
Bob is round.
Unknown
rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "round" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Bob is quiet.[(triple1)] Charlie is blue.[(triple2)] Fiona is blue.[(triple3)] Harry is kind.[(triple4)] @1: Harry is furry.[(((triple4) -> rule1))] @2: Harry is round.[(((triple4 ((triple4) -> rule1)) -> rule3))] @3: Harry is blue.[(((((triple4 ((triple4) -> rule1)) -> rule3)) -> rule8))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Fiona is blue.
("Fiona" "is" "blue" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Harry is furry.
("Harry" "is" "furry" "+")
((triple4) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple4 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((((triple4 ((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3