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