Charlie is blue. Charlie is furry. Charlie is not green. Charlie is nice. Charlie is rough. Charlie is not smart. Charlie is white. Dave is blue. Dave is nice. Dave is white. Erin is blue. Erin is furry. Erin is green. Erin is not smart. Erin is not white. If something is blue and green then it is nice.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is not green.
("Charlie" "is" "green" "-")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is not smart.
("Charlie" "is" "smart" "-")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is not smart.
("Erin" "is" "smart" "-")
Erin is not white.
("Erin" "is" "white" "-")
If something is blue and green then it is nice.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
Dave is nice.
True
1
proof
[(triple9)]
("Dave" "is" "nice" "+")
triple9
Erin is not green.
False
1
inv-proof
[(triple13)]
("Erin" "is" "green" "-")
triple13
Erin is nice.
True
3
proof
[(((triple11 triple13) -> rule1))]
("Erin" "is" "nice" "+")
((triple11 triple13) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not nice.
False
3
inv-proof
[(((triple11 triple13) -> rule1))]
("Erin" "is" "nice" "-")
((triple11 triple13) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Charlie is blue.[(triple1)] Charlie is furry.[(triple2)] Charlie is nice.[(triple4)] Charlie is not green.[(triple3)] Charlie is not smart.[(triple6)] Charlie is rough.[(triple5)] Charlie is white.[(triple7)] Dave is blue.[(triple8)] Dave is nice.[(triple9)] Dave is white.[(triple10)] Erin is blue.[(triple11)] Erin is furry.[(triple12)] Erin is green.[(triple13)] Erin is not smart.[(triple14)] Erin is not white.[(triple15)] @1: Erin is nice.[(((triple11 triple13) -> rule1))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is not green.
("Charlie" "is" "green" "-")
triple3
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple6
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
triple8
Dave is nice.
("Dave" "is" "nice" "+")
triple9
Dave is white.
("Dave" "is" "white" "+")
triple10
Erin is blue.
("Erin" "is" "blue" "+")
triple11
Erin is furry.
("Erin" "is" "furry" "+")
triple12
Erin is green.
("Erin" "is" "green" "+")
triple13
Erin is not smart.
("Erin" "is" "smart" "-")
triple14
Erin is not white.
("Erin" "is" "white" "-")
triple15
Erin is nice.
("Erin" "is" "nice" "+")
((triple11 triple13) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1