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