Charlie is not blue. Charlie is quiet. Charlie is rough. Charlie is smart. Charlie is white. Charlie is young. Dave is blue. Dave is green. Dave is rough. Gary is blue. Gary is not green. Gary is quiet. Gary is smart. Gary is white. Gary is young. Green, rough people are white. All smart, rough people are white. If someone is white and not blue then they are young. If Dave is young and Dave is green then Dave is rough. If Charlie is blue then Charlie is not smart. All white, blue people are smart. If Gary is quiet and Gary is white then Gary is young. If someone is young and not white then they are quiet.
Charlie is not blue.
("Charlie" "is" "blue" "-")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is not green.
("Gary" "is" "green" "-")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
Green, rough people are white.
((("someone" "is" "green" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
All smart, rough people are white.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
If someone is white and not blue then they are young.
((("someone" "is" "white" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "young" "+"))
If Dave is young and Dave is green then Dave is rough.
((("Dave" "is" "young" "+") ("Dave" "is" "green" "+")) -> ("Dave" "is" "rough" "+"))
If Charlie is blue then Charlie is not smart.
((("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "smart" "-"))
All white, blue people are smart.
((("someone" "is" "white" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
If Gary is quiet and Gary is white then Gary is young.
((("Gary" "is" "quiet" "+") ("Gary" "is" "white" "+")) -> ("Gary" "is" "young" "+"))
If someone is young and not white then they are quiet.
((("someone" "is" "young" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "quiet" "+"))
Charlie is smart.
True
1
proof
[(triple4)]
("Charlie" "is" "smart" "+")
triple4
Dave is not rough.
False
1
inv-proof
[(triple9)]
("Dave" "is" "rough" "-")
triple9
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "quiet" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Charlie is not blue.[(triple1)] Charlie is quiet.[(triple2)] Charlie is rough.[(triple3)] Charlie is smart.[(triple4)] Charlie is white.[(triple5 OR ((triple4 triple3) -> rule2))] Charlie is young.[(triple6 OR ((triple5 triple1) -> rule3) OR ((((triple4 triple3) -> rule2) triple1) -> rule3))] Dave is blue.[(triple7)] Dave is green.[(triple8)] Dave is rough.[(triple9)] Gary is blue.[(triple10)] Gary is not green.[(triple11)] Gary is quiet.[(triple12)] Gary is smart.[(triple13 OR ((triple14 triple10) -> rule6))] Gary is white.[(triple14)] Gary is young.[(triple15 OR ((triple12 triple14) -> rule7))] @1: Dave is white.[(((triple8 triple9) -> rule1))] @2: Dave is smart.[(((((triple8 triple9) -> rule1) triple7) -> rule6))]
Charlie is not blue.
("Charlie" "is" "blue" "-")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
Charlie is white.
("Charlie" "is" "white" "+")
triple5
((triple4 triple3) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple6
((triple5 triple1) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple4 triple3) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
triple7
Dave is green.
("Dave" "is" "green" "+")
triple8
Dave is rough.
("Dave" "is" "rough" "+")
triple9
Gary is blue.
("Gary" "is" "blue" "+")
triple10
Gary is not green.
("Gary" "is" "green" "-")
triple11
Gary is quiet.
("Gary" "is" "quiet" "+")
triple12
Gary is smart.
("Gary" "is" "smart" "+")
triple13
((triple14 triple10) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple14
Gary is young.
("Gary" "is" "young" "+")
triple15
((triple12 triple14) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple8 triple9) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((((triple8 triple9) -> (rule1 % int2)) triple7) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2