Charlie is rough. Erin is furry. Fiona is white. Gary is rough. Rough things are young. Kind, young things are rough. If Erin is white then Erin is smart. If something is kind and not rough then it is not white. All young, furry things are white. Rough, smart things are white. Young, rough things are smart. Furry, white things are smart.
Charlie is rough.
("Charlie" "is" "rough" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
Kind, young things are rough.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If Erin is white then Erin is smart.
((("Erin" "is" "white" "+")) -> ("Erin" "is" "smart" "+"))
If something is kind and not rough then it is not white.
((("something" "is" "kind" "+") ("something" "is" "rough" "~")) -> ("something" "is" "white" "-"))
All young, furry things are white.
((("something" "is" "young" "+") ("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
Rough, smart things are white.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
Young, rough things are smart.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
Furry, white things are smart.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
Charlie is rough.
True
1
proof
[(triple1)]
("Charlie" "is" "rough" "+")
triple1
Charlie is not rough.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "rough" "-")
triple1
Charlie is young.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "young" "+")
((triple1) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Gary is not young.
False
2
inv-proof
[(((triple4) -> rule1))]
("Gary" "is" "young" "-")
((triple4) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Charlie is smart.
True
4
proof
[(((((triple1) -> rule1) triple1) -> rule7))]
("Charlie" "is" "smart" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule7 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Gary is not smart.
False
4
inv-proof
[(((((triple4) -> rule1) triple4) -> rule7))]
("Gary" "is" "smart" "-")
((((triple4) -> (rule1 % int2)) triple4) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Charlie is white.
True
6
proof
[(((triple1 ((((triple1) -> rule1) triple1) -> rule7)) -> rule6))]
("Charlie" "is" "white" "+")
((triple1 ((((triple1) -> (rule1 % int3)) triple1) -> (rule7 % int2))) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is not white.
False
6
inv-proof
[(((triple1 ((((triple1) -> rule1) triple1) -> rule7)) -> rule6))]
("Charlie" "is" "white" "-")
((triple1 ((((triple1) -> (rule1 % int3)) triple1) -> (rule7 % int2))) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Fiona is not rough.
Unknown
inv-rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is smart.
Unknown
rconc
[@2: Fiona is smart.[CWA. Example of deepest failure = (rule7 <- rule2 <- FAIL)]]
("Fiona" "is" "smart" "+")
Fiona is not young.
Unknown
inv-rconc
[@2: Fiona is young.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Fiona" "is" "young" "-")
Erin is white.
Unknown
rconc
[@3: Erin is white.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule2 <- FAIL)]]
("Erin" "is" "white" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Charlie is rough.[(triple1)] Erin is furry.[(triple2)] Fiona is white.[(triple3)] Gary is rough.[(triple4)] @1: Charlie is young.[(((triple1) -> rule1))] Gary is young.[(((triple4) -> rule1))] @2: Charlie is smart.[(((((triple1) -> rule1) triple1) -> rule7))] Gary is smart.[(((((triple4) -> rule1) triple4) -> rule7))] @3: Charlie is white.[(((triple1 ((((triple1) -> rule1) triple1) -> rule7)) -> rule6))] Gary is white.[(((triple4 ((((triple4) -> rule1) triple4) -> rule7)) -> rule6))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
Fiona is white.
("Fiona" "is" "white" "+")
triple3
Gary is rough.
("Gary" "is" "rough" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
((triple1) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple4) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule7 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((triple4) -> (rule1 % int2)) triple4) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((triple1 ((((triple1) -> (rule1 % int3)) triple1) -> (rule7 % int2))) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
((triple4 ((((triple4) -> (rule1 % int3)) triple4) -> (rule7 % int2))) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3