Charlie is blue. Charlie is not cold. Charlie is furry. Charlie is nice. Charlie is quiet. Charlie is rough. Charlie is young. Dave is quiet. Dave is rough. Fiona is furry. Fiona is nice. Harry is blue. Blue people are rough. All rough people are blue. If Charlie is quiet and Charlie is blue then Charlie is nice. All furry people are nice. All cold, quiet people are nice. If someone is furry and not rough then they are not cold. All rough people are quiet. All nice people are quiet.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Blue people are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
All rough people are blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
If Charlie is quiet and Charlie is blue then Charlie is nice.
((("Charlie" "is" "quiet" "+") ("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "nice" "+"))
All furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
All cold, quiet people are nice.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
If someone is furry and not rough then they are not cold.
((("someone" "is" "furry" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "cold" "-"))
All rough people are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
All nice people are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
Charlie is blue.
True
1
proof
[(triple1 OR ((triple6) -> rule2))]
("Charlie" "is" "blue" "+")
triple1
((triple6) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Dave is not quiet.
False
1
inv-proof
[(triple8 OR ((triple9) -> rule7))]
("Dave" "is" "quiet" "-")
triple8
((triple9) -> (rule7 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Harry is rough.
True
2
proof
[(((triple12) -> rule1))]
("Harry" "is" "rough" "+")
((triple12) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Fiona is not quiet.
False
2
inv-proof
[(((triple11) -> rule8) OR ((((triple10) -> rule4)) -> rule8))]
("Fiona" "is" "quiet" "-")
((triple11) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((((triple10) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Harry is quiet.
True
3
proof
[(((((triple12) -> rule1)) -> rule7))]
("Harry" "is" "quiet" "+")
((((triple12) -> (rule1 % int2))) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not quiet.
False
3
inv-proof
[(((((triple12) -> rule1)) -> rule7))]
("Harry" "is" "quiet" "-")
((((triple12) -> (rule1 % int2))) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Fiona is not rough.
Unknown
inv-rconc
[@2: Fiona is rough.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Fiona" "is" "rough" "-")
Harry is nice.
Unknown
rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "nice" "+")
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "nice" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
@0: Charlie is blue.[(triple1 OR ((triple6) -> rule2))] Charlie is furry.[(triple3)] Charlie is nice.[(triple4 OR ((triple3) -> rule4) OR ((triple5 triple1) -> rule3) OR ((triple5 ((triple6) -> rule2)) -> rule3) OR ((((triple6) -> rule7) triple1) -> rule3) OR ((((triple6) -> rule7) ((triple6) -> rule2)) -> rule3) OR ((((((triple1) -> rule1)) -> rule7) triple1) -> rule3) OR ((((((triple1) -> rule1)) -> rule7) ((triple6) -> rule2)) -> rule3))] Charlie is not cold.[(triple2)] Charlie is quiet.[(triple5 OR ((triple4) -> rule8) OR ((triple6) -> rule7) OR ((((triple1) -> rule1)) -> rule7) OR ((((triple3) -> rule4)) -> rule8))] Charlie is rough.[(triple6 OR ((triple1) -> rule1))] Charlie is young.[(triple7)] Dave is quiet.[(triple8 OR ((triple9) -> rule7))] Dave is rough.[(triple9)] Fiona is furry.[(triple10)] Fiona is nice.[(triple11 OR ((triple10) -> rule4))] Harry is blue.[(triple12)] @1: Dave is blue.[(((triple9) -> rule2))] Fiona is quiet.[(((triple11) -> rule8) OR ((((triple10) -> rule4)) -> rule8))] Harry is rough.[(((triple12) -> rule1))] @2: Harry is quiet.[(((((triple12) -> rule1)) -> rule7))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
((triple6) -> (rule2 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
((triple3) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((triple5 triple1) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((triple5 ((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((triple6) -> (rule7 % int2)) triple1) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple6) -> (rule7 % int3)) ((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule7 % int2)) triple1) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
((((((triple1) -> (rule1 % int4))) -> (rule7 % int3)) ((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
((triple4) -> (rule8 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple6) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple3) -> (rule4 % int2))) -> (rule8 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
((triple1) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple7
Dave is quiet.
("Dave" "is" "quiet" "+")
triple8
((triple9) -> (rule7 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple9
Fiona is furry.
("Fiona" "is" "furry" "+")
triple10
Fiona is nice.
("Fiona" "is" "nice" "+")
triple11
((triple10) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple12
Dave is blue.
("Dave" "is" "blue" "+")
((triple9) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple11) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((((triple10) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((triple12) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple12) -> (rule1 % int2))) -> (rule7 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2