Anne is not nice. Bob is red. Erin is cold. Harry is not smart. If someone is red then they are smart. All cold people are smart. Nice, white people are kind. All cold people are kind. If Harry is white then Harry is cold. Nice people are not white. If someone is smart then they are nice. If Anne is cold and Anne is not kind then Anne is not quiet.
Anne is not nice.
("Anne" "is" "nice" "-")
Bob is red.
("Bob" "is" "red" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
If someone is red then they are smart.
((("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
All cold people are smart.
((("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "+"))
Nice, white people are kind.
((("someone" "is" "nice" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
All cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If Harry is white then Harry is cold.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "cold" "+"))
Nice people are not white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "-"))
If someone is smart then they are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
If Anne is cold and Anne is not kind then Anne is not quiet.
((("Anne" "is" "cold" "+") ("Anne" "is" "kind" "~")) -> ("Anne" "is" "quiet" "-"))
Harry is not smart.
True
1
proof
[(triple4)]
("Harry" "is" "smart" "-")
triple4
Bob is not red.
False
1
inv-proof
[(triple2)]
("Bob" "is" "red" "-")
triple2
Bob is smart.
True
2
proof
[(((triple2) -> rule1))]
("Bob" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not smart.
False
2
inv-proof
[(((triple2) -> rule1))]
("Bob" "is" "smart" "-")
((triple2) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is nice.
True
3
proof
[(((((triple2) -> rule1)) -> rule7))]
("Bob" "is" "nice" "+")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not nice.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule7))]
("Bob" "is" "nice" "-")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not white.
True
4
proof
[(((((((triple2) -> rule1)) -> rule7)) -> rule6))]
("Bob" "is" "white" "-")
((((((triple2) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is white.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule7)) -> rule6))]
("Bob" "is" "white" "+")
((((((triple2) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "smart" "-")
Harry is kind.
Unknown
rconc
[@2: Harry is kind.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Harry" "is" "kind" "+")
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "cold" "-")
Harry is nice.
Unknown
rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "nice" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Anne is not nice.[(triple1)] Bob is red.[(triple2)] Erin is cold.[(triple3)] Harry is not smart.[(triple4)] @1: Bob is smart.[(((triple2) -> rule1))] Erin is kind.[(((triple3) -> rule4))] Erin is smart.[(((triple3) -> rule2))] @2: Bob is nice.[(((((triple2) -> rule1)) -> rule7))] Erin is nice.[(((((triple3) -> rule2)) -> rule7))] @3: Bob is not white.[(((((((triple2) -> rule1)) -> rule7)) -> rule6))] Erin is not white.[(((((((triple3) -> rule2)) -> rule7)) -> rule6))]
Anne is not nice.
("Anne" "is" "nice" "-")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Harry is not smart.
("Harry" "is" "smart" "-")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple3) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple3) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
((((triple3) -> (rule2 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Bob is not white.
("Bob" "is" "white" "-")
((((((triple2) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Erin is not white.
("Erin" "is" "white" "-")
((((((triple3) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Erin is not white.
("Erin" "is" "white" "-")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3