Dave is nice. Dave is red. Erin is green. Erin is not nice. Erin is not red. Gary is green. Gary is not nice. Gary is white. Harry is green. Harry is nice. Harry is smart. Harry is white. All nice people are smart. White people are smart. All rough people are not green. If someone is rough then they are blue. Green, nice people are red. If Harry is not red then Harry is smart.
Dave is nice.
("Dave" "is" "nice" "+")
Dave is red.
("Dave" "is" "red" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is not nice.
("Erin" "is" "nice" "-")
Erin is not red.
("Erin" "is" "red" "-")
Gary is green.
("Gary" "is" "green" "+")
Gary is not nice.
("Gary" "is" "nice" "-")
Gary is white.
("Gary" "is" "white" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
All nice people are smart.
((("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
White people are smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
All rough people are not green.
((("someone" "is" "rough" "+")) -> ("someone" "is" "green" "-"))
If someone is rough then they are blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
Green, nice people are red.
((("someone" "is" "green" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If Harry is not red then Harry is smart.
((("Harry" "is" "red" "~")) -> ("Harry" "is" "smart" "+"))
Erin is green.
True
1
proof
[(triple3)]
("Erin" "is" "green" "+")
triple3
Dave is not nice.
False
1
inv-proof
[(triple1)]
("Dave" "is" "nice" "-")
triple1
Harry is red.
True
3
proof
[(((triple9 triple10) -> rule5))]
("Harry" "is" "red" "+")
((triple9 triple10) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Gary is not smart.
False
2
inv-proof
[(((triple8) -> rule2))]
("Gary" "is" "smart" "-")
((triple8) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Erin is not smart.
Unknown
inv-rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "smart" "-")
Harry is blue.
Unknown
rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "blue" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Dave is nice.[(triple1)] Dave is red.[(triple2)] Erin is green.[(triple3)] Erin is not nice.[(triple4)] Erin is not red.[(triple5)] Gary is green.[(triple6)] Gary is not nice.[(triple7)] Gary is white.[(triple8)] Harry is green.[(triple9)] Harry is nice.[(triple10)] Harry is smart.[(triple11 OR ((triple10) -> rule1) OR ((triple12) -> rule2))] Harry is white.[(triple12)] @1: Dave is smart.[(((triple1) -> rule1))] Gary is smart.[(((triple8) -> rule2))] Harry is red.[(((triple9 triple10) -> rule5))]
Dave is nice.
("Dave" "is" "nice" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Erin is green.
("Erin" "is" "green" "+")
triple3
Erin is not nice.
("Erin" "is" "nice" "-")
triple4
Erin is not red.
("Erin" "is" "red" "-")
triple5
Gary is green.
("Gary" "is" "green" "+")
triple6
Gary is not nice.
("Gary" "is" "nice" "-")
triple7
Gary is white.
("Gary" "is" "white" "+")
triple8
Harry is green.
("Harry" "is" "green" "+")
triple9
Harry is nice.
("Harry" "is" "nice" "+")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
triple11
((triple10) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((triple12) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple12
Dave is smart.
("Dave" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple8) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple9 triple10) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1