Charlie is not cold. Charlie is kind. Dave is cold. Gary is round. Harry is cold. Harry is kind. Harry is not nice. All kind, cold things are not nice. Red things are smart. Nice things are not smart. All nice, round things are not white. All kind things are white. If something is white and not cold then it is red. If Harry is kind then Harry is white. White things are round.
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is kind.
("Charlie" "is" "kind" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is not nice.
("Harry" "is" "nice" "-")
All kind, cold things are not nice.
((("something" "is" "kind" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "-"))
Red things are smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
Nice things are not smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "-"))
All nice, round things are not white.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "white" "-"))
All kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
If something is white and not cold then it is red.
((("something" "is" "white" "+") ("something" "is" "cold" "~")) -> ("something" "is" "red" "+"))
If Harry is kind then Harry is white.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "white" "+"))
White things are round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
Charlie is not cold.
True
1
proof
[(triple1)]
("Charlie" "is" "cold" "-")
triple1
Harry is not kind.
False
1
inv-proof
[(triple6)]
("Harry" "is" "kind" "-")
triple6
Harry is white.
True
2
proof
[(((triple6) -> rule5) OR ((triple6) -> rule7))]
("Harry" "is" "white" "+")
((triple6) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple6) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple2) -> rule5))]
("Charlie" "is" "white" "-")
((triple2) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
True
4
proof
[(((((triple2) -> rule5) triple1) -> rule6))]
("Charlie" "is" "red" "+")
((((triple2) -> (rule5 % int2)) triple1) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not red.
False
4
inv-proof
[(((((triple2) -> rule5) triple1) -> rule6))]
("Charlie" "is" "red" "-")
((((triple2) -> (rule5 % int2)) triple1) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is smart.
True
5
proof
[(((((((triple2) -> rule5) triple1) -> rule6)) -> rule2))]
("Charlie" "is" "smart" "+")
((((((triple2) -> (rule5 % int3)) triple1) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is not smart.
False
5
inv-proof
[(((((((triple2) -> rule5) triple1) -> rule6)) -> rule2))]
("Charlie" "is" "smart" "-")
((((((triple2) -> (rule5 % int3)) triple1) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "white" "-")
Harry is red.
Unknown
rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "red" "+")
Dave is not round.
Unknown
inv-rconc
[@2: Dave is round.[CWA. Example of deepest failure = (rule8 <- rule5 <- FAIL)]]
("Dave" "is" "round" "-")
Gary is red.
Unknown
rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "red" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Charlie is kind.[(triple2)] Charlie is not cold.[(triple1)] Dave is cold.[(triple3)] Gary is round.[(triple4)] Harry is cold.[(triple5)] Harry is kind.[(triple6)] Harry is not nice.[(triple7 OR ((triple6 triple5) -> rule1))] @1: Charlie is white.[(((triple2) -> rule5))] Harry is white.[(((triple6) -> rule5) OR ((triple6) -> rule7))] @2: Charlie is red.[(((((triple2) -> rule5) triple1) -> rule6))] Charlie is round.[(((((triple2) -> rule5)) -> rule8))] Harry is round.[(((((triple6) -> rule5)) -> rule8) OR ((((triple6) -> rule7)) -> rule8))] @3: Charlie is smart.[(((((((triple2) -> rule5) triple1) -> rule6)) -> rule2))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Gary is round.
("Gary" "is" "round" "+")
triple4
Harry is cold.
("Harry" "is" "cold" "+")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is not nice.
("Harry" "is" "nice" "-")
triple7
((triple6 triple5) -> (rule1 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple2) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple6) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple6) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((((triple2) -> (rule5 % int2)) triple1) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((triple6) -> (rule5 % int2))) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple6) -> (rule7 % int2))) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((((triple2) -> (rule5 % int3)) triple1) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3