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