Charlie is big. Charlie is cold. Charlie is kind. Charlie is white. Charlie is young. Harry is cold. Harry is kind. Harry is quiet. Harry is white. Harry is young. Kind people are big. Quiet, young people are white. Big, furry people are young. If Charlie is cold then Charlie is young. Quiet, big people are furry. Furry, white people are quiet.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
Kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
Quiet, young people are white.
((("someone" "is" "quiet" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
Big, furry people are young.
((("someone" "is" "big" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
If Charlie is cold then Charlie is young.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "young" "+"))
Quiet, big people are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
Furry, white people are quiet.
((("someone" "is" "furry" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
Charlie is white.
True
1
proof
[(triple4)]
("Charlie" "is" "white" "+")
triple4
Charlie is not young.
False
1
inv-proof
[(triple5 OR ((triple2) -> rule4))]
("Charlie" "is" "young" "-")
triple5
((triple2) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Harry is big.
True
2
proof
[(((triple7) -> rule1))]
("Harry" "is" "big" "+")
((triple7) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple7) -> rule1))]
("Harry" "is" "big" "-")
((triple7) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
True
4
proof
[(((triple8 ((triple7) -> rule1)) -> rule5))]
("Harry" "is" "furry" "+")
((triple8 ((triple7) -> (rule1 % int2))) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not furry.
False
4
inv-proof
[(((triple8 ((triple7) -> rule1)) -> rule5))]
("Harry" "is" "furry" "-")
((triple8 ((triple7) -> (rule1 % int2))) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Charlie is not furry.
Unknown
inv-rconc
[@2: Charlie is furry.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is quiet.
Unknown
rconc
[@2: Charlie is quiet.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Charlie is big.[(triple1 OR ((triple3) -> rule1))] Charlie is cold.[(triple2)] Charlie is kind.[(triple3)] Charlie is white.[(triple4)] Charlie is young.[(triple5 OR ((triple2) -> rule4))] Harry is cold.[(triple6)] Harry is kind.[(triple7)] Harry is quiet.[(triple8)] Harry is white.[(triple9 OR ((triple8 triple10) -> rule2) OR ((triple8 ((((triple7) -> rule1) ((triple8 ((triple7) -> rule1)) -> rule5)) -> rule3)) -> rule2))] Harry is young.[(triple10 OR ((((triple7) -> rule1) ((triple8 ((triple7) -> rule1)) -> rule5)) -> rule3))] @1: Harry is big.[(((triple7) -> rule1))] @2: Harry is furry.[(((triple8 ((triple7) -> rule1)) -> rule5))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple3) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
((triple2) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
triple6
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Harry is quiet.
("Harry" "is" "quiet" "+")
triple8
Harry is white.
("Harry" "is" "white" "+")
triple9
((triple8 triple10) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple8 ((((triple7) -> (rule1 % int4)) ((triple8 ((triple7) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
int4
Harry is young.
("Harry" "is" "young" "+")
triple10
((((triple7) -> (rule1 % int3)) ((triple8 ((triple7) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is big.
("Harry" "is" "big" "+")
((triple7) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple8 ((triple7) -> (rule1 % int2))) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2