Charlie is big. Charlie is furry. Charlie is kind. Charlie is young. Erin is cold. Erin is rough. Erin is smart. Fiona is cold. Fiona is furry. Fiona is smart. Harry is big. Harry is cold. Harry is furry. Harry is kind. Harry is rough. Harry is smart. Kind things are furry. Rough things are kind. Young things are big.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Kind things are furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
Rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
Young things are big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
Harry is furry.
True
1
proof
[(triple13 OR ((triple14) -> rule1) OR ((((triple15) -> rule2)) -> rule1))]
("Harry" "is" "furry" "+")
triple13
((triple14) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple15) -> (rule2 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not kind.
False
1
inv-proof
[(triple14 OR ((triple15) -> rule2))]
("Harry" "is" "kind" "-")
triple14
((triple15) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Erin is kind.
True
2
proof
[(((triple6) -> rule2))]
("Erin" "is" "kind" "+")
((triple6) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not kind.
False
2
inv-proof
[(((triple6) -> rule2))]
("Erin" "is" "kind" "-")
((triple6) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is furry.
True
3
proof
[(((((triple6) -> rule2)) -> rule1))]
("Erin" "is" "furry" "+")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not furry.
False
3
inv-proof
[(((((triple6) -> rule2)) -> rule1))]
("Erin" "is" "furry" "-")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Fiona is not big.
Unknown
inv-rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "big" "-")
Erin is big.
Unknown
rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "big" "+")
Fiona is not kind.
Unknown
inv-rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "kind" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
@0: Charlie is big.[(triple1 OR ((triple4) -> rule3))] Charlie is furry.[(triple2 OR ((triple3) -> rule1))] Charlie is kind.[(triple3)] Charlie is young.[(triple4)] Erin is cold.[(triple5)] Erin is rough.[(triple6)] Erin is smart.[(triple7)] Fiona is cold.[(triple8)] Fiona is furry.[(triple9)] Fiona is smart.[(triple10)] Harry is big.[(triple11)] Harry is cold.[(triple12)] Harry is furry.[(triple13 OR ((triple14) -> rule1) OR ((((triple15) -> rule2)) -> rule1))] Harry is kind.[(triple14 OR ((triple15) -> rule2))] Harry is rough.[(triple15)] Harry is smart.[(triple16)] @1: Erin is kind.[(((triple6) -> rule2))] @2: Erin is furry.[(((((triple6) -> rule2)) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple4) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
((triple3) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is young.
("Charlie" "is" "young" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
triple5
Erin is rough.
("Erin" "is" "rough" "+")
triple6
Erin is smart.
("Erin" "is" "smart" "+")
triple7
Fiona is cold.
("Fiona" "is" "cold" "+")
triple8
Fiona is furry.
("Fiona" "is" "furry" "+")
triple9
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
Harry is big.
("Harry" "is" "big" "+")
triple11
Harry is cold.
("Harry" "is" "cold" "+")
triple12
Harry is furry.
("Harry" "is" "furry" "+")
triple13
((triple14) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple15) -> (rule2 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
triple14
((triple15) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple15
Harry is smart.
("Harry" "is" "smart" "+")
triple16
Erin is kind.
("Erin" "is" "kind" "+")
((triple6) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2