Anne is kind. Anne is not nice. Anne is red. Bob is quiet. Gary is not green. Gary is red. Harry is green. All red, kind people are smart. All furry people are quiet. Quiet people are furry. Green people are nice. Quiet people are red. If someone is smart and furry then they are green. Red people are kind.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is not nice.
("Anne" "is" "nice" "-")
Anne is red.
("Anne" "is" "red" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Gary is not green.
("Gary" "is" "green" "-")
Gary is red.
("Gary" "is" "red" "+")
Harry is green.
("Harry" "is" "green" "+")
All red, kind people are smart.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
All furry people are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
Quiet people are furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
Green people are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Quiet people are red.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
If someone is smart and furry then they are green.
((("someone" "is" "smart" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
Red people are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
Anne is red.
True
1
proof
[(triple3)]
("Anne" "is" "red" "+")
triple3
Bob is not quiet.
False
1
inv-proof
[(triple4)]
("Bob" "is" "quiet" "-")
triple4
Bob is furry.
True
2
proof
[(((triple4) -> rule3))]
("Bob" "is" "furry" "+")
((triple4) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Gary is not kind.
False
2
inv-proof
[(((triple6) -> rule7))]
("Gary" "is" "kind" "-")
((triple6) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is smart.
True
4
proof
[(((triple6 ((triple6) -> rule7)) -> rule1))]
("Gary" "is" "smart" "+")
((triple6 ((triple6) -> (rule7 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Bob is not kind.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule7))]
("Bob" "is" "kind" "-")
((((triple4) -> (rule5 % int2))) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is smart.
True
6
proof
[(((((triple4) -> rule5) ((((triple4) -> rule5)) -> rule7)) -> rule1))]
("Bob" "is" "smart" "+")
((((triple4) -> (rule5 % int3)) ((((triple4) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is not smart.
False
6
inv-proof
[(((((triple4) -> rule5) ((((triple4) -> rule5)) -> rule7)) -> rule1))]
("Bob" "is" "smart" "-")
((((triple4) -> (rule5 % int3)) ((((triple4) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is green.
True
9
proof
[(((((((triple4) -> rule5) ((((triple4) -> rule5)) -> rule7)) -> rule1) ((triple4) -> rule3)) -> rule6))]
("Bob" "is" "green" "+")
((((((triple4) -> (rule5 % int5)) ((((triple4) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule1 % int3)) ((triple4) -> (rule3 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
int5
Bob is not green.
False
9
inv-proof
[(((((((triple4) -> rule5) ((((triple4) -> rule5)) -> rule7)) -> rule1) ((triple4) -> rule3)) -> rule6))]
("Bob" "is" "green" "-")
((((((triple4) -> (rule5 % int5)) ((((triple4) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule1 % int3)) ((triple4) -> (rule3 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
int5
Bob is nice.
True
10
proof
[(((((((((triple4) -> rule5) ((((triple4) -> rule5)) -> rule7)) -> rule1) ((triple4) -> rule3)) -> rule6)) -> rule4))]
("Bob" "is" "nice" "+")
((((((((triple4) -> (rule5 % int6)) ((((triple4) -> (rule5 % int6))) -> (rule7 % int5))) -> (rule1 % int4)) ((triple4) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is kind.
("Bob" "is" "kind" "+")
int5
Bob is red.
("Bob" "is" "red" "+")
int6
Bob is not nice.
False
10
inv-proof
[(((((((((triple4) -> rule5) ((((triple4) -> rule5)) -> rule7)) -> rule1) ((triple4) -> rule3)) -> rule6)) -> rule4))]
("Bob" "is" "nice" "-")
((((((((triple4) -> (rule5 % int6)) ((((triple4) -> (rule5 % int6))) -> (rule7 % int5))) -> (rule1 % int4)) ((triple4) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is kind.
("Bob" "is" "kind" "+")
int5
Bob is red.
("Bob" "is" "red" "+")
int6
Anne is not quiet.
Unknown
inv-rconc
[@2: Anne is quiet.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Anne" "is" "quiet" "-")
Anne is green.
Unknown
rconc
[@3: Anne is green.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule2 <- FAIL)]]
("Anne" "is" "green" "+")
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "nice" "-")
Harry is furry.
Unknown
rconc
[@2: Harry is furry.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Harry" "is" "furry" "+")
Harry is not red.
Unknown
inv-rconc
[@3: Harry is red.[CWA. Example of deepest failure = (rule5 <- rule2 <- rule3 <- FAIL)]]
("Harry" "is" "red" "-")
Anne is furry.
Unknown
rconc
[@2: Anne is furry.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is kind.[(triple1 OR ((triple3) -> rule7))] Anne is not nice.[(triple2)] Anne is red.[(triple3)] Bob is quiet.[(triple4)] Gary is not green.[(triple5)] Gary is red.[(triple6)] Harry is green.[(triple7)] @1: Anne is smart.[(((triple3 triple1) -> rule1) OR ((triple3 ((triple3) -> rule7)) -> rule1))] Bob is furry.[(((triple4) -> rule3))] Bob is red.[(((triple4) -> rule5))] Gary is kind.[(((triple6) -> rule7))] Harry is nice.[(((triple7) -> rule4))] @2: Bob is kind.[(((((triple4) -> rule5)) -> rule7))] Gary is smart.[(((triple6 ((triple6) -> rule7)) -> rule1))] @3: Bob is smart.[(((((triple4) -> rule5) ((((triple4) -> rule5)) -> rule7)) -> rule1))] @4: Bob is green.[(((((((triple4) -> rule5) ((((triple4) -> rule5)) -> rule7)) -> rule1) ((triple4) -> rule3)) -> rule6))] @5: Bob is nice.[(((((((((triple4) -> rule5) ((((triple4) -> rule5)) -> rule7)) -> rule1) ((triple4) -> rule3)) -> rule6)) -> rule4))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
((triple3) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not nice.
("Anne" "is" "nice" "-")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Gary is not green.
("Gary" "is" "green" "-")
triple5
Gary is red.
("Gary" "is" "red" "+")
triple6
Harry is green.
("Harry" "is" "green" "+")
triple7
Anne is smart.
("Anne" "is" "smart" "+")
((triple3 triple1) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple3 ((triple3) -> (rule7 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((triple4) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((triple4) -> (rule5 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple6) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple7) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((((triple4) -> (rule5 % int2))) -> (rule7 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((triple6 ((triple6) -> (rule7 % int2))) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((((triple4) -> (rule5 % int3)) ((((triple4) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
((((((triple4) -> (rule5 % int5)) ((((triple4) -> (rule5 % int5))) -> (rule7 % int4))) -> (rule1 % int3)) ((triple4) -> (rule3 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Bob is red.
("Bob" "is" "red" "+")
int5
Bob is nice.
("Bob" "is" "nice" "+")
((((((((triple4) -> (rule5 % int6)) ((((triple4) -> (rule5 % int6))) -> (rule7 % int5))) -> (rule1 % int4)) ((triple4) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is kind.
("Bob" "is" "kind" "+")
int5
Bob is red.
("Bob" "is" "red" "+")
int6