Charlie is furry. Charlie is green. Charlie is kind. Charlie is rough. Charlie is smart. Erin is young. Gary is furry. Gary is kind. Gary is smart. Harry is rough. All rough people are kind. Rough, furry people are kind. If someone is furry then they are blue. Kind, smart people are blue. All blue, furry people are smart. If Harry is kind then Harry is furry. All kind, smart people are not young. If Harry is not kind then Harry is green.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is rough.
("Harry" "is" "rough" "+")
All rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
Rough, furry people are kind.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
If someone is furry then they are blue.
((("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
Kind, smart people are blue.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
All blue, furry people are smart.
((("someone" "is" "blue" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
If Harry is kind then Harry is furry.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "furry" "+"))
All kind, smart people are not young.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "young" "-"))
If Harry is not kind then Harry is green.
((("Harry" "is" "kind" "~")) -> ("Harry" "is" "green" "+"))
Harry is rough.
True
1
proof
[(triple10)]
("Harry" "is" "rough" "+")
triple10
Gary is not kind.
False
1
inv-proof
[(triple8)]
("Gary" "is" "kind" "-")
triple8
Gary is blue.
True
2
proof
[(((triple7) -> rule3) OR ((triple8 triple9) -> rule4))]
("Gary" "is" "blue" "+")
((triple7) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple8 triple9) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Charlie is young.
False
3
inv-proof
[(((triple3 triple5) -> rule7) OR ((((triple4) -> rule1) triple5) -> rule7) OR ((((triple4 triple1) -> rule2) triple5) -> rule7) OR ((triple3 ((((triple1) -> rule3) triple1) -> rule5)) -> rule7) OR ((((triple4) -> rule1) ((((triple1) -> rule3) triple1) -> rule5)) -> rule7) OR ((((triple4 triple1) -> rule2) ((((triple1) -> rule3) triple1) -> rule5)) -> rule7))]
("Charlie" "is" "young" "+")
((triple3 triple5) -> (rule7 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
((((triple4) -> (rule1 % int2)) triple5) -> (rule7 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple4 triple1) -> (rule2 % int2)) triple5) -> (rule7 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((triple3 ((((triple1) -> (rule3 % int3)) triple1) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
((((triple4) -> (rule1 % int4)) ((((triple1) -> (rule3 % int3)) triple1) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
((((triple4 triple1) -> (rule2 % int4)) ((((triple1) -> (rule3 % int3)) triple1) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Harry is furry.
True
3
proof
[(((((triple10) -> rule1)) -> rule6))]
("Harry" "is" "furry" "+")
((((triple10) -> (rule1 % int2))) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not furry.
False
3
inv-proof
[(((((triple10) -> rule1)) -> rule6))]
("Harry" "is" "furry" "-")
((((triple10) -> (rule1 % int2))) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is blue.
True
4
proof
[(((((((triple10) -> rule1)) -> rule6)) -> rule3))]
("Harry" "is" "blue" "+")
((((((triple10) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is not blue.
False
4
inv-proof
[(((((((triple10) -> rule1)) -> rule6)) -> rule3))]
("Harry" "is" "blue" "-")
((((((triple10) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is smart.
True
8
proof
[(((((((((triple10) -> rule1)) -> rule6)) -> rule3) ((((triple10) -> rule1)) -> rule6)) -> rule5))]
("Harry" "is" "smart" "+")
((((((((triple10) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule3 % int2)) ((((triple10) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
Harry is not smart.
False
8
inv-proof
[(((((((((triple10) -> rule1)) -> rule6)) -> rule3) ((((triple10) -> rule1)) -> rule6)) -> rule5))]
("Harry" "is" "smart" "-")
((((((((triple10) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule3 % int2)) ((((triple10) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
Harry is not young.
True
11
proof
[(((((triple10) -> rule1) ((((((((triple10) -> rule1)) -> rule6)) -> rule3) ((((triple10) -> rule1)) -> rule6)) -> rule5)) -> rule7))]
("Harry" "is" "young" "-")
((((triple10) -> (rule1 % int5)) ((((((((triple10) -> (rule1 % int5))) -> (rule6 % int4))) -> (rule3 % int3)) ((((triple10) -> (rule1 % int5))) -> (rule6 % int4))) -> (rule5 % int2))) -> (rule7 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is kind.
("Harry" "is" "kind" "+")
int5
Harry is young.
False
11
inv-proof
[(((((triple10) -> rule1) ((((((((triple10) -> rule1)) -> rule6)) -> rule3) ((((triple10) -> rule1)) -> rule6)) -> rule5)) -> rule7))]
("Harry" "is" "young" "+")
((((triple10) -> (rule1 % int5)) ((((((((triple10) -> (rule1 % int5))) -> (rule6 % int4))) -> (rule3 % int3)) ((((triple10) -> (rule1 % int5))) -> (rule6 % int4))) -> (rule5 % int2))) -> (rule7 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is kind.
("Harry" "is" "kind" "+")
int5
Erin is not kind.
Unknown
inv-rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "kind" "-")
Erin is smart.
Unknown
rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "smart" "+")
Erin is not blue.
Unknown
inv-rconc
[@2: Erin is blue.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Erin" "is" "blue" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Harry" "is" "green" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
@0: Charlie is furry.[(triple1)] Charlie is green.[(triple2)] Charlie is kind.[(triple3 OR ((triple4) -> rule1) OR ((triple4 triple1) -> rule2))] Charlie is rough.[(triple4)] Charlie is smart.[(triple5 OR ((((triple1) -> rule3) triple1) -> rule5))] Erin is young.[(triple6)] Gary is furry.[(triple7)] Gary is kind.[(triple8)] Gary is smart.[(triple9 OR ((((triple7) -> rule3) triple7) -> rule5))] Harry is rough.[(triple10)] @1: Charlie is blue.[(((triple1) -> rule3) OR ((triple3 triple5) -> rule4) OR ((((triple4) -> rule1) triple5) -> rule4) OR ((((triple4 triple1) -> rule2) triple5) -> rule4))] Charlie is not young.[(((triple3 triple5) -> rule7) OR ((((triple4) -> rule1) triple5) -> rule7) OR ((((triple4 triple1) -> rule2) triple5) -> rule7) OR ((triple3 ((((triple1) -> rule3) triple1) -> rule5)) -> rule7) OR ((((triple4) -> rule1) ((((triple1) -> rule3) triple1) -> rule5)) -> rule7) OR ((((triple4 triple1) -> rule2) ((((triple1) -> rule3) triple1) -> rule5)) -> rule7))] Gary is blue.[(((triple7) -> rule3) OR ((triple8 triple9) -> rule4))] Gary is not young.[(((triple8 triple9) -> rule7) OR ((triple8 ((((triple7) -> rule3) triple7) -> rule5)) -> rule7))] Harry is kind.[(((triple10) -> rule1))] @2: Harry is furry.[(((((triple10) -> rule1)) -> rule6))] @3: Harry is blue.[(((((((triple10) -> rule1)) -> rule6)) -> rule3))] @4: Harry is smart.[(((((((((triple10) -> rule1)) -> rule6)) -> rule3) ((((triple10) -> rule1)) -> rule6)) -> rule5))] @5: Harry is not young.[(((((triple10) -> rule1) ((((((((triple10) -> rule1)) -> rule6)) -> rule3) ((((triple10) -> rule1)) -> rule6)) -> rule5)) -> rule7))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
((triple4) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((triple4 triple1) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
((((triple1) -> (rule3 % int2)) triple1) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple6
Gary is furry.
("Gary" "is" "furry" "+")
triple7
Gary is kind.
("Gary" "is" "kind" "+")
triple8
Gary is smart.
("Gary" "is" "smart" "+")
triple9
((((triple7) -> (rule3 % int2)) triple7) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
triple10
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple1) -> (rule3 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((triple3 triple5) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((triple4) -> (rule1 % int2)) triple5) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple4 triple1) -> (rule2 % int2)) triple5) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not young.
("Charlie" "is" "young" "-")
((triple3 triple5) -> (rule7 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
((((triple4) -> (rule1 % int2)) triple5) -> (rule7 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple4 triple1) -> (rule2 % int2)) triple5) -> (rule7 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((triple3 ((((triple1) -> (rule3 % int3)) triple1) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
((((triple4) -> (rule1 % int4)) ((((triple1) -> (rule3 % int3)) triple1) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
((((triple4 triple1) -> (rule2 % int4)) ((((triple1) -> (rule3 % int3)) triple1) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Gary is blue.
("Gary" "is" "blue" "+")
((triple7) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple8 triple9) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not young.
("Gary" "is" "young" "-")
((triple8 triple9) -> (rule7 % int1))
Gary is not young.
("Gary" "is" "young" "-")
int1
((triple8 ((((triple7) -> (rule3 % int3)) triple7) -> (rule5 % int2))) -> (rule7 % int1))
Gary is not young.
("Gary" "is" "young" "-")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
((triple10) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((((triple10) -> (rule1 % int2))) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((((((triple10) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
((((((((triple10) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule3 % int2)) ((((triple10) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
Harry is not young.
("Harry" "is" "young" "-")
((((triple10) -> (rule1 % int5)) ((((((((triple10) -> (rule1 % int5))) -> (rule6 % int4))) -> (rule3 % int3)) ((((triple10) -> (rule1 % int5))) -> (rule6 % int4))) -> (rule5 % int2))) -> (rule7 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is kind.
("Harry" "is" "kind" "+")
int5