Charlie is big. Charlie is furry. Charlie is smart. Charlie is white. Fiona is big. Fiona is furry. Fiona is green. Fiona is smart. Gary is big. Gary is not furry. Gary is green. Gary is rough. Gary is smart. Gary is white. Gary is young. If something is smart then it is rough. If something is furry and not rough then it is young. If Gary is rough and Gary is young then Gary is green. If something is furry and not rough then it is not white. If something is big and not furry then it is green. If something is young and smart then it is green.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is not furry.
("Gary" "is" "furry" "-")
Gary is green.
("Gary" "is" "green" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
If something is smart then it is rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If something is furry and not rough then it is young.
((("something" "is" "furry" "+") ("something" "is" "rough" "~")) -> ("something" "is" "young" "+"))
If Gary is rough and Gary is young then Gary is green.
((("Gary" "is" "rough" "+") ("Gary" "is" "young" "+")) -> ("Gary" "is" "green" "+"))
If something is furry and not rough then it is not white.
((("something" "is" "furry" "+") ("something" "is" "rough" "~")) -> ("something" "is" "white" "-"))
If something is big and not furry then it is green.
((("something" "is" "big" "+") ("something" "is" "furry" "~")) -> ("something" "is" "green" "+"))
If something is young and smart then it is green.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
Charlie is white.
True
1
proof
[(triple4)]
("Charlie" "is" "white" "+")
triple4
Gary is not rough.
False
1
inv-proof
[(triple12 OR ((triple13) -> rule1))]
("Gary" "is" "rough" "-")
triple12
((triple13) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Charlie is not green.
Unknown
inv-rconc
[@2: Charlie is green.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Charlie" "is" "green" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
@0: Charlie is big.[(triple1)] Charlie is furry.[(triple2)] Charlie is smart.[(triple3)] Charlie is white.[(triple4)] Fiona is big.[(triple5)] Fiona is furry.[(triple6)] Fiona is green.[(triple7)] Fiona is smart.[(triple8)] Gary is big.[(triple9)] Gary is green.[(triple11 OR ((triple12 triple15) -> rule3) OR ((triple15 triple13) -> rule6) OR ((triple9 triple10) -> rule5) OR ((((triple13) -> rule1) triple15) -> rule3))] Gary is not furry.[(triple10)] Gary is rough.[(triple12 OR ((triple13) -> rule1))] Gary is smart.[(triple13)] Gary is white.[(triple14)] Gary is young.[(triple15)] @1: Charlie is rough.[(((triple3) -> rule1))] Fiona is rough.[(((triple8) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Fiona is big.
("Fiona" "is" "big" "+")
triple5
Fiona is furry.
("Fiona" "is" "furry" "+")
triple6
Fiona is green.
("Fiona" "is" "green" "+")
triple7
Fiona is smart.
("Fiona" "is" "smart" "+")
triple8
Gary is big.
("Gary" "is" "big" "+")
triple9
Gary is green.
("Gary" "is" "green" "+")
triple11
((triple12 triple15) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple15 triple13) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((triple9 triple10) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple13) -> (rule1 % int2)) triple15) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not furry.
("Gary" "is" "furry" "-")
triple10
Gary is rough.
("Gary" "is" "rough" "+")
triple12
((triple13) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple13
Gary is white.
("Gary" "is" "white" "+")
triple14
Gary is young.
("Gary" "is" "young" "+")
triple15
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple3) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple8) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1