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