Bob is green. Bob is kind. Bob is quiet. Bob is smart. Bob is white. Erin is green. Erin is kind. Erin is quiet. Erin is red. Fiona is green. Fiona is quiet. Harry is green. Harry is quiet. Harry is smart. Harry is white. If someone is white and green then they are red. All red people are kind. All smart, quiet people are red.
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is white and green then they are red.
((("someone" "is" "white" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
All red people are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
All smart, quiet people are red.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
Erin is quiet.
True
1
proof
[(triple8)]
("Erin" "is" "quiet" "+")
triple8
Fiona is not green.
False
1
inv-proof
[(triple10)]
("Fiona" "is" "green" "-")
triple10
Bob is red.
True
3
proof
[(((triple4 triple3) -> rule3) OR ((triple5 triple1) -> rule1))]
("Bob" "is" "red" "+")
((triple4 triple3) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple5 triple1) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Harry is not red.
False
3
inv-proof
[(((triple14 triple13) -> rule3) OR ((triple15 triple12) -> rule1))]
("Harry" "is" "red" "-")
((triple14 triple13) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple15 triple12) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is kind.
True
4
proof
[(((((triple14 triple13) -> rule3)) -> rule2) OR ((((triple15 triple12) -> rule1)) -> rule2))]
("Harry" "is" "kind" "+")
((((triple14 triple13) -> (rule3 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple15 triple12) -> (rule1 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not kind.
False
4
inv-proof
[(((((triple14 triple13) -> rule3)) -> rule2) OR ((((triple15 triple12) -> rule1)) -> rule2))]
("Harry" "is" "kind" "-")
((((triple14 triple13) -> (rule3 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple15 triple12) -> (rule1 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Fiona is not red.
Unknown
inv-rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "red" "-")
Fiona is kind.
Unknown
rconc
[@2: Fiona is kind.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Fiona" "is" "kind" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is green.[(triple1)] Bob is kind.[(triple2 OR ((((triple4 triple3) -> rule3)) -> rule2) OR ((((triple5 triple1) -> rule1)) -> rule2))] Bob is quiet.[(triple3)] Bob is smart.[(triple4)] Bob is white.[(triple5)] Erin is green.[(triple6)] Erin is kind.[(triple7 OR ((triple9) -> rule2))] Erin is quiet.[(triple8)] Erin is red.[(triple9)] Fiona is green.[(triple10)] Fiona is quiet.[(triple11)] Harry is green.[(triple12)] Harry is quiet.[(triple13)] Harry is smart.[(triple14)] Harry is white.[(triple15)] @1: Bob is red.[(((triple4 triple3) -> rule3) OR ((triple5 triple1) -> rule1))] Harry is red.[(((triple14 triple13) -> rule3) OR ((triple15 triple12) -> rule1))] @2: Harry is kind.[(((((triple14 triple13) -> rule3)) -> rule2) OR ((((triple15 triple12) -> rule1)) -> rule2))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
((((triple4 triple3) -> (rule3 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((triple5 triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
Erin is green.
("Erin" "is" "green" "+")
triple6
Erin is kind.
("Erin" "is" "kind" "+")
triple7
((triple9) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple8
Erin is red.
("Erin" "is" "red" "+")
triple9
Fiona is green.
("Fiona" "is" "green" "+")
triple10
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple11
Harry is green.
("Harry" "is" "green" "+")
triple12
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
Harry is smart.
("Harry" "is" "smart" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
Bob is red.
("Bob" "is" "red" "+")
((triple4 triple3) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
((triple5 triple1) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple14 triple13) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple15 triple12) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((((triple14 triple13) -> (rule3 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple15 triple12) -> (rule1 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2