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