Fiona is furry. Fiona is quiet. Fiona is smart. Harry is furry. Harry is kind. Harry is nice. Harry is round. All quiet, round people are furry. If Fiona is round then Fiona is quiet. If Harry is nice then Harry is quiet. All kind people are smart. Smart people are nice. Nice, quiet people are kind. If someone is round and furry then they are nice. If someone is smart and green then they are round.
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is round.
("Harry" "is" "round" "+")
All quiet, round people are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
If Fiona is round then Fiona is quiet.
((("Fiona" "is" "round" "+")) -> ("Fiona" "is" "quiet" "+"))
If Harry is nice then Harry is quiet.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "quiet" "+"))
All kind people are smart.
((("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
Smart people are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
Nice, quiet people are kind.
((("someone" "is" "nice" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
If someone is round and furry then they are nice.
((("someone" "is" "round" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
If someone is smart and green then they are round.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
Harry is kind.
True
1
proof
[(triple5 OR ((triple6 ((triple6) -> rule3)) -> rule6) OR ((((triple7 triple4) -> rule7) ((triple6) -> rule3)) -> rule6) OR ((triple6 ((((triple7 triple4) -> rule7)) -> rule3)) -> rule6) OR ((((triple7 triple4) -> rule7) ((((triple7 triple4) -> rule7)) -> rule3)) -> rule6))]
("Harry" "is" "kind" "+")
triple5
((triple6 ((triple6) -> (rule3 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple7 triple4) -> (rule7 % int3)) ((triple6) -> (rule3 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((triple6 ((((triple7 triple4) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((triple7 triple4) -> (rule7 % int3)) ((((triple7 triple4) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Fiona is not quiet.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "quiet" "-")
triple2
Harry is quiet.
True
2
proof
[(((triple6) -> rule3) OR ((((triple7 triple4) -> rule7)) -> rule3) OR ((((((triple5) -> rule4)) -> rule5)) -> rule3))]
("Harry" "is" "quiet" "+")
((triple6) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple7 triple4) -> (rule7 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((((triple5) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is not smart.
False
2
inv-proof
[(((triple5) -> rule4) OR ((((triple6 ((triple6) -> rule3)) -> rule6)) -> rule4) OR ((((((triple7 triple4) -> rule7) ((triple6) -> rule3)) -> rule6)) -> rule4) OR ((((triple6 ((((triple7 triple4) -> rule7)) -> rule3)) -> rule6)) -> rule4) OR ((((((triple7 triple4) -> rule7) ((((triple7 triple4) -> rule7)) -> rule3)) -> rule6)) -> rule4))]
("Harry" "is" "smart" "-")
((triple5) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple6 ((triple6) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((triple7 triple4) -> (rule7 % int4)) ((triple6) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
((((triple6 ((((triple7 triple4) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
((((((triple7 triple4) -> (rule7 % int4)) ((((triple7 triple4) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Fiona is kind.
True
4
proof
[(((((triple3) -> rule5) triple2) -> rule6))]
("Fiona" "is" "kind" "+")
((((triple3) -> (rule5 % int2)) triple2) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is not kind.
False
4
inv-proof
[(((((triple3) -> rule5) triple2) -> rule6))]
("Fiona" "is" "kind" "-")
((((triple3) -> (rule5 % int2)) triple2) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "round" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Fiona is furry.[(triple1)] Fiona is quiet.[(triple2)] Fiona is smart.[(triple3)] Harry is furry.[(triple4 OR ((((triple6) -> rule3) triple7) -> rule1) OR ((((((((triple5) -> rule4)) -> rule5)) -> rule3) triple7) -> rule1))] Harry is kind.[(triple5 OR ((triple6 ((triple6) -> rule3)) -> rule6) OR ((((triple7 triple4) -> rule7) ((triple6) -> rule3)) -> rule6) OR ((triple6 ((((triple7 triple4) -> rule7)) -> rule3)) -> rule6) OR ((((triple7 triple4) -> rule7) ((((triple7 triple4) -> rule7)) -> rule3)) -> rule6))] Harry is nice.[(triple6 OR ((triple7 triple4) -> rule7) OR ((((triple5) -> rule4)) -> rule5))] Harry is round.[(triple7)] @1: Fiona is nice.[(((triple3) -> rule5))] Harry is quiet.[(((triple6) -> rule3) OR ((((triple7 triple4) -> rule7)) -> rule3) OR ((((((triple5) -> rule4)) -> rule5)) -> rule3))] Harry is smart.[(((triple5) -> rule4) OR ((((triple6 ((triple6) -> rule3)) -> rule6)) -> rule4) OR ((((((triple7 triple4) -> rule7) ((triple6) -> rule3)) -> rule6)) -> rule4) OR ((((triple6 ((((triple7 triple4) -> rule7)) -> rule3)) -> rule6)) -> rule4) OR ((((((triple7 triple4) -> rule7) ((((triple7 triple4) -> rule7)) -> rule3)) -> rule6)) -> rule4))] @2: Fiona is kind.[(((((triple3) -> rule5) triple2) -> rule6))]
Fiona is furry.
("Fiona" "is" "furry" "+")
triple1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
((((triple6) -> (rule3 % int2)) triple7) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((((((triple5) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) triple7) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Harry is kind.
("Harry" "is" "kind" "+")
triple5
((triple6 ((triple6) -> (rule3 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple7 triple4) -> (rule7 % int3)) ((triple6) -> (rule3 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((triple6 ((((triple7 triple4) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((triple7 triple4) -> (rule7 % int3)) ((((triple7 triple4) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
triple6
((triple7 triple4) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple5) -> (rule4 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
triple7
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple3) -> (rule5 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple6) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple7 triple4) -> (rule7 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((((triple5) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
((triple5) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple6 ((triple6) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((triple7 triple4) -> (rule7 % int4)) ((triple6) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
((((triple6 ((((triple7 triple4) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
((((((triple7 triple4) -> (rule7 % int4)) ((((triple7 triple4) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
((((triple3) -> (rule5 % int2)) triple2) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2