Charlie is furry. Charlie is white. Fiona is big. Fiona is furry. Fiona is kind. Fiona is quiet. Fiona is red. Harry is not big. Harry is not furry. Harry is not red. Harry is smart. Harry is not white. If someone is big then they are white. If someone is furry then they are big. All big, furry people are kind.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is not big.
("Harry" "is" "big" "-")
Harry is not furry.
("Harry" "is" "furry" "-")
Harry is not red.
("Harry" "is" "red" "-")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is not white.
("Harry" "is" "white" "-")
If someone is big then they are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
If someone is furry then they are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
All big, furry people are kind.
((("someone" "is" "big" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
Fiona is red.
True
1
proof
[(triple7)]
("Fiona" "is" "red" "+")
triple7
Fiona is not kind.
False
1
inv-proof
[(triple5 OR ((triple3 triple4) -> rule3) OR ((((triple4) -> rule2) triple4) -> rule3))]
("Fiona" "is" "kind" "-")
triple5
((triple3 triple4) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((((triple4) -> (rule2 % int2)) triple4) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is white.
True
2
proof
[(((triple3) -> rule1) OR ((((triple4) -> rule2)) -> rule1))]
("Fiona" "is" "white" "+")
((triple3) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Charlie is not big.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "big" "-")
((triple1) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is kind.
True
4
proof
[(((((triple1) -> rule2) triple1) -> rule3))]
("Charlie" "is" "kind" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not kind.
False
4
inv-proof
[(((((triple1) -> rule2) triple1) -> rule3))]
("Charlie" "is" "kind" "-")
((((triple1) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "kind" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Charlie is furry.[(triple1)] Charlie is white.[(triple2 OR ((((triple1) -> rule2)) -> rule1))] Fiona is big.[(triple3 OR ((triple4) -> rule2))] Fiona is furry.[(triple4)] Fiona is kind.[(triple5 OR ((triple3 triple4) -> rule3) OR ((((triple4) -> rule2) triple4) -> rule3))] Fiona is quiet.[(triple6)] Fiona is red.[(triple7)] Harry is not big.[(triple8)] Harry is not furry.[(triple9)] Harry is not red.[(triple10)] Harry is not white.[(triple12)] Harry is smart.[(triple11)] @1: Charlie is big.[(((triple1) -> rule2))] Fiona is white.[(((triple3) -> rule1) OR ((((triple4) -> rule2)) -> rule1))] @2: Charlie is kind.[(((((triple1) -> rule2) triple1) -> rule3))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is white.
("Charlie" "is" "white" "+")
triple2
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
triple3
((triple4) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple4
Fiona is kind.
("Fiona" "is" "kind" "+")
triple5
((triple3 triple4) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((((triple4) -> (rule2 % int2)) triple4) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple6
Fiona is red.
("Fiona" "is" "red" "+")
triple7
Harry is not big.
("Harry" "is" "big" "-")
triple8
Harry is not furry.
("Harry" "is" "furry" "-")
triple9
Harry is not red.
("Harry" "is" "red" "-")
triple10
Harry is not white.
("Harry" "is" "white" "-")
triple12
Harry is smart.
("Harry" "is" "smart" "+")
triple11
Charlie is big.
("Charlie" "is" "big" "+")
((triple1) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple3) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2