Bob is kind. Bob is nice. Bob is quiet. Erin is furry. Erin is nice. Harry is blue. Harry is furry. Harry is green. Harry is kind. Harry is quiet. If something is blue and nice then it is not green. If something is nice then it is blue. If something is furry and not green then it is not big. If something is kind and not nice then it is not quiet. All green things are quiet. If something is green and big then it is not kind.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If something is blue and nice then it is not green.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "-"))
If something is nice then it is blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
If something is furry and not green then it is not big.
((("something" "is" "furry" "+") ("something" "is" "green" "~")) -> ("something" "is" "big" "-"))
If something is kind and not nice then it is not quiet.
((("something" "is" "kind" "+") ("something" "is" "nice" "~")) -> ("something" "is" "quiet" "-"))
All green things are quiet.
((("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
If something is green and big then it is not kind.
((("something" "is" "green" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "-"))
Bob is kind.
True
1
proof
[(triple1)]
("Bob" "is" "kind" "+")
triple1
Bob is not quiet.
False
1
inv-proof
[(triple3)]
("Bob" "is" "quiet" "-")
triple3
Bob is blue.
True
2
proof
[(((triple2) -> rule2))]
("Bob" "is" "blue" "+")
((triple2) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Erin is not blue.
False
2
inv-proof
[(((triple5) -> rule2))]
("Erin" "is" "blue" "-")
((triple5) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Bob is not green.
True
4
proof
[(((((triple2) -> rule2) triple2) -> rule1))]
("Bob" "is" "green" "-")
((((triple2) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Erin is green.
False
4
inv-proof
[(((((triple5) -> rule2) triple5) -> rule1))]
("Erin" "is" "green" "+")
((((triple5) -> (rule2 % int2)) triple5) -> (rule1 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not big.
True
6
proof
[(((triple4 ((((triple5) -> rule2) triple5) -> rule1)) -> rule3))]
("Erin" "is" "big" "-")
((triple4 ((((triple5) -> (rule2 % int3)) triple5) -> (rule1 % int2))) -> (rule3 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is not green.
("Erin" "is" "green" "-")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is big.
False
6
inv-proof
[(((triple4 ((((triple5) -> rule2) triple5) -> rule1)) -> rule3))]
("Erin" "is" "big" "+")
((triple4 ((((triple5) -> (rule2 % int3)) triple5) -> (rule1 % int2))) -> (rule3 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is not green.
("Erin" "is" "green" "-")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "quiet" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Bob is kind.[(triple1)] Bob is nice.[(triple2)] Bob is quiet.[(triple3)] Erin is furry.[(triple4)] Erin is nice.[(triple5)] Harry is blue.[(triple6)] Harry is furry.[(triple7)] Harry is green.[(triple8)] Harry is kind.[(triple9)] Harry is quiet.[(triple10 OR ((triple8) -> rule5))] @1: Bob is blue.[(((triple2) -> rule2))] Erin is blue.[(((triple5) -> rule2))] @2: Bob is not green.[(((((triple2) -> rule2) triple2) -> rule1))] Erin is not green.[(((((triple5) -> rule2) triple5) -> rule1))] @3: Erin is not big.[(((triple4 ((((triple5) -> rule2) triple5) -> rule1)) -> rule3))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Erin is furry.
("Erin" "is" "furry" "+")
triple4
Erin is nice.
("Erin" "is" "nice" "+")
triple5
Harry is blue.
("Harry" "is" "blue" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Harry is green.
("Harry" "is" "green" "+")
triple8
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
((triple8) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple2) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple5) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Bob is not green.
("Bob" "is" "green" "-")
((((triple2) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Erin is not green.
("Erin" "is" "green" "-")
((((triple5) -> (rule2 % int2)) triple5) -> (rule1 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not big.
("Erin" "is" "big" "-")
((triple4 ((((triple5) -> (rule2 % int3)) triple5) -> (rule1 % int2))) -> (rule3 % int1))
Erin is not big.
("Erin" "is" "big" "-")
int1
Erin is not green.
("Erin" "is" "green" "-")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3