Anne is furry. Anne is red. Anne is smart. Charlie is big. Charlie is not furry. Charlie is green. Charlie is not nice. Charlie is not quiet. Charlie is red. Charlie is smart. Fiona is quiet. Fiona is red. Gary is big. Gary is furry. Gary is not green. Gary is smart. If Fiona is furry then Fiona is not nice. Nice things are furry. If something is smart then it is not nice. If Fiona is smart then Fiona is not big. If Fiona is furry and Fiona is green then Fiona is not red. Green, nice things are not quiet. Big, furry things are quiet. If something is smart and not nice then it is big.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is not nice.
("Charlie" "is" "nice" "-")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is not green.
("Gary" "is" "green" "-")
Gary is smart.
("Gary" "is" "smart" "+")
If Fiona is furry then Fiona is not nice.
((("Fiona" "is" "furry" "+")) -> ("Fiona" "is" "nice" "-"))
Nice things are furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
If something is smart then it is not nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "-"))
If Fiona is smart then Fiona is not big.
((("Fiona" "is" "smart" "+")) -> ("Fiona" "is" "big" "-"))
If Fiona is furry and Fiona is green then Fiona is not red.
((("Fiona" "is" "furry" "+") ("Fiona" "is" "green" "+")) -> ("Fiona" "is" "red" "-"))
Green, nice things are not quiet.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "quiet" "-"))
Big, furry things are quiet.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
If something is smart and not nice then it is big.
((("something" "is" "smart" "+") ("something" "is" "nice" "~")) -> ("something" "is" "big" "+"))
Anne is smart.
True
1
proof
[(triple3)]
("Anne" "is" "smart" "+")
triple3
Anne is not furry.
False
1
inv-proof
[(triple1)]
("Anne" "is" "furry" "-")
triple1
Gary is not nice.
True
2
proof
[(((triple16) -> rule3))]
("Gary" "is" "nice" "-")
((triple16) -> (rule3 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is nice.
False
2
inv-proof
[(((triple16) -> rule3))]
("Gary" "is" "nice" "+")
((triple16) -> (rule3 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Anne is big.
True
4
proof
[(((triple3 ((triple3) -> rule3)) -> rule8))]
("Anne" "is" "big" "+")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not nice.
("Anne" "is" "nice" "-")
int2
Anne is not big.
False
4
inv-proof
[(((triple3 ((triple3) -> rule3)) -> rule8))]
("Anne" "is" "big" "-")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not nice.
("Anne" "is" "nice" "-")
int2
Anne is quiet.
True
6
proof
[(((((triple3 ((triple3) -> rule3)) -> rule8) triple1) -> rule7))]
("Anne" "is" "quiet" "+")
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule8 % int2)) triple1) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not nice.
("Anne" "is" "nice" "-")
int3
Anne is not quiet.
False
6
inv-proof
[(((((triple3 ((triple3) -> rule3)) -> rule8) triple1) -> rule7))]
("Anne" "is" "quiet" "-")
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule8 % int2)) triple1) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not nice.
("Anne" "is" "nice" "-")
int3
Fiona is not furry.
Unknown
inv-rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "furry" "-")
Fiona is big.
Unknown
rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "big" "+")
Fiona is not nice.
Unknown
inv-random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Anne is furry.[(triple1)] Anne is red.[(triple2)] Anne is smart.[(triple3)] Charlie is big.[(triple4 OR ((triple10 triple7) -> rule8) OR ((triple10 ((triple10) -> rule3)) -> rule8))] Charlie is green.[(triple6)] Charlie is not furry.[(triple5)] Charlie is not nice.[(triple7 OR ((triple10) -> rule3))] Charlie is not quiet.[(triple8)] Charlie is red.[(triple9)] Charlie is smart.[(triple10)] Fiona is quiet.[(triple11)] Fiona is red.[(triple12)] Gary is big.[(triple13 OR ((triple16 ((triple16) -> rule3)) -> rule8))] Gary is furry.[(triple14)] Gary is not green.[(triple15)] Gary is smart.[(triple16)] @1: Anne is not nice.[(((triple3) -> rule3))] Gary is not nice.[(((triple16) -> rule3))] Gary is quiet.[(((triple13 triple14) -> rule7) OR ((((triple16 ((triple16) -> rule3)) -> rule8) triple14) -> rule7))] @2: Anne is big.[(((triple3 ((triple3) -> rule3)) -> rule8))] @3: Anne is quiet.[(((((triple3 ((triple3) -> rule3)) -> rule8) triple1) -> rule7))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
triple4
((triple10 triple7) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((triple10 ((triple10) -> (rule3 % int2))) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not nice.
("Charlie" "is" "nice" "-")
int2
Charlie is green.
("Charlie" "is" "green" "+")
triple6
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple5
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple7
((triple10) -> (rule3 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple8
Charlie is red.
("Charlie" "is" "red" "+")
triple9
Charlie is smart.
("Charlie" "is" "smart" "+")
triple10
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple11
Fiona is red.
("Fiona" "is" "red" "+")
triple12
Gary is big.
("Gary" "is" "big" "+")
triple13
((triple16 ((triple16) -> (rule3 % int2))) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
int2
Gary is furry.
("Gary" "is" "furry" "+")
triple14
Gary is not green.
("Gary" "is" "green" "-")
triple15
Gary is smart.
("Gary" "is" "smart" "+")
triple16
Anne is not nice.
("Anne" "is" "nice" "-")
((triple3) -> (rule3 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
((triple16) -> (rule3 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple13 triple14) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple16 ((triple16) -> (rule3 % int3))) -> (rule8 % int2)) triple14) -> (rule7 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not nice.
("Gary" "is" "nice" "-")
int3
Anne is big.
("Anne" "is" "big" "+")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule8 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not nice.
("Anne" "is" "nice" "-")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule8 % int2)) triple1) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not nice.
("Anne" "is" "nice" "-")
int3