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